SBCL build error: package lock when compiling strategies.lisp

[ptroja]

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).

; compiling file "/home/piotr/ports/PVS/src/prover/strategies.lisp" (written 28 MAY 2015 08:15:10 AM):

; file: /home/piotr/ports/PVS/src/prover/strategies.lisp
; in: DEFUN CHECK-FORMALS
;     (MEMBER (CADR PVS:FORMALS) PVS::VARS)
; ==>
;   (SB-KERNEL:%MEMBER SB-C::ITEM LIST)
; 
; note: unable to
;   optimize
; due to type uncertainty:
;   can't tell whether the first argument is a (OR FIXNUM (NOT NUMBER))

;     (MEMBER (CAR PVS:FORMALS) PVS::VARS)
; ==>
;   (SB-KERNEL:%MEMBER SB-C::ITEM LIST)
; 
; note: unable to
;   optimize
; due to type uncertainty:
;   can't tell whether the first argument is a (OR FIXNUM (NOT NUMBER))

; in: DEFUN UPDATE-DEPENDENT-PROOF-RULE
;     (DEFUN PVS::UPDATE-DEPENDENT-PROOF-RULE (PVS:NAME PVS::ENTRY)
;       (LET* ((PVS::ARGS
;               (IF #
;                   #
;                   #))
;              (PVS::INH-FORMALS (PVS::GET-&INHERIT-ARGS PVS::ARGS)))
;         (WHEN (MEMBER PVS:NAME PVS::INH-FORMALS :TEST #'PVS::SYMBOL-EQUAL)
;           (LET (#)
;             (IF PVS::RULES-INHERITANCE
;                 #
;                 #)))))
; --> PROGN 
; ==>
;   (SB-IMPL::%DEFUN 'PVS::UPDATE-DEPENDENT-PROOF-RULE
;                    (SB-INT:NAMED-LAMBDA PVS::UPDATE-DEPENDENT-PROOF-RULE
;                        (PVS:NAME PVS::ENTRY)
;                      (BLOCK PVS::UPDATE-DEPENDENT-PROOF-RULE
;                        (LET* (# #)
;                          (WHEN # #))))
;                    NIL 'NIL (SB-C:SOURCE-LOCATION))
; 
; caught STYLE-WARNING:
;   Call to PVS::RULE-ENTRY? could not be inlined because its source code was not
;   saved. A global INLINE or SB-EXT:MAYBE-INLINE proclamation must be in effect to
;   save function definitions for inlining.

; 
; caught ERROR:
;   READ error during COMPILE-FILE:
;   
;     Lock on package SB-IMPL violated when interning BACKQ-CONS while in package
;     PVS.
;   See also:
;     The SBCL Manual, Node "Package Locks"
;   
;     (in form starting at line: 478, column: 0, position: 17695)
; compilation aborted after 0:00:00.207
;      - Binary file /home/piotr/ports/PVS/src/prover/strategies.fasl is old or does not exist. 
;        Compile (and load) source file /home/piotr/ports/PVS/src/prover/strategies.lisp instead?
;      - Should I bother you if this happens again?

[MJDSys]

@ptroja Does PR #39 help? I think that was the error it solves.

[ptroja]

Yes, it does. Thanks!