The second incremental release of ACL2 is available, as described in an announcement already sent to the acl2 mailing list
Click here for a text-only copy of the release
notes. For the full updated documentation, download the release:
Also available, but optional, are these corresponding extra books, which
can be placed in
books/ and extracted.
Finally: Jared Davis has kindly provided a Windows installer for ACL2 Version 2.9.2..
The following times were for the full ACL2 regression suite (distributed and
workshop books), on the same, almost surely unloaded, x86 machine running
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.
- Gnu Common Lisp (GCL), Version 2.6.6:
10119.890u 140.310s 2:54:39.16 97.9% 0+0k 0+0io 12231519pf+0w
- Allegro Common Lisp, Version 6.2:
14456.560u 172.440s 4:07:50.43 98.3% 0+0k 0+0io 8555056pf+0w
- CMUCL 19a:
15172.750u 293.310s 4:23:30.34 97.8% 0+0k 0+0io 9938663pf+0w
- CLISP 2.33:
68754.020u 401.530s 19:25:31.69 98.8% 0+0k 0+0io 4019814pf+0w