Release Notes: The accumulated-persistence utility can now do finer-grained tracking, providing data for individual hypotheses and the conclusion of a rule. The defattach utility now permits the use of :program mode functions, though this requires the use of a trust tag. Redefinition is no longer permitted for functions that have attachments. The system function translate-and-test now permits its LAMBDA form to refer to the variable WORLD, which is bound to the current ACL2 logical world. The built-in "untranslate" functions were improved to produce let* expressions when appropriate.
Release Notes: There is improved support for controlling the printer and "eviscerating" large objects. Certificate files now take advantage of structure sharing and are more compact. The user now has more control over the "rulers" used in termination analysis. Many various efficiency improvements have been made, mainly with respect to supporting very large objects. A few soundness bugs have been patched, and there have been numerous other bugfixes.
Release Notes: A soundness bug and some other minor bugs have been fixed. Including books has been sped up by as much as 50%. Rewriting can be dynamically monitored. Accumulated persistence supports meta-rules and identifies useless rules, and many other minor updates have been made.
Release Notes: A few soundness bugs were identified and corrected along with several potential hard Lisp errors and other minor issues. The performance of theory invariants has been improved. New books include a resolution/paramodulation prover, concurrency modelling, transfinite induction, and a simplification utility. A new "trust tag" feature allows the use of potentially unsafe features in ACL2 extensions.
Release Notes: Several bugs were fixed, including a soundness bug. Efficiency has been significantly improved, and the regression suite runs about 20% faster. New features include time limits for the prover, enhanced controls for compilation with certify-book, and a new utility for debugging failed encapsulate and progn events.
Release Notes: A new make-event feature was introduced. It is almost like macros that take state. Better support was provided for :definition rules with :expand hints. Disabling guard checking was added. User-contributed books are now supported, and a variety of features have been improved, including guard verification involving ground terms, theory invariants, and diabling defthm events. A soundness bug related to certain local events has been fixed, as have minor bugs related to cw-gstack, wet, embeddable events, the prompt, proof trees, stobj printing, and :puff.
Release Notes: This release added a simple system for saving ACL2 images with "preloaded" theories and support for profiling your ACL2 functions using GCL (with gprof). Minor cleanups were made in the ground zero theory, several lemmas were added to the RTL books, and the system call mechanism for portable output redirection was improved. Untranslate preprocessing was added along with a new book that provides pattern-based untranslation. Various (non-soundness) bugfixes related to guards, linear arithmetic, the proof checker, and the ground zero theory were made.