Major Section: NOTE-2-6
We modified the tracking of skip-proofs events and the use of
state global ld-skip-proofsp in order to avoid some soundness
issues. For example, skip-proofs events buried in locally-included
books are now tracked. The ``Essay on Skip-proofs'' in source file
axioms.lisp gives several examples of dicey behavior that is no
longer supported.
We fixed a problem with some of the makefiles, so that recursive invocations
of make now use the version of make specified on the command line.
Files were fixed to help non-Unix/Linux users with book
certification. Thanks to John Cowles for finding some problems
and suggesting fixes to books/certify-numbers.lisp,
books/arithmetic/certify.lsp, and books/cowles/certify.lsp.
We thank Scott Burson for noticing and fixing some other such
problems. Moreover, a bdd test was being ignored entirely in
Version 2.5; this problem has been fixed as well.
A minor change in system function save-acl2-in-allegro will allow this function to continue to work in Allegro CL versions starting (someday) with 10.0. Thanks to Art Flatau for suggesting such a fix.
The books/case-studies/ directory has been removed. These books are
in support of the first (1998) ACL2 workshop, and are accessible via the
ACL2 home page on the Web at
http://www.cs.utexas.edu/users/moore/acl2/. Also, the
books/cli-misc directory has been renamed books/misc, and the
books/nqthm directory has been removed.
The notion of ACL2 version has been slightly modified to catch
unsoundness due to implementation dependencies. See version.
Another change to eliminate such unsoundness is that built-in
symbols now have a symbol-package-name of "COMMON-LISP"; formerly,
this string was "LISP" for ACL2 images built on GCL.
See symbol-package-name. At a low level, the (undocumented) constant
*main-lisp-package-name* is now "COMMON-LISP"; before, it was
"LISP" for GCL.