We have put on the web the Version 2.9.4 home page, documentation, and release notes.
acl2.tar.gz: ACL2 2.9.4 gzipped tarball
acl2-tar-gz-md5sum: corresponding md5sum file
patches/: optional patch files
books/and extracted. You will not be able to use previous versions of these books with a new incremental release, so if you want to use these books, be sure to fetch the tarballs!
workshops.tar.gz: Workshops tarball
workshops-tar-gz-md5sum: corresponding md5sum file
nonstd.tar.gz: ACL2(r) books tarball
nonstd-tar-gz-md5sum: corresponding md5sum file
The first set of numbers, immediately below, are from a 1-processor 2.60 GHz Pentium 4 with a 512 KB cache, running Linux (Ubuntu 5.10). 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
The second set of numbers is for runs on a 2-processor 2.7 GHz Macintosh PowerPC G5 with 512K cache per processor and 8GB of RAM, where the runs took advantage of both processors by invoking "make -j 3".
OpenMCL 1.0: real 153m59.139s user 276m30.983s sys 11m19.956s GCL 2.6.8 preliminary version: real 277m31.000s user 362m15.690s sys 143m44.793sPete Manolios reported the following times for the distributed books on a Mac OS X system with a dual 2.7 GhZ PowerPC G% and 6.5GB DDR SDRAM.
openmcl: 126m5.739s sbcl: 135m47.669s