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

P.P.S. I've made my final attempt to fix quicklisp in ACL2 for
LispWorks 8.0 and I seem to have gotten somewhat further along, but
I'm stuck.  I plan simply to exclude quicklisp libraries from
LispWorks-based ACL2 regressions.  I'm still open to receiving help to
fix this.

For details see:

https://www.cs.utexas.edu/users/kaufmann/quicklisp-lw/

There is also a GitHub Issue, entitled "Quicklisp for ACL2 doesn't
work with LispWorks 8.0" (# 1332) that points to this.

Thanks,
Matt