Note-2-6-system
ACL2 Version 2.6 Notes on System-level Changes
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. 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.
