Quicklisp
An ACL2 connection to the Quicklisp system for installing Lisp
libraries.
About Quicklisp
Quicklisp is a Common Lisp equivalent to tools like CPAN for Perl, or RubyGems for Ruby. It lets you to easily install and
load the latest versions of Common Lisp libraries (and their dependencies).
To make it easy to use Quicklisp from ACL2 we have developed some wrapper
books in the books/quicklisp directory. These books serve as the
basis for other libraries such as oslib and the ACL2 bridge.
Naturally, all of these books require trust-tags.
Every ANSI-compliant host Common Lisp suitable for ACL2 should support the
use of Quicklisp, where occasionally libraries may need to be installed. As of
late 2016, all host Common Lisp implementations suitable for ACL2 are
sufficiently ANSI-compliant for the use of Quicklisp except for GCL.
Because of this, if you want to use the Quicklisp books or any libraries
that depend on them, you may need to manually enable the Quicklisp
build. Please see the instructions in books-certification for the most
up-to-date details about how to do this.
In order to certify the Quicklisp books, OpenSSL may need to be installed in
the system. At least one instance was observed in which the certification of
the Quicklisp books on macOS Catalina with SBCL failed initially, but worked
after installing OpenSSL via Homebrew (using the command brew install
openssl). The initial certification error did not explicitly mention
OpenSSL, but rather a SIGABRT; thus, if this kind of certification error
is observed, installing OpenSSL may solve the problem. Additionally, on a Mac
Arm64 (e.g. M1) machine, you may need to create symlinks to Homebrew's OpenSSL
library files in /usr/local/lib (using the command ``ln -s
/opt/homebrew/opt/openssl/lib/*.dylib /usr/local/lib''). Note that Homebrew,
which is a package/application manager for Mac, can be installed from https://brew.sh, following the simple instructions
there.
Using the Quicklisp Books
Most ACL2 users will have no reason to directly load the Quicklisp
books in books/quicklisp. Instead, you will want to load
higher-level ACL2 libraries like oslib or the ACL2 bridge. This
is because the Quicklisp books only deal with getting the appropriate Common
Lisp libraries loaded—they do not, by themselves, introduce ACL2 wrapper
functions for actually using the associated Lisp libraries.
However, if you are an advanced user who wants to use Common Lisp libraries
to develop your own ACL2 extensions, then you will typically want to:
- Include the books for whichever libraries you want to use. For instance,
to load CL-FAD and OSICAT you could do:
(include-book "quicklisp/cl-fad" :dir :system)
(include-book "quicklisp/osicat" :dir :system)
- Add your own trust-tags, drop into raw Lisp with include-raw,
and implement your extension. How exactly to do this is, alas, far beyond the
scope of this documentation, but we do try to give some hints below.
Finding Quicklisp Libraries
If you don't know much about Quicklisp and are wanting to find out about the
available libraries, the following may be useful:
Adding Quicklisp Libraries
The books in quicklisp only wrap up a few Common Lisp libraries
that we have found to be useful. But it should be very easy to experiment with
any other Quicklisp libraries.
Basic steps:
- Edit quicklisp/update-libs.lsp and add the libraries you want
to the list.
- Run the update-libs.sh script. This should download the new libraries
into your quicklisp/bundle directory.
- Extend quicklisp/base-raw.lsp to load the new library and
certify it. This base book really is just a way to get the bundle loaded
into an ACL2 session so that the libraries can be found as needed. It
also (locally) loads the libraries that we expect to use, which ensures
everything gets downloaded at the same time, and avoids potential problems with
simultaneously compiling Common Lisp libraries during parallel builds.
- Add a new quicklisp/yourlib.lisp book, styled after the other
books in the Quicklisp directory. The book doesn't really need to live in the
quicklisp directory, but keeping them there makes it easy to see what we
are depending on and, if necessary, to change the way the wrappers work.
- Include your new book in quicklisp/top.lisp, just for
completeness. (Hrmn, actually this book probably isn't very useful for
anything.)
Note that you can also develop your own Common Lisp libraries or do one-off
hacking using the local-projects feature of the bundle directory. See the
documentation for Quicklisp Bundles for
more information.
Developing ACL2 Extensions
After you've added a Common Lisp library, how do you actually use it from
ACL2? As an example, say we want to make use of the CL-JSON library.
Normally you would do something like this:
; ** my-book.lisp
(in-package "MY-PKG")
; ** Load the library (after adding it as described above)
(include-book "quicklisp/cl-json" :dir :system)
; ** [OPTIONAL] develop a logical story so you can use the
; ** library from proper ACL2 functions...
(defun foo (x y z)
(declare (xargs :guard ...))
(progn$
(er hard? 'foo "Raw lisp definition not installed?")
(logical-story-of-foo x y z)))
; ** Add a ttag since we're going to use include-raw
(defttag :my-book)
; ** Tell cert.pl that we're going to be loading raw Lisp code
;; (depends-on "my-book-raw.lsp")
; ** Actually include the raw Lisp code for our book
(include-raw "my-book-raw.lsp"
:do-not-compile t
:host-readtable t)
You usually need to use the :host-readtable option because real Common
Lisp libraries will use things (packages, floats, etc.) that ACL2's reader will
reject. You usually need to use :do-not-compile because otherwise you
tend to not have the right packages around at compile time. You may be able to
work around that using eval-when.
The corresponding raw file, then would look something like this:
; ** my-book-raw.lsp
(in-package "MY-PKG")
; ** Redefine our interface functions, freely using cl-json
; ** functionality
(defun foo (x y z)
(cl-json:...))
The user has access to the CL-JSON functionality because the non-raw
cl-json.lisp book is included in the non-raw my-book.lisp book.
