What's New in ACL2 Matt Kaufmann and J Moore July 13, 2003 This talk gives an overview of some recent changes to ACL2, in particular: - Some of what's coming in ACL2 Version 2.8; - Features of ACL2 Version 2.7 that may deserve emphasis. The talk is organized by documentation subtopics of note-2-8, followed by highlights from note-2-7. The complete topics are available on the web, as are these notes. Many users of ACL2 have contributed bug reports and enhancements requests that have led to these improvements, as acknowledged in the detailed documentation referenced above. Thanks! Acknowledgements appear in the full documentaton, but for brevity, here we only acknowledge implementation contributions. =============================================================================== NOTE-2-8-NEW-FUNCTIONALITY ACL2 Version 2.8 Notes on New Functionality Defexec and mbe allow one to attach executable counterparts to functions. For example, consider the following. (DEFUN F (X) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (<= 0 X)))) (MBE :LOGIC (IF (ZP X) 1 (* X (F (- X 1)))) :EXEC (IF (= X 0) 1 (* X (F (- X 1)))))) Logically this is the same as using the :logic argument of mbe. (DEFUN F (X) (IF (ZP X) 1 (* X (F (- X 1))))) But the effect is that when the guard holds, the :exec argument of mbe is used, as though f were defined as follows in raw Lisp. (DEFUN F (X) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (<= 0 X) ))) (IF (= X 0) 1 (* X (F (- X 1))))) The above example is trivial, but Dave Greve and Matt Wilding will show a more serious application in a talk tomorrow. Jose Luis Ruiz Reyna has also used mbe to advantage, and with minimal consultation from us, Sandip Ray has produced a macro built on defpun that allows execution of partial functions. With Jose Luis we have developed a defexec macro built on mbe but requiring a proof of termination of the executable function. For example, if DEFUN is replaed by DEFEXEC above to produce (DEFEXEC F (X) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (<= 0 X) ))) (MBE :LOGIC (IF (ZP X) 1 (* X (F (- X 1)))) :EXEC (IF (= X 0) 1 (* X (F (- X 1)))))) then in addition to the defun above, a termination proof will be done for the following locally-defined (but thrown away) function: (DEFUN F (X) (IF (AND (INTEGERP X) (<= 0 X)) (IF (= X 0) 1 (* X (F (- X 1)))) NIL)) Thanks to Vernon Austel for a key observation leading to mbe. Rewrite stack overflows are now handled gracefully using a new ``rewrite-stack-limit.'' The user can now control multiple matching for free variables in hypotheses for :forward-chaining rules, as has already been supported for :rewrite and :linear rules. Thanks to Erik Reeber for doing an implementation and providing signifcant help with the documentation. It is no longer necessary to specify (set-match-free-error nil) in order to avoid free variable errors. The form (break-on-error) causes, at least for most Lisps, entry into the Lisp debugger whenever ACL2 causes an error. A new table has been provided so that advanced users can override the built-in untranslate functionality. The pstack mechanism (formerly denoted checkpoints) has been improved. The "process [prover] stack," or pstack, is automatically printed when proofs abort. Evaluation of function calls on explicit arguments during proofs is now tracked. Actual parameters are shown with (pstack t) rather than formals. =============================================================================== NOTE-2-8-BUG-FIXES Fixes have been made for two soundness bugs that can occur when using the proof-checker (expansion of a call of a constrained function with a :definition rule, and inappropriate use of if-term governors for "deriving" contradictions using s and related commands). Another soundness bug could be provoked in some Lisps by applying defpkg to the empty string. This has been disallowed. Misc. other smaller (non-soundness) bugs have been fixed, e.g., avoiding multiple loads of compiled files, and adding the reporting induction rules. =============================================================================== NOTE-2-8-OTHER ACL2 Version 2.8 Notes on Miscellaneous Changes Execution of table events has been sped up by avoiding excessive consing. =============================================================================== NOTE-2-8-PROOF-CHECKER ACL2 Version 2.8 Notes on Proof-checker Changes Added new proof-checker commands wrap (etc.) to create a single new goal. Fixed a bug in the = command when a governing IF-test of the current term is T. =============================================================================== NOTE-2-8-PROOFS ACL2 Version 2.8 Notes on Changes in Proof Engine During the computation of constraints for functional instantiation, (prog2$ term1 term2) and (the type term2) are now treated as term2. An improvement has been made in heuristics for controlling rewriting during proofs by induction. =============================================================================== NOTE-2-8-RULES ACL2 Version 2.8 Notes on Changes in Rules and Constants The theory minimal-theory has been changed by adding the definition rune for mv-nth to the theory. =============================================================================== NOTE-2-8-SYSTEM ACL2 Version 2.8 Notes on System-level Changes ACL2 now runs on OpenMCL, "an opensourced Common Lisp implementation, derived from Digitool's Macintosh Common Lisp product." Thanks to Greg Wright and Robert Krug for doing most of the work for this port. =============================================================================== =============================================================================== NOTE-2-7 ACL2 Version 2.7 (November, 2002) Notes The Version 2.7 notes are divided into the subtopics below. Here we give only a brief summary of a few of the changes that seem most likely to impact existing proofs. Not included in this brief summary, but included in the subtopics, are descriptions of improvements (including bug fixes and new functionality) that should not get in the way of existing proof efforts. In particular, please see *Note NOTE-2-7-NEW-FUNCTIONALITY:: for discussion of a number of new features that you may find useful. Acknowledgements and elaboration, as well as other changes, can be found in the subtopics listed below. o New functionality (see *Note NOTE-2-7-NEW-FUNCTIONALITY::): + ACL2 now works harder to apply :rewrite and :linear rules with free variables in the hypotheses. See *Note NOTE-2-7-NEW-FUNCTIONALITY::, in particular its first two paragraphs, for details. Forward-chaining also does more with free variables. + A new macro, bind-free, provides a simple way to get much or most of the power of metafunctions. Thanks to Eric Smith for coming up with the idea and to Robert Krug for providing an initial implementation. + Lots of other stuff: minimal-theory, e/d (``enable/disable''), defund and defthmd, new books (especially, ordinals from Manolios/Vroon as discussed earlier today), :expand :lambdas, monitoring of simple rules, (certify-book "foo" ?), and others. o Bug fixes (see *Note NOTE-2-7-BUG-FIXES::): + Three soundness bugs were fixed. These bugs were probably rarely hit, so users may well not notice these changes. + Certify-book now requires :skip-proofs-ok t (respectively, :defaxioms-okp t) if there are skip-proofs (respectively, defaxiom) events in the book or any included sub-books. + When :by hints refer to a definition, they now use the original body of that definition rather than the simplfied ("normalized") body. + When ld is applied to a stringp file name, it now temporarily sets the connected book directory (see *Note CBD::) to the directory of that file while evaluating forms in that file. o Changes in proof engine (see *Note NOTE-2-7-PROOFS::): + Some prover heuristics have changed slightly. Among other consequences, this can cause subgoal hints to change. For example, suppose that the Version_2.6 proof of a particular theorem generated "Subgoal 2" and "Subgoal 1" while Version_2.7 only generates the second of these. Then a subgoal hint attached to "Subgoal 1" in Version_2.6 would have to be attached to "Goal'" in Version_2.7. (See *Note GOAL-SPEC::.) The full topic has details (see *Note NOTE-2-7-PROOFS::). o Changes in rules and definitions (see *Note NOTE-2-7-RULES::): + The package name of a generated variable has changed for defcong. o Guard-related changes (see *Note NOTE-2-7-GUARDS::): + Guard verification formerly succeeded in a few cases where it should have failed. + Guards generated from type declarations now use functions signed-byte-p and unsigned-byte-p, now defined in source file axioms.lisp and formerly defined rather similarly under books/ihs/. o Proof-checker changes (see *Note NOTE-2-7-PROOF-CHECKER::): + See the above doc topic. o System-level changes (see *Note NOTE-2-7-SYSTEM::): + See the above doc topic. o Other changes (see *Note NOTE-2-7-OTHER::): + A new table, invisible-fns-table, takes the place of the handling of invisible functions in the acl2-defaults-table, + The theory-invariant event has been modified so that the default action is an error rather than a warning. + Proof output that reports destructor elimination no longer uses the word "generalizing".