ACL2 Version 3.0 News

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