#+sbcl (sb-ext:unlock-package "COMMON-LISP")

was added before the loads to keep SBCL happy.
This patch came from Matthias Hoelzl <tc@xantira.com>
Fix compilation issues on OSX Mavericks from Matthias Hoelzl <tc@xantira.com>
From Matthias Hoelzl <tc@xantira.com>: Fix build on Centos 6.5 x64
Changed binpath to exported PVSBINPATH to support pvs-info
1. Changed excl:without-interrupts to excl:with-delayed-interrupts
2. Added pvs-meta-info function to collect PVS information, useful for
   ETB and bug reporting.
1. Added a context stack, and push-context and pop-context commands
2. Modified load-strategies-file to let the load wrapper know that strategies
   files are being loaded.
Added missing commands to menu, and rearranged
Added library slot to pvs-formula-reference struct
Modified show-declaration, goto-declaration, whereis-declaration-used,
unusedby-proof-of-formula, usedby-proofs, and show-expanded-form to work with
libraries as well as PVS files in the current context.
Modified pvs-formula-origin to include the library in the
pvs-formula-reference
Modified current-pvs-file to allow for PVS files from libraries
Misc fixes
Fixed get-file-git-sha1 for allegro/sbcl
Fixed pvs-ltx.el for older versions of Emacs