		Search-engine friendly clone of the ACL2 documentation.

Obtaining-common-lisp

Allegro-cl

Allegro Common Lisp as a host for ACL2

Allegro Common Lisp (Allegro CL) is one of the Common Lisp implementations upon which an ACL2 executable can be built (see obtaining-common-lisp). But here, we discuss a concern.

Although testing is ongoing for ACL2 built upon Allegro CL, the version used has been Allegro CL 10.1 since 2017. What's more, in September 2025, for an ACL2 executable built with host Lisp Allegro CL, the use of “make regression” resulted in four books (in the community-books) that failed to certify. We discuss those failures in the “Details” section below. These failures may suggest that Allegro CL, at least for its Version 10.1, does not correctly support the Common Lisp language, or at least there is problematic ACL2 code specific to Allegro CL. In practice we don't expect a lot of problems when using ACL2 built on Allegro CL. However, since Allegro CL is relatively slow compared to several other Common Lisp implementations that can host ACL2 — SBCL, CCL, LispWorks, and GCL — those failures suggest that Allegro CL might not be a good choice for ACL2 users.

Details

Here are details regarding the four certification failures under books/ that are referenced above. These details are quite technical and probably only of interest to system implementors.

kestrel/c/syntax/validator.lisp

The following error from the corresponding validator.cert.out file is very surprising, since the defrec form for ACL2::CLAUSE-PROCESSOR-HINT has a “cheap” flag of nil, so the same error can be expected to show up regardless of the host Lisp — yet as of this writing (in September 2025) it seems not to have shown up for a long time, if ever.
```
HARD ACL2 ERROR in ACL2::RECORD-ERROR:  An attempt was made to treat
(49683 :TYPE-PRESCRIPTION BLOCK-ITEM-TYPES) as a record of type
ACL2::CLAUSE-PROCESSOR-HINT.
```
There were other errors like that one as well.

So for that same ACL2 version (ACL2 git hash fe29908c4589c1de3b41d6c98cc8bec012c7eba3), the same book and the books that (recursively) support it were certified using a safety-3 ACL2 executable built on CCL. The book certified without any “HARD ACL2 ERROR”. This suggests that the problem is likely restricted to runs using Allegro CL.

However, that book allows some trust tags (in file cert.acl2 in that directory), so perhaps there are shenanigans that somehow exonerate the Allegro CL build of ACL2. But the last failure discussed below does not involve trust tags.
kestrel/axe/examples/aes-blast.lisp
kestrel/axe/examples/aes-blast-boolean.lisp

These two report errors (in their .cert.out files) that involve using the serialize capability to write the .cert file. But cert.acl2 in that directory allows trust tags, which could be relevant. Note that serialize errors may be very difficult to debug.

A second certification was tried on the second of these (picked arbitrarily) in case this was just a weird glitch. However, a similar error occurred (though with a slightly different backtrace).
projects/aleo/vm/circuits/axe/blake2s-proof2.lisp

This one shows a backtrace that includes the following form.
```
(RATIONALP 8444461749428370424248824938781546531375899335154063827935233455916872368129)
```
That shouldn't cause an error, but apparently it did. Maybe the image was already corrupted. Submitting that form in a fresh session produced no error.

As with the first example, a safety-3 CCL-based certification (of this book and all supporting books, recursively) produced no errors. But unlike the first example, this book does not allow trust tags. This example thus provides strong evidence that Allegro CL is not a great choice for hosting ACL2.