Acl2 Version 1.6 Notes
A new key has been implemented for the ACL2-defaults-table,
:ignore-ok. See set-ignore-ok.
It is now legal to have color events, such as (red), in the
portcullis of a book. More generally, it is legal to set the ACL2-defaults-table in the portcullis of a book. For example, if you
execute :red and then certify a book, the event (red) will show up
in the portcullis of that book, and hence the definitions in that book
will all be red (except when overridden by appropriate declarations or events). When that book is included, then as always, its portcullis
must first be ``raised,'' and that will cause the default color to become red
before the events in the book are executed. As always, the value of
ACL2-defaults-table immediately after execution of an include-book, certify-book, or encapsulate form will be the
same as it was immediately before execution (and hence, so will the default
color). See portcullis and, for more about books, see books.
A theory ground-zero has been defined to contain exactly those
rules that are enabled when Acl2 starts up. See ground-zero.
The function nth is now enabled, correcting an oversight
from Version 1.5.
Customization files no longer need to meet the syntactic restrictions put
on books; rather, they can contain arbitrary Acl2 forms. See ACL2-customization.
Structured directory names and structured file names are supported; see
especially the documentation for pathname, book-name, and cbd.
Acl2 now works with some Common Lisp implementations other than akcl,
including Lucid, Allegro, and MCL.
A facility has been added for displaying proof trees, especially using
emacs; see proof-tree.
There is a considerable amount of new documentation, in particular
for the printing functions fmt, fmt1, and fms, and for
the notion of Acl2 term (see term).
It is possible to introduce new well-founded relations, to specify which
relation should be used by defun, and to set a default relation. See
It is possible to make functions suggest new inductions. See induction.
It is possible to change how Acl2 expresses type-set information; in
particular, this affects what clauses are proved when forced
assumptions are generated. See type-set-inverter.
A new restriction has been added to defpkg, having to do with
undoing. If you undo a defpkg and define the same package name again,
the imports list must be identical to the previous imports or else an
explanatory error will occur. See package-reincarnation-import-restrictions.
Theory-invariant and set-irrelevant-formals-ok are now
embedded event forms.
The command :good-bye may now be used to quit entirely out of
Lisp, thus losing your work forever. This command works in akcl but may not
work in every Common Lisp.
A theory ground-zero has been added that contains exactly the enabled rules in the startup theory. See ground-zero.
Define-pc-macro and define-pc-atomic-macro now automatically
define :red functions. (It used to be necessary, in general, to change
color to :red before invoking these.)
For a proof of the well-foundedness of e0-ord-< on the
e0-ordinalps, see proof-of-well-foundedness. [Note added later:
Starting with Version_2.8, o< and o-p replace e0-ord-<
and e0-ordinalp, respectively.]
Free variables are now handled properly for hypotheses of :type-prescription rules.
When the system is loaded or saved, state is now bound to
Certify-book has been modified so that when it compiles a file, it
loads that object file.
Defstub has been modified so that it works when the color is hot
(:red or :pink).
Several basic, but not particularly commonly used, events have been
added or changed. The obscure axiom symbol-name-intern has been
modified. The definition of firstn has been changed. Butlast is
now defined. The definition of integer-length has been modified. The
left-hand side of the rewrite rule rational-implies2 has been changed
from (* (numerator x) (/ (denominator x))) to (* (/ (denominator x))
(numerator x)), in order to respect the fact that unary-/ is
invisible with respect to binary-*. See loop-stopper.
The `preprocess' process in the waterfall (see hints for a
discussion of the :do-not hint) has been changed so that it works to
avoid case-splitting. The `simplify' process refuses to force (see force) when there are if terms, including and and or
terms, in the goal being simplified.
The function apply is no longer introduced automatically by
translation of user input to internal form when functions are called on
inappropriate explicit values, e.g., (car 3).
The choice of which variable to use as the measured variable in a recursive
definition has been very slightly changed.