Acl2 Version 1.4 Notes
Once again ld only takes one required argument, as the
Three commands have been added in the spirit of
Book naming conventions have been changed somewhat. The once-required
A table exists for controlling whether Acl2 prints comments when it
forces hypotheses of rules; see
We have improved the way we report rules used by the simplifier. All runes of the same type are reported together in the running commentary associated with each goal, so that for example, executable-counterparts are listed separately from definitions, and rewrite rules are listed separately from linear rules. The preprocessor now mentions ``simple'' rules; see simple.
The mechanism for printing warning messages for new rewrite rules, related
to subsumption, now avoids worrying about nonrecursive function symbols when
those symbols are disabled. These messages have also been eliminated
for the case where the old rule is a
Backquote has been modified so that it can usually provide predictable results when used on the left side of a rewrite rule.
Time statistics are now printed even when an event fails.
The Acl2 trace package has been modified so that it prints using the values
of the Lisp globals
We have relaxed the translation rules for
The loop-stopper test has been relaxed. The old test required that every new argument be strictly less than the corresponding old argument in a certain term-order. The new test uses a lexicographic order on term lists instead. For example, consider the following rewrite rule.
(equal (variable-update var1 val1 (variable-update var2 val2 vs)) (variable-update var2 val2 (variable-update var1 val1 vs)))
This rule is permutative. Now imagine that we want to apply this rule to the term
(variable-update u y (variable-update u x vs)).
Since the actual corresponding to both
Messages about events now contain a space after certain left parentheses, in order to assist emacs users. For example, the event
leads to a summary containing the line
Form: ( DEFTHM ABC ...)
and hence, if you search backwards for ``
More tautology checking is done during a proof; in fact, no goal printed to
the screen, except for the results of applying
Warning messages are printed with short summary strings, for example the
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE the formula of an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE FOO) in the hint provided for Goal. See :DOC using- enabled-rules.
At the end of the event, just before the time is printed, all such summary strings are printed out.
Some irrelevant formals are detected; see irrelevant-formals.
A bug in the application of metafunctions was fixed: now if the output of a metafunction is equal to its input, the application of the metafunction is deemed unsuccessful and the next metafunction is tried.
A documentation section called proof-builder has been added for the interactive facility, whose documentation has been slightly improved. See in particular the documentation for proof-builder, verify, and macro-command.