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.

Here is a link to the web page for Yishai Feldman's Computer-Aided Reasoning course at The Interdisciplinary Center, Herzliya.
Ruben Gamboa and John Cowles, COSC5000: Seminar: Introduction to ACL2, Univ. of Wyoming.
John Cowles, COSC5010: Formalizing the JVM in ACL2, Univ. of Wyoming.
Links to some of Warren Hunt's courses, many of which use ACL2, may be found here.
Here is are links to web pages for two courses taught by Pete Manolios at Georgia Tech
- CS 8803 Computational Logic (Spring 2005)
- CS 8001 Hardware Verification Fall 2004
Links to some of J Moore's courses, many of which use ACL2, may be found here.
Here are links to some web pages for a course taught by Rex Page at the Univ. of Oklahoma.
Eric Smith's web page for a class at Stanford

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.

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

Gnu Common Lisp (GCL), Version 2.6.5:
7466.960u 129.770s 2:11:31.18 96.2% 0+0k 0+0io 11430218pf+0w
Allegro Common Lisp, Version 6.2:
10615.780u 149.870s 3:06:06.97 96.4% 0+0k 0+0io 8109773pf+0w
CMUCL 19a:
11589.550u 245.780s 3:31:30.61 93.2% 0+0k 0+0io 9459367pf+0w
CLISP 2.33:
49368.210u 316.910s 14:08:00.34 97.6% 0+0k 0+0io 4157852pf+0w
Lispworks: Time omitted (run on slower machine due to license issue).

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))))
        (t
         nil)))