From: Matt Kaufmann <kaufmann@cs.utexas.edu>
To: ACL2 Help <acl2-help@utlists.utexas.edu>
Subject: quicklisp-related certification failure
Date: Wed, 15 Dec 2021 12:55:53 -0600
Reply-To: Matt Kaufmann <kaufmann@cs.utexas.edu>
Archived-At: <https://utlists.utexas.edu/sympa/arcsearch_id/acl2-help/2021-12/t4dpmpxae9y.fsf%40cs.utexas.edu>

Hi acl2-help,

This email is directed at anyone who knows something about quicklisp.
(I'm not such a person!)

I've installed a new version of LispWorks on a linux machine: Version
8.0, where formerly I used Version 7.1.2.  With the new version I got
a certification failure (repeatedly) for books/quicklisp/base.lisp,
with the following error.

HARD ACL2 ERROR in INCLUDE-RAW:  Load of "base-raw.lsp" failed with
the following message:
ASDF/SYSTEM:SYSTEM-DESCRIPTION is defined as an ordinary function #<Function
ASDF/SYSTEM:SYSTEM-DESCRIPTION 41E001E384>

That error occurred immediately after the following in the
base.cert.out file.

; Upgrading ASDF from version 3.3.5 to version 3.3.1

That's disturbing, since decreasing a version number isn't what one
would normally call "upgrading".  This was generated by running
cert.pl on base.lisp, which I tried repeatedly after the original
failure.  The full log may be found here (at least for now):

https://www.cs.utexas.edu/users/kaufmann/base.cert.out

Here's the corresponding message from the LispWorks 7.1.2 run:

; Upgrading ASDF from version 3.3.0 to version 3.3.1

Both LispWorks runs were with the latest github version of ACL2
(commit hash: 693d8e0b7aa3551ba1aaafcb47bf64082d8ac293).

Any suggestions?  It would be sad not to be able to run a full ACL2
regression with LispWorks as the host Lisp.

Thanks,
Matt

============================================================

From: Matt Kaufmann <kaufmann@cs.utexas.edu>
To: ACL2 Help <acl2-help@utlists.utexas.edu>
Subject: Re: quicklisp-related certification failure
In-Reply-To: <t4dpmpxae9y.fsf@cs.utexas.edu> (message from Matt Kaufmann on Wed, 15 Dec 2021 12:55:53 -0600)
Date: Wed, 15 Dec 2021 14:47:35 -0600
Reply-To: Matt Kaufmann <kaufmann@cs.utexas.edu>
Archived-At: <https://utlists.utexas.edu/sympa/arcsearch_id/acl2-help/2021-12/t4dmtl1a93s.fsf%40cs.utexas.edu>

P.S. More info here for anyone willing and able to help with the
quicklisp issue that I reported:

I see the following two forms at the end of books/quicklisp/base.lisp,
where the second is the one that causes the error.

; (depends-on "bundle/bundle.lisp")
(include-raw "bundle/bundle.lisp" :host-readtable t)

; (depends-on "base-raw.lsp")
(local (include-raw "base-raw.lsp"
                    :host-readtable t
                    :do-not-compile t))

Near the top of books/quicklisp/bundle/bundle.lisp I see the following:

(require "asdf")

So after starting a LispWorks build of ACL2 I did the following.

ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2 1 > (require "asdf")
; Loading /v/filer5b/v11q001/acl2/lisps/lispworks/lw64-8.0/lib/8-0-0-0/load-on-demand/utilities/asdf.64ufasl on demand...
T

ACL2 2 > (symbol-function 'ASDF/SYSTEM:SYSTEM-DESCRIPTION)
#<Function ASDF/SYSTEM:SYSTEM-DESCRIPTION 418008200C>

ACL2 3 >

Notice that the function is indeed an ordinary function.  My guess is
that it's not good that asdf was loaded from the LispWorks
distribution rather than the books quicklisp bundle, but I don't know.

On the other hand, the last form in that base.lisp file is (as noted
above) one that loads books/quicklisp/base-raw.lsp, which has the
following forms.

; It may be that we should do this for all Lisps instead of just Allegro.
#+(or allegro lispworks)
(load "bundle/asdf.lisp")

When in a fresh session I load bundle/asdf.lisp (while standard in
books/quicklisp/) I get a different, "generic" function for
ASDF/SYSTEM:SYSTEM-DESCRIPTION.

ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2 1 > (load "bundle/asdf.lisp")
; Loading text file /v/filer5b/v11q001/acl2/acl2-lw/books/quicklisp/bundle/asdf.lisp
#P"/v/filer5b/v11q001/acl2/acl2-lw/books/quicklisp/bundle/asdf.lisp"

ACL2 2 > (symbol-function 'ASDF/SYSTEM:SYSTEM-DESCRIPTION)
#<STANDARD-GENERIC-FUNCTION ASDF/SYSTEM:SYSTEM-DESCRIPTION 418001BAF4>

ACL2 3 >

This is probably all I've got to offer on this issue.  Suggestions?

Thanks,
Matt