ACL2 Version 3.0 News

Table of Contents

• Performance Comparisons
• Patch for GCL profiling
• Contributing Books to ACL2
• The POPLmark Challenge
• ACL2 Course Materials
• OpenMCL patch
• GCL Tips

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.

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:

• Gnu Common Lisp (GCL), Version 2.6.7:
  12712.650u 232.366s 3:38:32.41 98.7% 0+0k 0+0io 1pf+0w
• SBCL 0.98:
  19496.062u 590.336s 5:37:17.49 99.2% 0+0k 0+0io 0pf+0w
• Allegro Common Lisp, Version 7.0:
  20236.888u 187.415s 5:43:06.93 99.2% 0+0k 0+0io 0pf+0w
• CMUCL 19b:
  20530.959u 494.658s 5:53:09.77 99.2% 0+0k 0+0io 0pf+0w
• Lispworks:
  28889.313u 243.047s 8:08:04.13 99.4% 0+0k 0+0io 0pf+0w
• CLISP 2.38:
  72702.279u 515.380s 20:32:36.02 99.0% 0+0k 0+0io 2pf+0w

Mac OS X times:

• OpenMCL 1.0 with -j 2:
  23021.449u 879.092s 3:28:30.71 191.0% 0+0k 0+6912io 0pf+0w
• SBCL 0.9.12 without -j (apparently cannot run successfully with -j 2):
  23818.622u 2021.217s 7:25:12.69 96.7% 0+0k 0+9797io 0pf+0w
• GCL 2.6.8pre with -j 2:
  25229.008u 9517.534s 5:11:23.07 185.9% 0+0k 0+10168io 0pf+0w

Sun/Solaris times:

• Allegro 6.2:
  33600.0u 367.0s 9:56:57 94% 0+0k 0+0io 0pf+0w
• CMUCL 18d:
  52551.0u 1579.0s 15:47:15 95% 0+0k 0+0io 0pf+0w

• 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.
  • http://www.cs.ou.edu/~rlpage/SEcollab/rlpNotesCAR.zip
  • http://www.cs.ou.edu/~rlpage/SEcollab/rlpSEprojects.zip
  • http://www.cs.ou.edu/~rlpage/SEtools/ACL2books/
• Eric Smith's web page for a class at Stanford

• Installing ACL2 on top of GCL 2.6.5 in an X86 running Fedora Core 3
• Building on GCL 2.6.0 and earlier