Note-2-8-new-functionality
ACL2 Version 2.8 Notes on New Functionality
WARNING: You may find that control-d (in emacs, control-c
control-d) can throw you completely out of Lisp where it had not formerly
done so.
(CLISP and Allegro CL only) ACL2 now starts up inside the ACL2 loop —
that is, (lp) is executed automatically — when built
on CLISP or Allegro CL. This was already the case for GCL and CMUCL, and it
still is not true for LispWorks. Thanks to Joe Corneli for bringing the CLISP
command-line option "-i" to our attention, which led to this CLISP
change and inspired reconsideration of how to do this for Allegro CL.
Pete Manolios and Daron Vroon have changed the representation of ordinals
in ACL2, defined algorithms for ordinal arithmetic, and created a library of
theorems to reason about ordinal arithmetic. We thank them for these nice
contributions. See note-2-8-ordinals for details, in particular, for
how to preserve existing proofs that depend on the previous ordinal
representation.
Sometimes users create rules of class :rewrite that cause an
infinite loop in the ACL2 rewriter. This has lead to Lisp stack overflows and
even segmentation faults. Now, the depth of calls of functions in the ACL2
rewriter is limited, and under user control. See rewrite-stack-limit.
Macros mbe (``must be equal'') and mbt (``must be true'')
have been introduced, which allow the user to attach fast executable
definitions to (presumably slower) :logic mode functions. Thanks
to Vernon Austel for a key idea. Also provided is a macro defexec,
which employs mbe but enforces the requirement that the executable
definition also terminates. Thanks to Jose Luis Ruiz Reina for collaborating
in the design and development of defexec, and for useful comments from
a number of others as well in the development of mbe including Joe
Hendrix and Rob Sumners.
Definitions have been added for functions rassoc-eq and rassoc-equal, which are like rassoc but use different tests and have
different guards. (Compare assoc-eq and assoc-equal, which
are in similar relation to assoc.)
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. For
:forward-chaining rules, ``free variables'' are those in the hypotheses
not bound by a given trigger term. As for :rewrite and :linear
rules, free-variable matching may be limited to the first successful attempt
by specifying :match-free :once with :forward-chaining in the
:rule-classes, and add-match-free-override may be used to
modify the behavior of an existing rule. Thanks to Erik Reeber for most of
the implementation of these new capabilities, as well as significant
assistance with a corresponding new documentation topic (see free-variables-examples-forward-chaining).
It is no longer necessary to specify (set-match-free-error nil) in
order to avoid errors when a rule with free variables in its hypotheses is
missing the :match-free field. (This was already true during book
certification, but now it is the case in interactive sessions as well.)
The form (break-on-error) causes, at least for most Lisps, entry into
the Lisp debugger whenever ACL2 causes an error. See break-on-error.
Thanks to John Erickson for providing encouragement to provide this
feature.
A new table has been provided so that advanced users can override
the built-in untranslate functionality. See user-defined-functions-table.
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. Thanks to Bill Legato for suggesting the first two of
these improvements and, in general, encouraging changes that make ACL2 easier
to use.
The defstobj event is now allowed to take an :inline argument,
which can speed up execution. Thanks to Rob Sumners for suggesting and
implementing this new feature.
Macro assert$ has been added in order to make it easy to write
assertions in one's code. Semantically, (assert$ test form) is the same
as form, but it causes a hard error (using illegal) if test
evaluates to nil.
Macro cw-gstack no longer takes arguments for the gstack or state. However, it now takes a keyword argument (which is optional),
:evisc-tuple, that can be used to control how it prints terms. In
particular, cw-gstack abbreviates large terms by default, but
(cw-gstack :evisc-tuple nil) causes terms to be printed in full. Thanks
to Robert Krug and Eric Smith for requesting this improvement.
The advanced user now has more control over the evisceration of terms. See
ld-evisc-tuple, in particular the new paragraph on ``The printing of
error messages and warnings.''
The include-book event now has an additional (optional) keyword,
:dir. The value of :dir should be a keyword that is associated with
an absolute directory pathname to be used in place of the current book
directory (see cbd) for resolving the first argument of
include-book to an absolute pathname. At start-up, the only such keyword
is :system, so that for example (include-book "arithmetic/top" :dir
:system) will include the book "arithmetic/top" under the
"books/" directory of your ACL2 installation. But you can associate
``projects'' with keywords using add-include-book-dir, e.g.,
(add-include-book-dir :my-project "/u/smith/project0/"). See add-include-book-dir and also see delete-include-book-dir and see
include-book. Note: You will probably not find :dir :system to be
useful if the distributed books are not placed in the path of their original
location, pointed to by :dir :system, which will often happen if the
executable image is obtained from another site. Also see include-book,
in particular its ``soundness warning''.
The printing of results in raw mode (see set-raw-mode) may now be
partially controlled by the user: see add-raw-arity. [Note added 2021:
this utility has been removed and is no longer necessary.] Also, newlines are
printed when necessary before the value is printed.
For those using Unix/Linux `make': A cert.acl2 file can contain forms
to be evaluated before an appropriate certify-book command is invoked
automatically (not included in cert.acl2).
Jared Davis has contributed a new set of books for ordered finite set
theory to the standard distribution, books/finite-set-theory/osets-0.81/.
See the README file in that directory. Thanks, Jared.
Robert Krug has contributed two related changes (thanks, Robert!) in
support of stronger arithmetic reasoning. First, one can now enable and
disable nonlinear arithmetic with a :nonlinearp hint, which will override
the default provided by set-non-linearp (initially, nil). See
hints. Second, computed-hints can now have access to the
HISTORY, PSPV, and CTX variables of the waterfall, which (for
example) allows the writing of a hint which will enable nonlinear arithmetic
on precisely those goals that are stable-under-simplificationp. See
computed-hints.
Robert Krug has contributed a new set of arithmetic books to the standard
distribution, books/arithmetic-3/. See the README file in that
directory. Thanks, Robert.