NOTE-3-2

Major Section:  RELEASE-NOTES

NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded here.

Before this release, a raw Lisp error could put the ACL2 user into the debugger of the host Common Lisp. Now, such cases will generally put the user back at the top-level loop after an informative message. For details, see set-debugger-enable; also see break$.

Fixed a soundness bug that was allowing unknown packages to sneak into a book and wreak havoc. Thanks to Peter Dillinger for sending an interesting example that led us to an exploration resulting in finding this bug. (A comment in the source code for note-3-2 shows such an example.) That example led us to fix a couple of other bugs related to packages. See hidden-death-package if you are generally interested in such issues, and for associated examples, see comments in note-3-2 in the ACL2 source code.

Fixed subtle soundness bugs related to :meta rules by restricting evaluators (see defevaluator), as discussed in a new documentation topic: see evaluator-restrictions.

Fixed a soundness bug that was allowing redefinition from :logic to :program mode. This prohibition had been in ACL2 for awhile but was accidentally removed in the preceding version.

Fixed a soundness bug related to trace$. Thanks to Peter Dillinger for bringing it to our attention and for useful discussions, and providing a proof of nil, the essence of which is illustrated as follows:

(value-triple (trace$ (bar :entry (defun foo () 17))))

Closed a loophole that could be viewed as compromising soundness. It was possible to write files during book certification by exploiting make-event expansion, but that is no longer the case by default. A new function open-output-channel! is identical as a function to open-output-channel, except that the new function may be called even during make-event expansion and clause-processor hints, but requires that there is an active trust tag (see defttag). Thanks to Peter Dillinger for producing a convincing example (forging a certificate during book certification; see open-output-channel!) and to him, Sandip Ray, and Jared Davis for useful discussions on the topic.

Added book books/defexec/reflexive/reflexive.lisp to illustrate reflexive functions.

ACL2 now generate scripts that invoke the saved image with exec. (Previously this was only done for GCL and CLISP.) The benefit of this change can be to avoid the lingering of ACL2 processes after enclosing processes have exited. Thanks to Peter Dillinger for pointing out this issue.

ACL2 has a better implementation of (good-bye) (hence of synonyms (quit) and (exit)). As a result, you should now be able to exit ACL2 and Lisp from within the ACL2 read-eval-print loop with any of the above; formerly, this was not supported for some Lisp implementations, and was slow in OpenMCL. Thanks to SBCL developer Harald Hanche-Olsen for useful advice.

Fixed a bug in raw-mode (see set-raw-mode) that was causing hard errors when evaluating calls of er-progn, or of macros expanding to such calls.

Fixed a few Makefile dependencies, necessary only for parallel make.

A new book, misc/defpun-exec-domain-example.lisp, provides an example showing how partial functions which return a unique value for arguments in a specified domain can be efficiently executed with ACL2. Execution is achieved using the mbe construct. Thanks to Sandip Ray for providing this example.

Existing function mod-expt computes (mod (expt base exp) mod) with great efficiency in GCL, but not in other Lisps. Now, the book arithmetic-3/floor-mod/mod-expt-fast.lisp defines a function mod-expt-fast that should provide significantly improved performance for such expressions in other Lisps as well, though still probably not as fast as when using mod-expt in GCL. Thanks to Warren Hunt, with contributions from Robert Krug, for providing this book,

Modified macro break-on-error to print of an error message before entering a break, and to cause a hard error if the underlying Lisp cannot handle it (formerly, a raw Lisp break would occur). Thanks to Bob Boyer for bringing these issues to our attention.

The book books/misc/defpun.lisp, as well as other books related to the defpun macro, has been modified to avoid namespace collisions by prefixing function symbol names with "DEFPUN-"; for example base has been replaced by defpun-base. Thanks to Dave Greve for providing a first version of this update to defpun.lisp.

A theory, base, in books/arithmetic-3/bind-free/top.lisp, has been renamed arithmetic-3-bind-free-base, to avoid potential name conflicts.

