NOTE-2-9-2

Major Section:  RELEASE-NOTES

Also see note-2-9-1 for other changes since the last non-incremental release (Version_2.9).

There was a bug in non-linear arithmetic (see non-linear-arithmetic) that caused the following error:

ACL2 !>(include-book "rtl/rel4/lib/top" :dir :system)
....
ACL2 !>(set-non-linearp t)
 T
ACL2 !>(thm
 (implies (and (bvecp a 77)
               (bvecp b 50))
          (bvecp (fl (/ (* a b) (expt 2 23)))
                 104))
 :hints (("Goal" :in-theory (enable bvecp))))

[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

By the simple :definition BVECP, the :executable-counterparts of EXPT
and UNARY-/ and the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce
the conjecture to

Goal'
(IMPLIES (AND (INTEGERP A)
              (<= 0 A)
              (< A 151115727451828646838272)
              (INTEGERP B)
              (<= 0 B)
              (< B 1125899906842624))
         (BVECP (FL (* A B 1/8388608)) 104)).


HARD ACL2 ERROR in VARIFY:  This should not have happened.  The supposed
variable, '1/8388608, is instead a constant.

ACL2 !>

Guard-checking was being inhibited (since v2-9) for calls of built-in primitives on explicit values, e.g., (car 3). This has been fixed.

Guard-related warnings could be printed during proofs (this bug was introduced in Version_2.9.1). These warnings have been eliminated.

Compound-recognizer rules natp-compound-recognizer and posp-compound-recognizer are now built into ACL2 for predicates natp and posp, and hence have been deleted from book natp-posp.lisp (where they were called natp-cr and posp-cr, respectively).

The function file-clock-p, which recognizes a component of the ACL2 state, is now defined using natp instead of integerp. Thanks to Jared Davis for suggesting this change. (Technical explanation about functions in ACL2 source file axioms.lisp: With a file-clock of -1, the call of make-input-channel in open-input-channel will create a channel that can't be closed; see the guard of close-input-channel.)

(Allegro CL users only) Support is now provided for building an Allegro CL application, provided you have an Allegro CL dynamic runtime license. (Our belief is that with such a license, many users can use the same application, rather than each user needing a separate license.) See new GNUmakefile target allegro-app and file build-allegro-exe.cl for more information.

The new home page now contains a link to a new page other-releases.html, which contains information about other ACL2 releases. (This is in one's local home page, but may not show up on the central ACL2 home page until the next non-incremental release.) Thanks to Warren Hunt for suggesting this addition.

We thank Erik Reeber for suggesting a solution to output redirection using sys-call, which we have described at the end of its documentation.

A new documentation topic fixes the flawed argument for conservativity of the defchoose event that appears in Appendix B of Kaufmann and Moore's paper, ``Structured Theory Development for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203). See conservativity-of-defchoose. Thanks to John Cowles and Ruben Gamboa for helpful feedback on drafts of this note.

The solution to exercise 6.15 in books/textbook/chap6/solutions.txt has been fixed. Thanks to Aaron Smith for pointing out the problem.

A new documentation topic defun-sk-example gives a little more help in using defun-sk effectively. Thanks to Julien Schmaltz for presenting this example as a challenge.

(GCL only) There is now a way to speed up GCL builds of ACL2, at the cost of perhaps a percent or so in performance of the resulting image. Using `make' one supplies the following.

LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

Various makefiles have been improved in several ways.

(1) Parallel book certification, using GNU make's -j option, can be used.

(2) Book certifications now stops at the first failure if books/Makefile or books/Makefile-generic is used, and returns non-zero exit status. However, the various make targets in the ACL2 source directory (regression, certify-books, etc.) still continue past failures unless you provide ACL2_IGNORE=' ' on the `make' command line.

(3) The build process has been modified (file GNUmakefile) so that it stops upon a failed compile or a failed initialization.

(4) The automatic dependency generation (from ``make dependencies'' has been improved so that commands of the form (ld "my-book.lisp") in .acl2 files cause the appropriate depedencies to be generated.

Thanks to comments from several users that led to the above Makefile improvements: Ray Richards, Doug Harper, and the Rockwell ACL2 users for (1) and (2) (and inspiring (4)), and David Rager for (2) and (3). In particular, Doug Harper sent a replacement for the .date mechanism, which was interfering with make -n; so, these files are no longer written.

A mechanism has been added for saving output. In particular, you can now call ld on a file with output turned off, for efficiency, and yet when a proof fails you can then display the proof attempt for the failed (last) event. See set-saved-output. Another new command -- see set-print-clause-ids -- causes subgoal numbers to be printed during proof attempts when output is inhibited.

Documentation has been added for using ACL2's makefile support to automate the certification of collections of books. See books-certification-classic.

Fixed a bug in sys-call-status that was causing hard Lisp errors.

Improved cw-gstack to allow a :frames argument to specify a range of one or more frames to be printed. see cw-gstack.

Fixed a bug in proof-checker command forwardchain. Thanks to Ming-Hsiu Wang for bringing this bug to our attention.

We have provided a mechanism for saving an executable image. See saving-and-restoring and see save-exec. We have eliminated obsolete functions note-lib and make-lib.

Modified the ground-zero theory so that it contains all of the built-in rules (in ACL2 source file axioms.lisp). It had formerly failed to include rules from some definitions and theorems near the end of axioms.lisp.

A new event, set-enforce-redundancy, allows the enforcement of defthm, defun, and most other events during book development. See set-enforce-redundancy.

A bug has been fixed that had allowed deftheory events to cause a hard Lisp error when calling union-theories on ill-formed theories after, for example:

:set-guard-checking nil
(in-theory (union-theories '((:rewrite no-such-rule))
                           (current-theory 'ground-zero)))

(GCL ONLY) Removed the -dir setting in the ACL2 wrapper script for GCL. This should generally have no effect for most users, but it eliminates a potential source of error down the road.

Several interesting new definitions and lemmas have been added to the rtl library developed at AMD, and incorporated into books/rtl/rel4/lib/. Other book changes include a change to lemma truncate-rem-elim in books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis.

The macro real/rationalp may now be referred to in in-theory events and hints, thanks to a new add-macro-alias event. Thanks to Jared Davis for this suggestion.

ACL2 terms of the form (if p 'nil 't) are now printed as (not p), where in some setting they had been printed as (and (not p) t). Thanks to Robert Krug for this improvement.

(GCL ONLY) Added profiling support, based heavily on code supplied by Camm Maguire. See file save-gprof.lsp for instructions. Thanks to Camm, and also to David Hardin for inspiring this addition.

Added support for preprocessing before printing (untranslating) a term. See user-defined-functions-table, in particular the discussion of untranslate-preprocess. Thanks to Jared Davis for inspiring this addition, and for providing a book that takes advantage of it (books/misc/untranslate-patterns.lisp).

The documentation has been improved for explaining how runes are assigned; see rune. Thanks to Robert Krug for pointing out inaccuracies in the existing documentation.