From time to time we may release a patch file. Most users can probably get by pretty well without bothering to load a patch file.
Installation instructions appear at the top of the patch file. The "raw Lisp version" just below is one that can be loaded into raw Lisp but typically lacks some of the fixes in the "certifiable book" version.
patch-3.2-4.lisp
(certifiable book version; 5:13 pm
CDT, May 17, 2007)patch-3.2-4-raw.lisp (raw
Lisp version)
(OpenMCL and multi-threaded SBCL only) Fixed a soundness bug in the
evaluation of mbe forms in the presence of Lisp feature
:acl2-mv-as-values. Thanks to Sol Swords for reporting this problem and
sending a simple proof of nil (which can be found in a comment in the
ACL2 sources, in (deflabel note-3-3 ...)).
Fixed a bug in evaluation of calls of with-prover-time-limit.
Fixed bugs in pl (which are similarly present in the
proof-checker's sr (show-rewrites) command. The first bug was
evident from the following forms sent by Robert Krug, which caused an error.
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) :pl (mod (+ 1 x) n)The second bug was due to a failure to take note of which rules are disabled, and could be seen by executing the following (very slow!).
(defstub modulus () t) (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) :pl (mod (+ x y) (modulus))
Enhanced accumulated-persistence to break down results by useful vs.
useless rule applications. In particular, this provides information about
which rules were ever applied successfully, as requested by Bill Young.
Added coverage of :meta rules to the accumulated-persistence
statistics.
Fixed a bug that was causing a :clause-processor hint to fire on a
subgoal of the goal to which it was attached, when the original application
didn't change the clause. Thanks to Dave Greve for pointing out this bug and
providing a useful example.
A Windows Installer for ACL2 is provided courtesy
of Alex Spiridonov and Jared Davis. The download includes a Unix environment,
pre-certified standard and workshop books, and a copy of Gnu Emacs.
Performance Comparisons
The following times were for the full ACL2 regression suite (distributed and workshop books). Not shown is a successful regression run on Windows using GCL 2.6.7.
In each case 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
11799.493u 199.084s 3:23:01.41 98.4% 0+0k 0+0io 0pf+0w23238.340u 206.408s 6:35:25.26 98.8% 0+0k 0+0io 0pf+0w25371.713u 468.985s 7:15:43.23 98.8% 0+0k 0+0io 1516pf+0w33377.025u 263.156s 9:25:29.63 99.1% 0+0k 0+0io 0pf+0wmake -j 4
...", on the same machine running Debian GNU/Linux 2.6.17.8.
8975.824u 386.304s 44:57.63 347.0% 0+0k 0+0io 394pf+0w12174.492u 473.973s 57:07.33 369.0% 0+0k 0+0io 0pf+0w14672.556u 381.567s 1:09:33.14 360.7% 0+0k 0+0io 383pf+0w103051.040u 729.001s 8:04:37.51 356.9% 0+0k 0+0io 0pf+0w23424.671u 875.465s 3:33:37.75 189.5% 0+0k 0+7184io 0pf+0w26240.375u 2242.717s 8:12:29.69 96.3% 0+0k 0+12224io 0pf+0w29277.0u 551.0s 8:32:48 96% 0+0k 0+0io 0pf+0w38326.0u 443.0s 10:57:04 98% 0+0k 0+0io 0pf+0w60529.0u 1635.0s 17:28:19 98% 0+0k 0+0io 0pf+0w