Acl2 Version 1.5 Notes
Acl2 now allows ``complex rationals,'' which are complex numbers whose real parts are rationals and whose imaginary parts are non-zero rationals. See complex.
A new way of handling forced hypotheses has been implemented.
Rather than cause a case split at the time the force occurs, we
complete the main proof and then embark on one or more ``forcing rounds'' in
which we try to prove the forced hypotheses. See forcing-round.
To allow us to compare the new handling of force with the old, Version
1.5 implements both and uses a flag in state to determine which method
should be used. Do
(thm (implies (and (true-listp a) (true-listp b)) (equal (append (append a b) c) (append a (append b c)))))
Include-book and encapsulate now restore the ACL2-defaults-table when they complete. See include-book and see encapsulate.
The guards on many Acl2 primitives defined in
It is possible to attach heuristic filters to
A tutorial has been added (but as of Version_3.6.1 it has become obsolete).
Events now print the Summary paragraph listing runes used,
time, etc., whether they succeed or fail. The format of the ``failure
banner'' has been changed but still has multiple asterisks in it.
A new event form skip-proofs has been added; see skip-proofs.
A user-specific customization facility has been added in the form of a book that is automatically included, if it exists on the current directory. See ACL2-customization.
A facility for conditional metalemmas has been implemented; see meta.
The acceptable values for ld-skip-proofsp have changed. In the old
version (Version 1.4), a value of
In order to turn off the forcing of assumptions, one should now disable the
The macros enable-forcing and disable-forcing make it convenient to enable or disable forcing. See enable-forcing and see disable-forcing.
The new commands
The new history commands
Theory expressions now are allowed to use the free variable world and prohibited from using the free variable state. See theories, although it is essentially the same as before except it mentions world instead of state. See world for a discussion of the Acl2 logical world. Allowing in-theory events to be state-sensitive violated an important invariant about how books behaved.
Table keys and values now are allowed to use the free variable world and prohibited from using the free variable state. See the note above about theory expressions for some explanation.
The macro for minus, -, used to expand
A new class of rule,
A new class of rule,
The new command pcb! is like pcb but sketches the command and then prints its subsidiary events in full. See pcb!.
The rules for how loop-stoppers control permutative rewrite rules
have been changed. One effect of this change is that now when the built-in
commutativity rules for + are used, the terms
Extensive documentation has been provided on the topic of Acl2's ``term ordering.'' See term-order.
Calls of ld now default ld-error-action to
The command descriptor
The command descriptor
The order of the arguments to defcong has been changed.
The simplifier now reports the use of unspecified built-in type information about the primitives with the phrase ``primitive type reasoning.'' This phrase may sometimes occur in situations where ``propositional calculus'' was formerly credited with the proof.
The function pairlis has been replaced in the code by a new function pairlis$, because Common Lisp does not adequately specify its pairlis function.
Some new Common Lisp functions have been added, including logtest,
logcount, integer-length, make-list, remove-duplicates, string, and concatenate. The source file
The functions defuns and theory-invariant have been documented. See defuns and see theory-invariant.
A few symbols have been added to the list
A new key has been implemented for the ACL2-defaults-table,
The connected book directory, cbd, must be nonempty and begin and end with a slash. It is set (and displayed) automatically upon your first entry to lp. You may change the setting with set-cbd. See cbd.
Documentation has been written about the ordinals. See :DOC
The color events — (red), (pink), (blue), and (gold) — may no longer be enclosed inside calls of local, for soundness reasons. In fact, neither may any event that sets the ACL2-defaults-table. See embedded-event-form.
See ld-keyword-aliases for an example of how to change the exit
The attempt to install a monitor on
A new message is sometimes printed by the theorem prover, indicating that a given simplification is ``specious'' because the subgoals it produces include the input goal. In Version 1.4 this was detected but not reported, causing behavior some users found bizarre. See specious-simplification.
A warning is printed if a macro form with keyword arguments is given
duplicate keyword values. Execute
A new restriction has been placed on encapsulate. Non-local recursive definitions inside the encapsulate may not use, in their tests and recursive calls, the constrained functions introduced by the encapsulate. See subversive-recursions. (Note added in Version 2.3: Subversive recursions were first recognized by us here in Version 1.5, but our code for recognizing them was faulty and the bug was not fixed until Version 2.3.)
The events defequiv, defcong, defrefinement, and defevaluator have been reimplemented so that they are just macros that expand into appropriate defthm or encapsulate events; they are no longer primitive events. See the documentation of each affected event.
Error reporting has been improved for inappropriate in-theory hints and events, and for syntax errors in rule classes, and for non-existent filename arguments to ld.
Technical Note: We now maintain the Third Invariant on