NOTE-2-6-SYSTEM

ACL2 Version 2.6 Notes on System-level Changes
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, 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.