ACL2 Version 2.6 Notes on New Functionality
A fundamental change is the provision of the ``nu-rewriter'' for
simplifying expressions composed of
A new flag has been added to the
A new flag has been added to permit the system to abbreviate output by
A ``raw mode'' has been added, primarily for faster loading of applications. see set-raw-mode.
Functions alphorder and lexorder have been put in
The ACL2 user can now make system calls to the host operating system. See sys-call and see sys-call-status. Thanks to Rob Sumners for working out this idea with Pete Manolios and Robert Krug, who we also thank, and for working out the implementation with us.
It is no longer required to use absolute pathnames in include-book forms that have been executed before a certify-book. Any relative pathname strings in such contexts will be expanded into absolute pathnames before they are saved in the portcullis of the certificate of the book being certified.
ACL2 can now be built on top of Allegro Common Lisp 6.0, and also on Windows platforms on top of Allegro Common Lisp and GCL. Thanks to Pete Manolios and Vinay K. Siddhavanahalli for their help with Windows.
Rob Sumners has designed and provided an initial implementation for two improvements to defstobj (also see stobj). First, array fields can now be resized. Resize and length functions are provided for array fields, which can be used to resize stobj array fields dynamically. The recognizers for array fields have been simplified to accommodate this change, so that they only check that each element of the array field has the specified type. Second, performance has been improved for stobjs with a large number of fields, by changing their Common Lisp implementation to store the fields in a simple vector instead of a list.
Now stobjs may be bound locally; see with-local-stobj. Thanks to Rob Sumners, who encouraged us to implement this capability, was an early user of it, and participated usefully in discussions on its design.
New functions fms!, fmt!, and fmt1! are the same as
their respective functions without the ``
The documentation has been improved. In particular, a new documentation topic provides a gentle introduction to ACL2 arrays — see arrays-example — and additional documentation has been provided for getting started with proof trees in emacs — see proof-tree.
New Makefile targets
make fasl ACL2=my-allegro-acl2
which will create compiled (
The user may now control backchaining. This feature was designed and primarily implemented by Robert Krug (though the authors of ACL2 are responsible for any errors); thanks, Robert! See backchain-limit.
It is now possible to ``slow down'' the rate at which case splits are generated by the simplifier. See set-case-split-limitations.
(defstobj foo a b :renaming ((b c)))
then the term
Computed hints have been improved. It is now possible to detect within a computed hint whether the goal clause is stable under simplification; it is also possible for a computed hint to change the list of available hints. See computed-hints.
It is now possible to provide ``default hints'' that are appended to the hints explicitly provided. See set-default-hints.
Using computed hints (see computed-hints) and default hints (see
set-default-hints) it is possible to implement a book that supports
``priority phased simplification.'' Using this book you can assign priorities
to your rules and cause the theorem prover to simplify each goal maximally
under all the rules of one priority before enabling rules of the next
The macro defabbrev has been improved to allow declare forms and documentation strings and to do more error-checking. Thanks to Rob Sumners for designing this enhancement and providing the first implementation. See defabbrev.
Further changes were made to support CMU Lisp. Wolfhard Buss helped with these changes.
A new table was added that is used when printing proof output, so that nests of right-associated calls of a binary function are replaced by corresponding macro calls, as has been the case for binary-+ and +, binary-append and append, and so on. See add-binop.
Operators logand, logior, logxor, and logeqv are now macros (formerly, they were functions) that call corresponding
binary functions (e.g.,
ACL2 now runs under
Michael ``Bogo'' Bogomolny has created a search engine, accessible from the ACL2 home page. For that purpose he modified the HTML translator to create one file per topic (a good idea in any case). Thanks, Bogo!
An emacs file of potential (but optional) use for ACL2 users may be found
Some books have been added or modified. In particular, Robert Krug