ACL2 Version 2.9 News

Contributing Books to ACL2

Please see the email request for contributing and documenting ACL2 books and the instructions for contributing books to ACL2.

The POPLmark Challenge

An email has been placed here

ACL2 Course Materials

At some point, perhaps "ACL2 Course Materials" will be a top-level link on the ACL2 home page. For now, we provide some links.

OpenMCL patch

There is a bug that could affect users of OpenMCL Version 0.14.2 or 0.14.3 under Version 10.4 or 10.4.1 of Mac OS X. You can obtain a fix here, graciously provided by Gary Byers.

GCL Tips

Incremental Releases

NOTE: If you fetch an incremental release then you are advised to skip the remainder of this page.

Performance Comparisons: Linux

For more up-to-date performance comparisons than is found below, follow the link just above to the latest incremental release.

The following times were for the full ACL2 regression suite (distributed and workshop books), on the same, almost surely unloaded, x86 machine running Debian GNU/Linux 3.0.

Below, the first number, User time, is probably the most relevant for comparisons. The format is essentially:

         %Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k
         %Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps
Note: Noah Friedman has observed that the difference in performance for CLISP is due to its bytecode-interpreted runtime vs. [for example] GCL's native object code execution.

Performance Comparisons: Mac OS X

Robert Krug has supplied the following timing results for distributed books (hence not including the workshop books), using a Dual 2.7 GHz PowerPC G5 with 6 GB DDR SDRAM. He says: "All of these times are an average from three runs. None of these runs varied by more than one percent on the user or sys times, although the real times varied by about two percent."

GCL: 2.6.7 CLtL1
real: 131m
user: 98m30s
sys: 32m30s

OpenMCL 0.14.3
real: 105m
user: 98m45s
sys:  4m30s

OpenMCL 1.0 32 bit
real: 94m
user: 88m30s
sys: 3m:30s

OpenMCL 1.0 64 bit
real: 105m
user: 98m30s
sys: 4m45s

Patch for an arithmetic book

Robert Krug has supplied the following patch for a distributed book: books/arithmetic-3/bind-free/integerp.lisp, in order to prevent potential looping. This change appears in the incremental releases following ACL2 Version 2.9.
(defun reduce-integerp-+-fn-1 (x mfc state)
  (declare (xargs :guard (and (pseudo-termp x)
                              (eq (fn-symb x) 'BINARY-+))))
  (cond ((and (not (equal (fargn x 1) ''0))
              (proveably-integer (fargn x 1) mfc state))
         (list (cons 'z (fargn x 1))))
        ((eq (fn-symb (fargn x 2)) 'BINARY-+)
         (reduce-integerp-+-fn-1 (fargn x 2) mfc state))
        ((and (not (equal (fargn x 2) ''0))
              (proveably-integer (fargn x 2) mfc state))
         (list (cons 'z (fargn x 2))))