We have put on the web the Version 3.0.1 home page, documentation, and release notes.
acl2.tar.gz: ACL2 3.0.1 gzipped tarballacl2-tar-gz-md5sum: corresponding md5sum filebooks/ 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 file:pl command or the proof-checker command
show-rewrites
(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
above patch-pl.lisp.
Place the form (load "[path].patch-pl.lisp") in your
~/acl2-init.lsp file.
OR, you can edit your [path]/saved_acl2 script to load the
above patch-pl.lisp. file. Below we show how to do this for some
Lisp implementations.
-eval argument as indicated below:exec "[path]/gcl-saved_acl2.gcl" \
-eval '(load "[path]/patch-pl.lisp")' $*-eval argument from
'(acl2::cmulisp-restart)' to:'(progn (load "[path]/patch-pl.lisp")
(acl2::cmulisp-restart))'.-e argument from
"(acl2::acl2-default-restart)" to:'(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 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