ACL2 Version 2.6 Notes on Other (Minor) Changes
Warning strings are now case-insensitive. See set-inhibit-warnings.
A minor modification has been made to defstobj that can have a positive impact on performance in Allegro Common Lisp. (For Lisp hackers: the stobj name was formerly declared special, and that was disabling Allegro's tail-merging routing for compilation of some recursive functions using stobjs.) The downside is that stobj names can no longer be evaluated in raw Lisp. However, raw Lisp is not the right place to be evaluating ACL2 forms anyhow; see set-raw-mode. We thank Rob Sumners for bringing this issue to our attention.
Before Version 2.6, there has been the following problem with defstub and encapsulate in the case that the current package is not
the ACL2 package. If a signature was specified using the symbol
Bugs in defun-sk have been fixed.
The trace mechanism has been fixed to handle stobjs, and to avoid the printing of so-called enabled structures.
The brr command
An include-book of an uncertified book no longer loads an associated compiled file.
We added a few checks to make sure that the underlying lisp is suitable, for example checking that the reader is case-insensitive and reads in symbols with upper-case names where appropriate.
We now warn when forcing (see force) or immediate force mode (see immediate-force-modep) change state between enabled and disabled. Also see enable-immediate-force-modep and see disable-immediate-force-modep for information about these new macros, which may be used to control immediate force mode.
We have eliminated the use of a low-level raw Lisp constant,
Fixnum declarations are now realized as
A new documentation topic functional-instantiation-example illustrates functional instantiation.
A bug has been fixed in the monitoring of runes (see monitor). Thanks to Dave Greve for sending an example that clearly showed the problem.
A warning is now issued when it is detected that a
An error is caused for rules of class
A minor bug has been fixed in
A minor hole in
Previously, the Allegro compiler was not eliminating tail recursion for executable counterparts of functions, because of the way one of its flags had been set. As a result, calls of functions whose guards had not been verified could run out of stack space when this was not necessary. This situation has been fixed.
Executable counterparts could have slow array accesses. This has been fixed (specifically, constants are no longer replaced with their values in the definitions of executable counterparts).
Various improvements have been made to the documentation. Thanks in particular to Eric Smith for pointing out a numbers of places where fixes were in order.
File "mcl-acl2-startup.lisp" has been updated, thanks to feedback from Philippe Georgelin.
Inefficiencies in GCL fixnum computations were remedied for macros