In case you are using Redhat FC1 and are thinking of using GCL, you may want to read the following note from Jonathan S. Shapiro, who tells me that the GCL maintainer is working on the problem -- hence future versions of GCL may be OK on Redhat FC1, but currently GCL cannot be built on that platform.
It seems that the exec-shield changes that were introduced in Redhat Fedora Core 1 (FC1) render GCL non-functional. There is a workaround, but it requires disabling a major FC1 security feature, which is inadvisable.
The best solution for the moment is to use CMUCL instead, which runs fine under Fedore Core 1. After installing CMUCL, I successfully built ACL2 with the commandmake LISP=lispWe have made the relevant RPM files available from the Systems Research Laboratory at Johns Hopkins University. If you like, you can simply download them from:http://srl.cs.jhu.edu/YUM/srl-stuff
In general, see ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/images/README.html
for links to ACL2 executables. Each
.md5sum file was
md5sum. We may add additional links from time to
This bug will be fixed when ACL2 Version 2.8 is released, which may not be for
a few months. In the meantime, if you want a fix, you can replace source file
proof-checker-b.lisp with a fixed version, which modifies the
functionality of the above commands. Simply obtain the
proof-checker-b.lisp with that file, and
With this fix, the proof-checker's
expand command will succeed
only when the function symbol of the current term is a defined function symbol,
in which case the original definition is always used, in analogy to how the
:expand hint works in the prover; see :DOC HINTS.
Here is an example that exhibits the above bug.
(in-package "ACL2") (encapsulate (((foo *) => *) ((bar *) => *)) (local (defun foo (x) x)) (local (defun bar (x) (not x))) (defthm foo-open (equal (foo x) x) :rule-classes :definition) (defthm bar-not-foo (equal (bar x) (not (foo x))) :rule-classes :definition)) (defthm bad (equal (foo x) (bar x)) :rule-classes nil :instructions ((:dv 1) :expand :nx :expand :top :s)) (defthm contradiction nil :rule-classes nil :hints (("Goal" :use bad)))
make regression-fresh" was timed on the same Linux machine (a 731 MH Pentium III) for ACL2 images built on top of various Lisp implementations. We have been told that CMUCL may not do nearly this well comparatively under Solaris.
Below, the first number, User time, is probably the most relevant for comparisons. The format (from the man page) is:
%Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k %Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps
18185.620u 149.210s 5:08:24.64 99.0% 0+0k 0+0io 6148850pf+0w
18896.280u 112.610s 5:18:16.54 99.5% 0+0k 0+0io 5812334pf+0w
23629.520u 276.780s 6:39:37.41 99.7% 0+0k 0+0io 5893266pf+0w
31541.270u 146.320s 8:50:51.33 99.4% 0+0k 0+0io 6390416pf+0w
83436.380u 300.320s 23:39:51.76 98.2% 0+0k 0+0io 3242033pf+0w