Fixed books/arithmetic-3/bind-free/banner.lisp to print (as before) a message about how to turn on non-linear arithmetic, by modifying the call of value-triple to use :on-skip-proofs t. Thanks to Robert Krug for bringing this issue to our attention.

Modified books/Makefile-subdirs and books/Makefile-psubdirs so that they can be used with books/Makefile-generic. Thus, one can set things up so that make can be used to certify books both in the current directory and subdirectories, for example as follows.

  ACL2 = ../../saved_acl2

  arith-top: top all
  all: top

  DIRS = pass1 bind-free floor-mod
  include ../Makefile-subdirs
  include ../Makefile-generic

  top.cert: top.lisp
  top.cert: bind-free/top.cert
  top.cert: floor-mod/floor-mod.cert
  top.cert: floor-mod/mod-expt-fast.cert

An experimental extension of ACL2 is under development by Bob Boyer and Warren Hunt to support function memoization, hash conses, and an applicative version of hash tables. The default build of ACL2 does not include this extension, other than simple logic definitions of functions in new source file hons.lisp. Future versions of ACL2 may fully incorporate this experimental extension.

The defevaluator event macro has been modified primarily by adding a new constraint as follows, where evl is the evaluator. The idea is that for the evaluation of a function call, one may replace each argument by the quotation of its evaluation and then also replace the alist environment with nil.

(DEFTHMD UNHIDE-evl-CONSTRAINT-0
  (IMPLIES (AND (CONSP X)
                (SYNTAXP (NOT (EQUAL A ''NIL)))
                (NOT (EQUAL (CAR X) 'QUOTE)))
           (EQUAL (evl X A)
                  (evl (CONS (CAR X)
                             (KWOTE-LST (UNHIDE-evl-LIST (CDR X) A)))
                       NIL))))

(DEFTHM UNHIDE-evl-CONSTRAINT-1
  (IMPLIES (SYMBOLP X)
           (EQUAL (UNHIDE-evl X A)
                  (AND X (CDR (ASSOC-EQ X A))))))

Explicit compilation is now avoided for OpenMCL, resulting in fewer files to manage (no more files resulting from compilation) and, according to some tests, slightly faster run times. See compilation. Thanks to Bob Boyer and Warren Hunt for suggesting this possibility.

Now, the term-evisc-tuple (see ld-evisc-tuple) is overridden by state global user-term-evisc-tuple in all cases. Formerly, this was only the case when term-evisc-tuple was called with non-nil first argument.

Symbols with the dot (.) character are generally no longer printed with vertical bars. For example, before this change:

  ACL2 !>'ab.c
  |AB.C|
  ACL2 !>

  ACL2 !>'ab.c
  AB.C
  ACL2 !>

Fixed bugs in guard verification for theorems. The following examples illustrate these bugs. If either theorem's body is executed in raw Lisp there is likely to be a hard Lisp error, even though verify-guards was supposed to ensure against that behavior.

; Example: Verify-guards failed to check that all functions in the theorem
; had already been guard-verified.
(defun my-car (x) (car x))
(defthm my-car-compute-example (equal (my-car 3) (my-car 3)))
(verify-guards my-car-compute-example)

; Example: Verify guards of a theorem whose body uses state improperly.
(defthm bad-state-handler
  (if (state-p state)
      (equal (car state) (car state))
    t)
  :rule-classes nil)
(verify-guards bad-state-handler)

See GCL for an example, developed with Warren Hunt and Serita Nelesen, that shows how to get fast fixnum (small integer) arithmetic operations in GCL.

Fixnum declarations are now realized as (signed-byte 30) and (unsigned-byte 29) instead of what was generally (signed-byte 29) and (unsigned-byte 28). MCL users may thus find better performance if they switch to OpenMCL. Note that some definitions have changed correspondingly; for example, zpf now declares its argument to be of type (unsigned-byte 29) instead of (unsigned-byte 28). A few books may thus need to be adjusted; for example, changes were made to books in books/data-structures/memories/.

ACL2's rewriter now avoids removing certain true hypotheses and false conclusions. When a hypothesis rewrites to true or a conclusion rewrites to false, ACL2 formerly removed that hypothesis or conclusion. Now, it only does such removal when the hypothesis or conclusion is either a call of equal or an equivalence relation (see equivalence), or else is sufficiently trivial (roughly, either redundant with another hypothesis or conclusion or else trivially true without considering the rest of the goal). A specific example may be found in source file simplify.lisp; search for ``; But we need to do even more work''. Thanks to Robert Krug for providing the idea for this improvement and its initial implementation. As is common with heuristic changes, you may find it necessary on occasion to rename some subgoals in your hints. And in this case, you might also find it necessary on rare occasions to add :do-not '(generalize) hints.

A new function, mfc-relieve-hyp, allows (for example) for more powerful bind-free hypotheses, by providing an interface to the rewriter's routine for relieving hypotheses. See extended-metafunctions. Thanks to Robert Krug for providing the idea for this feature and its initial implementation.

Two improvements have been made to non-linear arithmetic (see non-linear-arithmetic). One allows for deducing strict inequality (<) for the result of certain polynomial multiplications, where previously only non-strict inequality (<=) was deduced. A second allows the use of the product of two polynomials when at least one of them is known to be rational. We had previously restricted the use of the product to the case where both were known to be rational. Thanks to Robert Krug for these improvements.

(OpenMCL and Allegro CL only) Fixed ACL2's redefinitions of raw Lisp trace and untrace in OpenMCL and Allegro CL so that when given no arguments, they return the list of traced functions. For trace, this is an ANSI spec requirement. Note that trace$ and untrace$ continue to return nil in the ACL2 loop.

Fixed a bug that was allowing the symbol &whole to appear in other than the first argument position for a defmacro event, in violation of the Common Lisp spec (and leading to potentially surprising behavior). Thanks to Peter Dillinger for bringing this bug to our attention.

It had been illegal to use make-event under some calls of ld. This has been fixed. Thanks to Jared Davis for bringing this issue to our attention with a simple example, in essence:

(ld '((defmacro my-defun (&rest args) `(make-event '(defun ,@args)))
      (my-defun f (x) x)))

