A few days ago I successfully built ACL2 Version 3.0 on top of SBCL 0.9.12 on
Mac OS 10.4.6 (Darwin Kernel Version 8.6.0). However, the "-j" option for
"make" doesn't yet work for me; just thought I'd let you know in case this is
news to you, given your "next on the list" remark below. But there's no hurry
as far as I'm concerned.
SBCL has impressive performance. You might find interesting the Performance
Comparisons at http://www.cs.utexas.edu/users/moore/acl2/v3-0/new.html.
From: Christophe Rhodes <csr21@...>
Date: Thu, 09 Feb 2006 13:32:50 +0000
Sender: Christophe Rhodes <csr21@...>
X-SpamAssassin-Status: No, hits=-2.1 required=5.0
X-UTCS-Spam-Status: No, hits=-282 required=180
Matt Kaufmann <kaufmann@...> writes:
> Great! I appreciate your efforts and that of the SBCL developer community,
> including Juho Snellman <jsnell@...> who has helped a lot in earlier email
The utf-8 segmentation fault in subsumption-subst.lisp should now be
fixed (there was a buffer overread in the resyncing code for
variable-width external formats); the acl2 regression test just ran to
completion here on a Linux/PPC dual G5 with sbcl-0.9.9.24.
> In my original bug report, I mentioned other errors in "make -j 2
> regression" and "make -j 3 regression" that occur at other (earlier)
> points in the regression than the one you've been looking at.
Right, investigation of these is next on the list.
> If there is an SBCL test suite, perhaps you'll want to add the ACL2
> 2.9.4 regression to it (instructions are in my original bug email),
> and perhaps later releases as well.
There is an SBCL test suite, but the various distributed developers
don't all have access to very fast hardware -- and indeed even on a
very recent G5 the ACL2 regression tests take upwards of 3 hours,
which is impractical to run on every commit.
> There's an ACL2 mailing list with links from the ACL2 home page, or
> I can just make a note to email sbcl-devel upon new ACL2 releases,
> generally every few months, if you like.
This might be useful, or indeed (since sbcl is simple, we hope, to
build) regressions could be tested for by an interested ACL2 user or