Performance Comparisons
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).
Possible GCL/Windows issues
We have seen problems with ACL2 on GCL Version 2.6.5 on Windows. We are
providing assistance to GCL maintainer Camm Maguire as he looks into this. In
the meantime, a workaround is to download the following files and put them
in the directory with your ACL2 image (presumably the ACL2 source directory).
gazonk520.o
windows_saved_acl2
The file windows_saved_acl2 (which you are welcome to rename) will
be your ACL2 executable. Open it in an editor and edit pathnames as
indicated.
Optionally, instead of downloading gazonk520.o, you can download
gazonk520.lsp and compile it
yourself to create gazonk520.o.