ACL2 Version 3.1 News

Windows Installer
Performance Comparisons
ACL2 Course Materials

Windows Installer

Thanks to Alex Spiridonov and Jared Davis, a Windows Installer for ACL2 is available. The download includes a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs.

Performance Comparisons

The following times were for the full ACL2 regression suite (distributed and workshop books). Not shown is a successful regression run on Windows using GCL 2.6.7.

In each case 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

Linux times:

Each of the Linux runs was on the same, almost surely unloaded machine running Debian GNU/Linux 2.6.17.4.

Gnu Common Lisp (GCL), Version 2.6.7:
11728.520u 206.800s 3:24:10.87 97.4% 0+0k 0+0io 0pf+0w
SBCL 0.98:
19754.766u 486.058s 5:41:29.19 98.7% 0+0k 0+0io 0pf+0w
Allegro Common Lisp, Version 7.0:
22868.401u 247.715s 6:29:41.28 98.8% 0+0k 0+0io 0pf+0w
CMUCL 19b:
25064.694u 461.220s 7:10:48.64 98.7% 0+0k 0+0io 4pf+0w
Lispworks 4.4.6:
33156.124u 251.771s 9:19:58.55 99.4% 0+0k 0+0io 0pf+0w
CLISP 2.38:
83010.275u 577.688s 23:33:45.72 98.5% 0+0k 0+0io 6pf+0w

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.

Mac OS X times:

Each of the Macintosh runs was on the same unloaded Macintosh 2P G5 running Mac OS 10.4.8.

OpenMCL 1.0 with -j 2:
17540.280u 744.166s 2:41:06.86 189.1% 0+0k 0+6511io 0pf+0w
SBCL 0.9.12 without -j (apparently cannot run successfully with -j 2):
18362.756u 1516.801s 5:43:16.01 96.5% 0+0k 1+9786io 0pf+0w

Sun/Solaris times:

Each of the Sun/Solaris runs was on the same Sun4u sparc machine running Solaris 2.9.

Allegro 6.2:
36753.0u 542.0s 10:29:54 98% 0+0k 0+0io 0pf+0w
CMUCL 18d:
58865.0u 1597.0s 16:56:57 99% 0+0k 0+0io 0pf+0w

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