We have put on the web the Version 3.0.1 home page, documentation, and release notes.
Downloads:
acl2.tar.gz: ACL2 3.0.1 gzipped tarballacl2-tar-gz-md5sum: corresponding md5sum filepl.lisp: optional patch for :plbooks/ 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 tarballworkshops-tar-gz-md5sum: corresponding md5sum filenonstd.tar.gz: ACL2(r) books tarballnonstd-tar-gz-md5sum: corresponding md5sum fileThe following times are for certifying the full ACL2 regression suite (distributed and workshop books). The comparisons give an idea of relative performance of ACL2 built on these lisps, but are not necessarily representative of their general performance for other than ACL2. For example, ACL2 handles multiple values in at least 3 different ways depending on the underlying lisp, and it proclaims functions in some lisps but not others.
The first set of numbers, immediately below, are from a 1-processor 2.60 GHz Pentium 4 with a 512 KB cache, running Linux 2.6.17.4. 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
ACL2 3.0.1: 10262.389u 155.841s 2:56:18.82 98.4% 0+0k 0+0io 0pf+0w ACL2 3.0: 12712.650u 232.366s 3:38:32.41 98.7% 0+0k 0+0io 1pf+0w
ACL2 3.0.1: 16974.108u 402.069s 4:51:44.69 99.2% 0+0k 0+0io 0pf+0w ACL2 3.0: 19496.062u 590.336s 5:37:17.49 99.2% 0+0k 0+0io 0pf+0w
ACL2 3.0.1: 18990.630u 184.307s 5:23:10.11 98.8% 0+0k 0+0io 0pf+0w ACL2 3.0: 20236.888u 187.415s 5:43:06.93 99.2% 0+0k 0+0io 0pf+0w
ACL2 3.0.1: 18929.054u 359.858s 5:26:20.34 98.5% 0+0k 0+0io 2pf+0w ACL2 3.0: 20530.959u 494.658s 5:53:09.77 99.2% 0+0k 0+0io 0pf+0w
ACL2 3.0.1: 28129.421u 211.693s 7:59:37.23 98.4% 0+0k 0+0io 0pf+0w ACL2 3.0: 28889.313u 243.047s 8:08:04.13 99.4% 0+0k 0+0io 0pf+0w