guard-multiplicity.lisp
in order to fix a rather obscure soundness bug, introduced in Version
3.6, that was discovered by Sol Swords after the Version 4.0 release.
Discussion and installation instructions are at the top of the file,
in particular:
This bug is unlikely to affect most users, as it can only occur when a function that returns a stobj or multiple values is called in its own guard (or the guard of a function being defined in the same mutual-recursion); even then, the use of mbe may be necessary in order to prove a contradiction.Below is the documentation that may appear in the next release notes to explain this patch.
We fixed a soundness bug that could occur when a function that returns multiple values that is called in its own guard. Thanks to Sol Swords for reporting this bug and sending a small self-contained example, which is included in a comment in the functionchk-acceptable-defuns1in ACL2 source filedefuns.lisp.
ACL2 Books Repository
The acl2-books Google
group allows you to contribute ACL2 books (input files), and also
to update to the latest version if you don't want to wait for the next
ACL2 release. Quoting from that web site:
This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.
The various cases below correspond to runs of the ACL2 regression suite (distributed and workshop books) for ACL2 executables built on different platforms, as indicated. Not shown are results of testing on Windows and Mac OS X. Also, we successfully ran the entire regression suite very shortly before final testing, using safety 3 (CCL).
Statistics shown below are for running make regression.
Each 32-bit Linux regression reported below was run with
make option -j 8 on an 8-core 2.8 GHz Intel
Processor running Ubuntu Linux. Each 64-bit Linux regression reported
below was run with make option -j 24 on a
2.6GHz machine with four processors, each a Six-Core AMD Opteron(tm)
Processor 8435. So comparisons between a 32-bit run and 64-bit run
are ill-advised.
11536.937u 201.764s 47:19.68 413.3% 0+0k 182848+965448io 145pf+0w
13205.069u 220.633s 52:16.14 428.0% 0+0k 169248+913272io 219pf+0w
12236.300u 529.861s 40:19.87 527.5% 0+0k 229352+2160456io 215pf+0w
14916.508u 824.051s 1:05:32.27 400.2% 0+0k 154168+1069816io 245pf+0w
workshops/ books. The user time alone was 63034s.
18798.386u 372.339s 59:51.87 533.7% 0+0k 223864+657208io 1189pf+0w
32808.510u 2057.476s 1:11:56.31 807.7% 0+0k 261840+1990192io 0pf+0w/pre>
19270.596u 970.160s 58:57.45 572.1% 0+0k 17248+838168io 0pf+0w
ACL2 Course Materials
At some point, perhaps "ACL2 Course Materials" may be a top-level link on the
ACL2 home page. For now, we provide some links.