ACL2 no longer prohibits certain make-event forms when including uncertified books. Thanks to Peter Dillinger for first bringing this issue to our attention.

Hard errors arose when using break-rewrite stack display commands, in particular :path and :frame, from inside the proof-checker. This has been fixed.

Fixed a bug that could cause functions that call system built-ins f-put-global, f-get-global, or f-boundp-global to cause a raw Lisp error even when proving theorems. Thanks to Peter Dillinger, for reporting such a failure for the form (thm (w '(1 2 3))).

Renamed the formal parameters of function set-equal in distributed book books/arithmetic-3/bind-free/normalize.lisp so that more distributed books can be included together in the same session. In particular books books/data-structures/set-theory and books/arithmetic-3/extra/top-ext can now be included together. Thanks to Carl Eastlund for bringing this problem to our attention and to Robert Krug for suggesting the formals renaming as a fix.

Metafunctions must now be executable. See meta.

New utilities allow for user-defined simplifiers at the goal level, both verified and unverified (``trusted''), where the latter can even be defined by programs outside ACL2. See clause-processor, which points to a new directory books/clause-processors/ that contains examples of these new utilities, including for example a system (``SULFA'') contributed by Erik Reeber that implements a decision procedure (thanks, Erik). Also see proof-checker-commands for the new proof-checker command clause-processor (or for short, cl-proc).

The rewriter has been tweaked to run faster in some cases involving very large terms. Thanks to Eric Smith and Jared Davis for providing a helpful example that helped us locate the source of this inefficiency.

Added books/make-event/defspec.lisp. This book shows how one can mimic certain limited forms of higher-order statements in ACL2 by use of macros, make-event, and table events. Thanks to Sandip Ray for his contribution.

A new release of the RTL library, books/rtl/rel7/, replaces the previous version, books/rtl/rel6/. Thanks to Hanbing Liu and David Russinoff for providing this new version.

We thank David Russinoff for providing a proof of the law of quadratic reciprocity. See books/quadratic-reciprocity/Readme.lsp.

Eliminated a slow array warning (see slow-array-warning) that could occur when exiting a wormhole after executing an in-theory event in that wormhole. Thanks to Dave Greve for bringing this problem to our attention.

A new accessor, (mfc-rdepth mfc), provides a new field, the remaining rewrite stack depth, which has been added to metafunction context structures; see extended-metafunctions. Thanks to Eric Smith for suggesting this addition.

The algorithms were modified for collecting up rule names and other information used in proofs, into so-called ``tag-trees''. Tag-trees are now free of duplicate objects, and this change can dramatically speed up some proofs that involve many different rules. Thanks to Eric Smith for doing some profiling that brought this issue to our attention, and for reporting that this change reduced proof time on an example by about 47% (from 3681.46 reported seconds down to 1954.69).

All legal xargs keywords may now be used in verify-termination events. In particular, this is the case for :normalize.

(SBCL and CMUCL only) Fixed a problem with stobj array resizing functions that was causing a hard error in ACL2 images built on SBCL or CMUCL.

A new table, evisc-table, allows you to introduce print abbreviations, for example for large constants. Moreover, a new reader macro -- #, -- makes it convenient to reference constants even inside a quote. See evisc-table. Thanks to Bob Boyer and Warren Hunt for useful discussions leading to this feature.

The macros in books/misc/expander.lisp now have a new keyword argument, :simplify-hyps-p. The default behavior is as before, but now case splitting from hypothesis simplification can be avoided. For details, evaluate (include-book "misc/expander" :dir :system) and then :doc! defthm? and :doc! symsym. Thanks to Daron Vroon for sending a question that prompted this additional functionality.

ACL2 failed to apply :restrict hints to rules of class :definition, except for the simplest sorts (see simple). This has been fixed. Thanks to Jared Davis for pointing out this bug by sending a small example.

Added a new :msg argument to assert-event; see assert-event. The implementation of value-triple has been modified to support this change.

Fixed a bug in macro io? that now allows the commentp argument to be t. This provides a way other than cw to print without modifying state, for example as follows. (Warning: Certain errors may leave you in a wormhole, in which case use :a! to abort.)

ACL2 !>(prog2$ (io? event t state
                    ()
                    (fms "Howdy~%" nil *standard-co* state nil))
               (+ 3 4))

Howdy
7
ACL2 !>:set-inhibit-output-lst (proof-tree event)
 (PROOF-TREE EVENT)
ACL2 !>(prog2$ (io? event t state
                    ()
                    (fms "Howdy~%" nil *standard-co* state nil))
               (+ 3 4))
7
ACL2 !>

ACL2 now disallows calls of progn! inside function bodies, just as it already disallowed such calls of progn, since in both cases the Common Lisp meaning differs from the ACL2 meaning.

Redefinition of system functions now always requires an active trust tag (see defttag). This restriction was intended before, but there was a hole that allowed a second redefinition without an active trust tag. Thanks to Peter Dillinger for pointing out this bug.

Verify-termination has been disabled for a few more built-in functions that are in :program mode. (If you are curious about which ones they are, evaluate (f-get-global 'built-in-program-mode-fns state).) [Note added for Version_3.4: This state global has been changed to 'program-fns-with-raw-code.] Moreover, such functions now will execute only their raw Lisp code, so for example they cannot be called during macroexpansion. Thanks to Peter Dillinger and Sandip Ray for useful discussions on details of the implementation of this restriction.

New untouchable state global variables, temp-touchable-vars and temp-touchable-fns, can control the enforcement of untouchability. See remove-untouchable. Thanks to Peter Dillinger for suggesting these features.

The ``TTAG NOTE'' string was being printed by encapsulate events whenever an active trust tag was already in effect (see defttag), even if the encapsulate event contained no defttag event. This has been fixed. Thanks to Peter Dillinger for a query leading to this fix.

Fixed a bug in progn! that could leave the user in raw-mode (see set-raw-mode). This could occur when certifying a book with a compile-flg value of t (see certify-book), when that book contained a progn! event setting raw-mode to t without setting raw-mode back to nil:

(progn! (set-raw-mode t) ...)