{"action":"closed","issue":{"url":"https://api.github.com/repos/SRI-CSL/PVS/issues/44","labels_url":"https://api.github.com/repos/SRI-CSL/PVS/issues/44/labels{/name}","comments_url":"https://api.github.com/repos/SRI-CSL/PVS/issues/44/comments","events_url":"https://api.github.com/repos/SRI-CSL/PVS/issues/44/events","html_url":"https://github.com/SRI-CSL/PVS/issues/44","id":81866123,"number":44,"title":"SBCL build error: package lock when compiling strategies.lisp","user":{"login":"ptroja","id":161602,"avatar_url":"https://avatars.githubusercontent.com/u/161602?v=3","gravatar_id":"","url":"https://api.github.com/users/ptroja","html_url":"https://github.com/ptroja","followers_url":"https://api.github.com/users/ptroja/followers","following_url":"https://api.github.com/users/ptroja/following{/other_user}","gists_url":"https://api.github.com/users/ptroja/gists{/gist_id}","starred_url":"https://api.github.com/users/ptroja/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ptroja/subscriptions","organizations_url":"https://api.github.com/users/ptroja/orgs","repos_url":"https://api.github.com/users/ptroja/repos","events_url":"https://api.github.com/users/ptroja/events{/privacy}","received_events_url":"https://api.github.com/users/ptroja/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-05-28T10:27:28Z","updated_at":"2015-05-29T07:15:31Z","closed_at":"2015-05-29T07:15:31Z","body":"I am getting an error when compiling with the latest SBCL on Linux (sbcl-1.2.11-x86-64-linux, binary package from SBCL website; compilation on Debian Wheezy).\r\n\r\n```lisp\r\n; compiling file \"/home/piotr/ports/PVS/src/prover/strategies.lisp\" (written 28 MAY 2015 08:15:10 AM):\r\n\r\n; file: /home/piotr/ports/PVS/src/prover/strategies.lisp\r\n; in: DEFUN CHECK-FORMALS\r\n;     (MEMBER (CADR PVS:FORMALS) PVS::VARS)\r\n; ==>\r\n;   (SB-KERNEL:%MEMBER SB-C::ITEM LIST)\r\n; \r\n; note: unable to\r\n;   optimize\r\n; due to type uncertainty:\r\n;   can't tell whether the first argument is a (OR FIXNUM (NOT NUMBER))\r\n\r\n;     (MEMBER (CAR PVS:FORMALS) PVS::VARS)\r\n; ==>\r\n;   (SB-KERNEL:%MEMBER SB-C::ITEM LIST)\r\n; \r\n; note: unable to\r\n;   optimize\r\n; due to type uncertainty:\r\n;   can't tell whether the first argument is a (OR FIXNUM (NOT NUMBER))\r\n\r\n; in: DEFUN UPDATE-DEPENDENT-PROOF-RULE\r\n;     (DEFUN PVS::UPDATE-DEPENDENT-PROOF-RULE (PVS:NAME PVS::ENTRY)\r\n;       (LET* ((PVS::ARGS\r\n;               (IF #\r\n;                   #\r\n;                   #))\r\n;              (PVS::INH-FORMALS (PVS::GET-&INHERIT-ARGS PVS::ARGS)))\r\n;         (WHEN (MEMBER PVS:NAME PVS::INH-FORMALS :TEST #'PVS::SYMBOL-EQUAL)\r\n;           (LET (#)\r\n;             (IF PVS::RULES-INHERITANCE\r\n;                 #\r\n;                 #)))))\r\n; --> PROGN \r\n; ==>\r\n;   (SB-IMPL::%DEFUN 'PVS::UPDATE-DEPENDENT-PROOF-RULE\r\n;                    (SB-INT:NAMED-LAMBDA PVS::UPDATE-DEPENDENT-PROOF-RULE\r\n;                        (PVS:NAME PVS::ENTRY)\r\n;                      (BLOCK PVS::UPDATE-DEPENDENT-PROOF-RULE\r\n;                        (LET* (# #)\r\n;                          (WHEN # #))))\r\n;                    NIL 'NIL (SB-C:SOURCE-LOCATION))\r\n; \r\n; caught STYLE-WARNING:\r\n;   Call to PVS::RULE-ENTRY? could not be inlined because its source code was not\r\n;   saved. A global INLINE or SB-EXT:MAYBE-INLINE proclamation must be in effect to\r\n;   save function definitions for inlining.\r\n\r\n; \r\n; caught ERROR:\r\n;   READ error during COMPILE-FILE:\r\n;   \r\n;     Lock on package SB-IMPL violated when interning BACKQ-CONS while in package\r\n;     PVS.\r\n;   See also:\r\n;     The SBCL Manual, Node \"Package Locks\"\r\n;   \r\n;     (in form starting at line: 478, column: 0, position: 17695)\r\n; compilation aborted after 0:00:00.207\r\n;      - Binary file /home/piotr/ports/PVS/src/prover/strategies.fasl is old or does not exist. \r\n;        Compile (and load) source file /home/piotr/ports/PVS/src/prover/strategies.lisp instead?\r\n;      - Should I bother you if this happens again?\r\n```"}}