We have put on the web the Version 3.0.1 home page, documentation, and release notes.
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
:plcommand or the proof-checker command
sr), and would like a fix. Here we include a patch for
:pl, for which we expect to have the following description in the next release notes.
Fixed a bug in :pl and the proof-checker's show-rewrites (sr) command that was causing a Lisp break. For :pl, also improved the display of unifying substitutions, modified output to take binding hypotheses (equal var term) into account properly, and arranged for inclusion of meta rules that modify the given term. Thanks to Eric Smith for bringing these issues to our attention.For this particular issue it's fine to load a patch into raw Lisp (not always a sound way to deal with patches, but in this case it's fine):
Below are two methods to choose from if you would like the patch file to be
loaded automatically, where below we write "
[path]" in place of
the absolute pathname of your ACL2 sources directory, to which you save the
Place the form
(load "[path].patch-pl.lisp") in your
OR, you can edit your
[path]/saved_acl2 script to load the
patch-pl.lisp. file. Below we show how to do this for some
-evalargument as indicated below:
exec "[path]/gcl-saved_acl2.gcl" \
-eval '(load "[path]/patch-pl.lisp")' $*
'(progn (load "[path]/patch-pl.lisp") (acl2::cmulisp-restart))'.
'(progn (load "[path]/acl2-sources/patch-pl.lisp") (acl2::acl2-default-restart))'.
The 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 22.214.171.124. 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