Major Section: NOTE-2-6
Warning strings are now case-insensitive. See set-inhibit-warnings.
ACL2 causes a warning when an in-theory hint or event causes a 0-ary
function's definition to be disabled but its :executable-counterpart
to be enabled.
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 =>,
then that symbol had have been imported into the current package
from the ACL2 package when the current package was defined. There
are no longer any package restrictions on the use of =>. Thanks to
John Cowles for bringing this problem to our attention.
Bugs in defun-sk have been fixed. Defun-sk forms introducing
functions of no arguments were failing to be admitted, for example:
(defun-sk always-p1 () (forall (x) (p1 x))).
Thanks to John Cowles for bringing this problem to our attention.
Also, defun-sk failed on an example in the documentation
(see tutorial4-defun-sk-example), as pointed out by Matyas
Sustik; this bug has been fixed as well.
The trace mechanism has been fixed to handle stobjs, and to avoid the printing of so-called enabled structures.
The brr command :type-alist now produces more readable output.
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,
*most-recent-multiplicity*. Our test suite saw a speed-up
of approximately 2% as a result for an ACL2 image built on GCL
(but no significant speed-up for an ACL2 image built on Allegro
Common Lisp). We thank Rob Sumners for suggesting this improvement.
Fixnum declarations are now realized as (signed-byte 29) instead of
(signed-byte 27). We check that the underlying Common Lisp
recognizes objects of type (signed-byte 29) as fixnums, with
the exception of CLISP, which is said to have an efficient bignum
implementation.
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
:type-prescription rule may not be as strong as it appears because
it is not sufficient to prove itself by type reasoning.
An error is caused for rules of class :meta when the function symbol
IF is among the :trigger-fns. (IF was ignored anyhow; the point of
this change is to avoid misleading the user.)
A minor bug has been fixed in :pr, evident for example if this
command was applied to IF.
A minor hole in :set-bogus-mutual-recursion-ok did not permit the
acceptance of mutual-recursion forms that include constant function
definitions. This has been fixed. Thanks to Eric Smith for coming
up with a simple example illustrating the problem.
The temporary files "TMP.lisp" and "TMP1.lisp" written out by :comp
are now written to the connected book directory (see cbd).
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 +f and
*f. Thanks to Rob Sumners for pointing out this issue.