Major Section: RELEASE-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
(assign old-style-forcing t) if you want
force to be handled
as it was in Version 1.4. However, we expect to eliminate the
old-style forcing eventually because we think the new style is more
effective. To see the difference between the two approaches to
forcing, try proving the associativity of append under both settings
old-style-forcing. To get the new behavior invoke:
(thm (implies (and (true-listp a) (true-listp b)) (equal (append (append a b) c) (append a (append b c)))))Then
(assign old-style-forcing t)and invoke the
thmcommand above again.
:cases hints allows proof by cases. See hints.
encapsulate now restore the
when they complete. See include-book and see encapsulate.
The guards on many Acl2 primitives defined in
axioms.lisp have been
weakened to permit them to be used in accordance with lisp custom
It is possible to attach heuristic filters to
rewrite rules to
limit their applicability. See syntaxp.
A tutorial has been added; see acl2-tutorial.
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.
Thm also prints a Summary, whether it succeeds or fails; but
not an event.
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
t meant that proofs and
events are to be skipped. In Version 1.5, a value of
t means proofs
local events) are to be skipped. A value of
means proofs and
local events are to be skipped. There are two
other, more obscure, acceptable values. See ld-skip-proofsp.
In order to turn off the forcing of assumptions, one should now
force (rather than the
force, as in the previous release); see force.
disable-forcing make it convenient to
enable or disable forcing. See enable-forcing and
The new commands
pr! print the rules created by an event or
command. See pr and see pr!.
The new history commands
puff* will replace a compound
command such as an
include-book by the sequence of
events in it. That is, they ``puff up'' or ``lift'' the subevents
of a command to the command level, eliminating the formerly superior
command and lengthening the history. This is useful if you want to
``partially undo'' an
encapsulate or book or other compound command
so you can experiment. See puff and see puff*.
Theory expressions now are allowed to use the free variable
and prohibited from using the free variable
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
Table keys and values now are allowed to use the free variable
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
(- x 3) to
(+ x -3) and now
expands it to
(+ -3 x) instead. The old macro, if used in the
left-hand sides of rewrite rules, produced inapplicable rules
because the constant occurs in the second argument of the
potential target terms generally had the constant in the first
argument position because of the effect of
A new class of rule,
:linear-alias rules, allows one to implement
the nqthm package and similar hacks in which a disabled function is
to be known equivalent to an arithmetic function.
A new class of rule,
:built-in-clause rules, allows one to extend
the set of clauses proved silently by
defun during measure and guard
processing. See built-in-clauses.
The new command
pcb! is like
pcb but sketches the command and then
prints its subsidiary events in full. See pcb!.
Rewrite class rules may now specify the
See rule-classes and see loop-stopper.
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
are permuted into adjacency. For example,
(+ a b (- a)) is now
normalized by the commutativity rules to
(+ a (- a) b); in Version
b was considered syntactically smaller than
(- a) and so
(+ a b (- a)) is considered to be in normal form. Now it is
possible to arrange for unary functions be be considered
``invisible'' when they are used in certain contexts. By default,
unary-- is considered invisible when its application appears in
the argument list of
binary-+. See loop-stopper and
see :DOC set-invisible-fns-table.
Extensive documentation has been provided on the topic of Acl2's ``term ordering.'' See term-order.
ld now default
:return rather than to
the current setting.
The command descriptor
:x has been introduced and is synonymous with
max, the most recently executed command. History commands such as
pbt print a
:x beside the most recent command, simply to indicate
that it is the most recent one.
The command descriptor
:x-23 is synonymous with
(:x -23). More
generally, every symbol in the keyword package whose first character
#\x and whose remaining characters parse as a negative integer
is appropriately understood. This allows
(:max -10) or
(:here -10) were previously used. The old forms
are still legal.
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.
pairlis has been replaced in the code by a new function
pairlis$, because Common Lisp does not adequately specify its
Some new Common Lisp functions have been added, including
concatenate. The source file
/slocal/src/acl2/axioms.lisp is the
ultimate reference regarding Common Lisp functions in Acl2.
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
:irrelevant-formals-ok. See set-irrelevant-formals-ok.
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
oops will undo the last
ubt. See oops.
Documentation has been written about the ordinals. See e0-ordinalp and see e0-ord-<.
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
See ld-keyword-aliases for an example of how to change the exit
q to something else.
The attempt to install a monitor on
rewrite rules stored as simple
abbreviations now causes an error because the application of
abbreviations is not tracked.
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.
Definition rules are no longer always required to specify the
:controller-alist fields; those fields can be defaulted
to system-determined values in many common instances.
A warning is printed if a macro form with keyword arguments is given
duplicate keyword values. Execute
(thm t :doc nil :doc "ignored")
and read the warning printed.
A new restriction has been placed on
recursive definitions inside the
encapsulate may not use, in their
tests and recursive calls, the constrained functions introduced by
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.)
been reimplemented so that they are just macros that expand into
encapsulate events; they are no longer
primitive events. See the documentation of each affected event.
defcor event, which was a shorthand for a
established a corollary of a named, previously proved event, has
been eliminated because its implementation relied on a technique we
have decided to ban from our code. If you want the effect of a
defcor in Version 1.5 you must submit the corresponding
:by hint naming the previously proved event.
Error reporting has been improved for inappropriate
and events, and for syntax errors in rule classes, and for
non-existent filename arguments to
Technical Note: We now maintain the Third Invariant on
as described in the Essay on the Invariants on Type-alists, and
Canonicality. This change will affect some proofs, for example, by
causing a to rewrite more quickly to
(equiv a b) and
(equiv b c) are both known and
c is the canonical
representative of the three.