ACL2 Version 2.7 News

GCL on Redhat FC1

For Redhat Fedora Core 1 ACL2 users only:

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 command 

	  make LISP=lisp
We 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

Executable saved images

Jared Davis has graciously provided an ACL2 2.7 Binary for Windows. That page explains that download may be slow. If you experience problems, please email us and we will make this avaiable from UT.

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 created using md5sum. We may add additional links from time to time.

Bugs

We have discovered, thanks to an example sent in by John Erickson, that ACL2 has had a soundness bug (probably for many years) that can occur when using the proof-checker. Specifically, the expand command, and hence x and x-dumb commands (which call expand), are involved; see :DOC PROOF-CHECKER-COMMANDS. The bug can occur when applying the above commands when the current term is a call of a constrained function symbol for which there is a :definition rule.

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 fixed-proof-checker-b.lisp and replace proof-checker-b.lisp with that file, and recompile/rebuild.

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)))

Performance comparisons

Below are times reported when "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