Matt Kaufmann, 12/16/2021 (supporting GitHub Issue #1332)
I found that ACL2 community
book books/quicklisp/base.lisp fails to certify with
ACL2 built on LispWorks Version 8.0. Here I describe my attempts to
fix the problem. It would be great if someone could
fix books/quicklisp!
My final email (12/16/2021) to acl2-help on this issue:
My first two emails to acl2-help on this issue:
David Rager was kind enough to talk with me about this issue, in
particular pointing me to the wiki page
https://github.com/acl2/acl2/wiki/How-to-update-quicklisp
and mentioning that the section "Adding Quicklisp Libraries"
of :DOC
quicklisp isn't only about adding libraries, but also is
about updating.
I came away with the impression that asdf should be loaded
from books/quicklisp/bundle/asdf.lisp, not from whatever
asdf is provided by the host Lisp with (require "asdf"),
but that wasn't happening. We have been getting away with that,
apparently, but LispWorks is using a later version of asdf (3.3.5)
than SBCL (3.3.1) or CCL (3.3.3), as per Lisp
variable ASDF/UPGRADE:*ASDF-VERSION*, which can be read
after executing (require "asdf").
So my final attempt was to force a load
of books/quicklisp/bundle/asdf.lisp. That seemed to
help, but an error occurred when attempting to load something related
to Bordeaux threads; see
the base.cert.out
file for that run (which is the one linked to under "final email"
above). Here are diffs showing that final attempt.
eld:/projects/acl2/acl2-lw/books/quicklisp% git diff .
diff --git a/books/quicklisp/base-raw.lsp b/books/quicklisp/base-raw.lsp
index 78d176eeb..0a94d1348 100644
--- a/books/quicklisp/base-raw.lsp
+++ b/books/quicklisp/base-raw.lsp
@@ -32,7 +32,9 @@
; It may be that we should do this for all Lisps instead of just Allegro.
-#+(or allegro lispworks)
+; Matt K. mod, 12/2021: Formerly lispworks was included here, but now that's
+; dealt with near the top of bundle/bundle.lisp.
+#+allegro
(load "bundle/asdf.lisp")
; Preload (i.e., compile) all Quicklisp libraries that we're making available.
diff --git a/books/quicklisp/bundle/bundle.lisp b/books/quicklisp/bundle/bundle.lisp
index 8f7145977..70c5deabd 100644
--- a/books/quicklisp/bundle/bundle.lisp
+++ b/books/quicklisp/bundle/bundle.lisp
@@ -1,7 +1,12 @@
(cl:in-package #:cl-user)
(eval-when (:compile-toplevel :load-toplevel :execute)
+ #-lispworks
(require "asdf")
+; Matt K. mod, 12/2021: get the appropriate ASDF loaded rather than the one
+; from LispWorks.
+ #+lispworks
+ (load "bundle/asdf.lisp")
(unless (find-package '#:asdf)
(error "ASDF could not be required")))
eld:/projects/acl2/acl2-lw/books/quicklisp%