NOTE-5-0

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.

Below we roughly organize the changes since Version 4.3 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, changes at the system level and to distributed books, Emacs support, and experimental versions. Each change is described in just one category, though of course many changes could be placed in more than one category.

NOTE: ACL2 is now distributed under Version 2 of the GNU General Public License. [Added later: The license has changed since Version_5.0. See LICENSE.] Formerly, any later version had been acceptable. Moreover, books are no longer distributed from a University of Texas website, but rather, from Google Code at http://code.google.com/p/acl2-books/downloads/.

CHANGES TO EXISTING FEATURES

A fatal error now occurs if environment variable ACL2_CUSTOMIZATION has a value other than NONE or the empty string, but is not the name of an existing file. Thanks to Harsh Raju Chamarthi for requesting such a change.

Functions read-acl2-oracle (and read-acl2-oracle@par), read-run-time, and main-timer are no longer untouchable (see remove-untouchable).

We now avoid certain duplicate conjuncts in the constraint stored for encapsulate events. For example, the constraint stored for the following event formerly included (EQUAL (FOOP (CONS X Y)) (FOOP Y)) and (BOOLEANP (FOOP X)) twice each, but no more.

(encapsulate
 ((foop (x) t))
 (local (defun foop (x) (declare (ignore x)) t))
 (defthm foop-constraints
   (and (booleanp (foop x))
        (equal (foop (cons x y)) (foop y)))
   :rule-classes
   ((:type-prescription :corollary (booleanp (foop x)))
    (:rewrite :corollary (equal (foop (cons x y)) (foop y))))))

The :guard for a constrained function (see signature) may now mention function symbols introduced in the same encapsulate event that introduces that function. Thanks to Nathan Wetzler for a helpful discussion leading to this improvement.

The test for redundancy (see redundant-events) of encapsulate events has been improved in cases involving redefinition (see ld-redefinition-action). Thanks to Jared Davis for providing the following example, which illustrates the problem.

  (redef!)

  (encapsulate ()
    (defun g (x)
      (+ 3 x)))

  (g 0) ; 3, as expected

  (encapsulate ()
    (defun g (x)
      (+ 4 x)))

  (g 0) ; 4, as expected

  ; Unfortunately, the following was flagged as redundant because it agreed
  ; with the first encapsulate above.  That has been fixed; now, it is
  ; recognized as not being redundant.
  (encapsulate ()
    (defun g (x)
      (+ 3 x)))

The test for redundancy of defun and defconst events has been improved in the case that redefinition is active. In that case, redundancy now additionally requires that the ``translated'' body is unchanged, i.e., even after expanding macro calls and replacing constants (defined by defconst) with their values. Thanks to Sol Swords for requesting this enhancement, and to Jared Davis for pointing out a bug in a preliminary change. See redundant-events, in particular the ``Note About Unfortunate Redundancies''. Note that this additional requirement was already in force for redundancy of defmacro events.

The macro defmacro-last and the table return-last-table have been modified so that when they give special treatment to a macro mac and its raw Lisp counterpart mac-raw, a call (return-last 'mac-raw ...) can be made illegal when encountered directly in the top level loop, as opposed to inside a function body. See return-last. Thanks to Harsh Raju Chamarthi for showing us an example that led us to make this improvement.

We removed a barrier to admitting function definitions, as we explain using the following example.

(defun foo (m state)
  (declare (xargs :stobjs state))
  (if (consp m)
      (let ((state (f-put-global 'last-m m state)))
        (foo (cdr m) state))
    state))

It is no longer the case that break-on-error causes a Lisp break when encountering an error during translation of user input into internal (translated) form (see term). The reason is that an improvement to the translation process, specifically the one described in the preceding paragraph, allows certain backtracking from ``errors'', which are intended to be silent rather than causing breaks into raw Lisp. Thanks to Jared Davis for sending an example leading to this change.

(CCL and SBCL only) When the host Lisp is CCL or SBCL, then since all functions are compiled, a certify-book command will no longer load the newly-compiled file (and similarly for include-book with argument :load-compiled-file :comp).

Set-write-acl2x now returns an error triple and can take more values, some of which automatically allow including uncertified books when certify-book is called with argument :acl2x t.

The environment variable COMPILE_FLG has been renamed ACL2_COMPILE_FLG; see certify-book.

The macros defthmd and defund no longer return an error triple with value :SKIPPED when proofs are being skipped. Rather, the value returned is the same as would be returned on success when proofs are not skipped.

For those who use set-write-acl2x: now, when certify-book is called without a :ttagsx argument supplied, then the value of :ttagsx defaults to the (explicit or default) value of the :ttags argument.

The :pl and :pl2 commands can now accept terms that had previously been rejected. For example, the command :pl (member a (append x y)) had caused an error, but now it works as one might reasonably expect, treating member as member-equal (see equality-variants for relevant background). Thanks to Jared Davis for reporting this problem by sending the above example.

We have eliminated some hypotheses in built-in rewrite rules characterp-nth and ordered-symbol-alistp-delete-assoc-eq.

Added the symbols f-get-global, f-put-global, and state-global-let* to *acl2-exports*.

Added to the guards of push-untouchable and remove-untouchable the requirement that the second argument must be a Boolean. Thanks to Jared Davis for sending an example that led to this change.

The built-in function string-for-tilde-@-clause-id-phrase has been put into :logic mode and had its guards verified, as have some subsidiary functions. A few new rules have been added in support of this work; search for string-for-tilde-@-clause-id-phrase in ACL2 source file boot-strap-pass-2.lisp if interested. Thanks to David Rager for contributing an initial version of this improvement.

All trust tags are now in the keyword package. The defttag event may still take a symbol in an arbitrary package, but the trust tag created will be in the keyword package (with the same symbol-name as the symbol provided). Similarly, non-nil symbols occurring in the :ttags argument of an include-book or certify-book command will be converted to corresponding keywords. See defttag.

There have been several changes to gag-mode. It is now is initially set to :goals, suppressing most proof commentary other than key checkpoints; see set-gag-mode. (As before, see pso for how to recover the proof output.) Also, top-level induction schemes are once again printed when gag-mode is on, though these as well as printing of guard conjectures can be abbreviated (``eviscerated'') with a new evisc-tuple; see set-evisc-tuple, in particular the discussion there of :GAG-MODE. Finally, the commentary printed within gag-mode that is related to forcing-rounds is now less verbose. Thanks to Dave Greve and David Rager for discussions leading to the change in the printing of induction schemes under gag-mode; thanks to Warren Hunt for an email that led us to similar handling for printing of guard conjectures; and thanks to Robert Krug for a suggestion that led us to restore, in abbreviated form, important information about the sources of forcing round goals.

An error now occurs if ld is called while loading a compiled book. See calling-ld-in-bad-contexts. Thanks to David Rager for reporting a low-level assertion failure that led us to make this change.

The proof-checker interactive loop is more robust: most errors will leave you in that loop, rather than kicking you out of the proof-checker and thus back to the main ACL2 read-eval-print loop. Thanks to David Hardin for suggesting this improvement in the case of errors arising from extra right parentheses.

The summary at the end of a proof now prints the following note when appropriate:

[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Improved dmr to show the function being called in the case of explicit evaluation: ``(EV-FNCALL function-being-called)''.

It is now permitted to bind any number of stobjs to themselves in the bindings of a LET expression. But if any stobj is bound to other than itself in LET bindings, then there still must be only one binding in that LET expression. The analogous relaxation holds for LAMBDA expressions. Thanks to Sol Swords for requesting such a change, which was needed for some code generated by macro calls.

The macro top-level now returns without error; See top-level. Formerly, this macro always returned an error triple (mv t .. state), which meant that normal calls of ld would stop after encountering a call of top-level. Thanks to Jared Davis for bringing this issue to our attention.

It is no longer the case that when you specify xargs keyword :non-executable t in a defun form rather than using defun-nx, then the form of the body need match only the shape (prog2$ (throw-nonexec-error ... ...) ...). We now require that the body of the definition of a function symbol, fn, with formals (x1 ... xk), be of the form (prog2$ (throw-nonexec-error 'fn (list x1 ... xk)) ...). This fixes the following odd behavior, which could be considered a bug. Consider a book that contains the following two events.

(defun foo (x)
  (declare (xargs :guard t :non-executable t :mode :logic))
  (prog2$ (throw-nonexec-error 'bar (list x))
          (cons 3 x)))
(defn h (x)
  (foo x))

ACL2 !>(h 3)


ACL2 Error in TOP-LEVEL:  ACL2 cannot ev the call of undefined function
BAR on argument list:

(3)

To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

A tautology checker used in the ACL2 sources (function if-tautologyp) has been limited somewhat in the effort it makes to recognize a tautology. While we expect it to be rare for the effect of this change to be noticeable, we thank Sol Swords for sending us an example that motivated this change: a guard verification that took about 5 seconds in Version_4.3 now takes, on the same machine, about 0.07 seconds.

The behavior of backquote (`) has been changed slightly to be compatible with its behavior in raw Lisp. The change is to allow the use of comma-atsign (,@) at the end of a list, as in the following example.

(let ((x 3) (y 2) (z 7)) `(,x ,y ,@z))

A call of the theory macro had previously returned nil when applied to other than the name of name of a previously executed deftheory event. Now, a hard error occurs.

The table binop-table has been replaced by the table untrans-table. However, add-binop and remove-binop continue to have the same effect as before. See add-macro-fn, which is a new feature discussed below.

The function booleanp is now defined using eq instead of equal, which may increase its efficiency. Thanks to Jared Davis for this change.

For pairs (key . val) in the macro-aliases-table, there had been a requirement that val is a known function symbol. Now, it only needs to be a symbol. (This change was made to support the new feature, defun-inline, described elsewhere in these release notes.)

NEW FEATURES

A new ``tau system'' provides a kind of ``type checker.'' See tau-system. Thanks to Dave Greve for supplying a motivating example (on which this system can provide significant speedup), and to Sol Swords for sending a very helpful bug report on a preliminary implementation.

Users may now arrange for additional summary information to be printed at the end of events. [Note added at Version_6.1: Formerly we pointed here to print-summary-user, but now, see finalize-event-user; also see note-6-1]. Thanks to Harsh Raju Chamarthi for requesting this feature and participating in a design discussion.

A new, advanced proof-checker command, geneqv, shows the generated equivalence relation at the current subterm. Thanks to Dave Greve for an inquiry leading to this enhancement.

A new reader macro, #u, permits the use of underscore characters in a number. See sharp-u-reader. Thanks to Jared Davis for requesting this capability.

New proof-checker commands pl and pr provide interfaces to the ACL2 commands :pl and :pr, respectively. These can be useful if you want to see trivially-proved hypotheses, as now clarified in the proof-checker documentation for its show-rewrites command. See proof-checker-commands. Thanks to Pete Manolios for suggesting such clarification and capability.

It is now legal to call non-executable functions without the usual signature restrictions imposed on executable code. For example, the third event below was not admissible, but now it is.

(defstobj foo fld)
(defun-nx id (x)
  x)
(defun f (foo)
  (declare (xargs :stobjs foo :verify-guards nil))
  (cons 3 (id foo)))

(defstobj foo (fld))
(defun-nx my-identity (x) x)
(defun my-fld (foo)
  (declare (xargs :stobjs foo))
  (mbe :logic (my-identity foo)
       :exec (let ((val (fld foo)))
               (update-fld val foo))))

A new macro, non-exec, allows the use of non-executable code, for example inside ordinary function definitions. Thanks to Sol Swords for requesting this enhancement.

A new ``provisional certification'' process is supported that can allow books to be certified before their included sub-books have been certified, thus allowing for potentially much greater `make'-level parallelism. See provisional-certification. Thanks to Jared Davis for requesting this feature and for helpful discussions, based in part on rudimentary provisional certification schemes that he developed first at Rockwell Collins and later for his `Milawa' project. Also, thanks to Jared and to Sol Swords for testing this feature and for providing a fix for a bug in a preliminary implementation, and thanks to Sol for providing performance feedback and a crucial suggestion that led to an improved implementation.

Event summaries now show the names of events that were mentioned in hints of type :use, :by, or :clause-processor. See set-inhibited-summary-types. Thanks to Francisco J. Martin Mateos for requesting such an enhancement (actually thanks to the community, as his request is the most recent but this has come up from time to time before).

ACL2 now stores a data structure representing the relation ``Event A is used in the proof of Event B.'' See dead-events, which explains this data structure and mentions one application: to identify dead code and unused theorems. Thanks to Shilpi Goel for requesting such a feature and for helpful feedback.

A new documentation topic provides a guide to programming with state; see programming-with-state. Thanks to Sarah Weissman for suggesting that such a guide might be useful, and to David Rager for helpful feedback on a preliminary version. There also has been some corresponding reorganization of the documentation as well as creation of additional documentation (e.g., see state-global-let*). Now, most built-in functions and macros commonly used in programs (as opposed to events like defun, for example) are subtopics of a new topic -- see acl2-built-ins -- which is a subtopic of programming, a topic that in turn has considerably fewer direct subtopics than before.

It is now possible to bind extra variables in a :USE hint, thus avoiding the error message: ``The formula you wish to instantiate, ..., mentions only the variable(s) ...''. See lemma-instance, in particular the discussion of keyword :extra-bindings-ok. Thanks to Sol Swords for requesting such an enhancement.

The function read-object-suppress is like read-object except that it avoids errors and discards the value read. See io.

A stobj may now be passed as an argument where another stobj is expected if the two are ``congruent''. See defstobj, in particular, its discussion of the new :congruent-to keyword of defstobj. Thanks to Sol Swords for requesting this enhancement and for useful discussions contributing to its design.

A new top-level utility has been provided that shows the assembly language for a defined function symbol; see disassemble$. Thanks to Jared Davis for requesting such a utility and to Shilpi Goel for pointing out an inconvenience with the initial implementation. Note that it uses the distributed book books/misc/disassemble.lisp, which users are welcome to modify (see http://www.cs.utexas.edu/users/moore/acl2/).

The macro set-accumulated-persistence is an alias for accumulated-persistence. Thanks to Robert Krug for suggesting this addition.

A new documentation topic lists lesser-known and advanced ACL2 features, intended for those with prior ACL2 experience who wish to extend their knowledge of ACL2 capabilities. See advanced-features. Thanks to Warren Hunt and Anna Slobodova for requesting such information.

A new macro, deftheory-static, provides a variant of deftheory such that the resulting theory is the same at include-book time as it was at certify-book time. Thanks to Robert Krug for helpful discussions on this new feature and for updating his books/arithmetic-5/ distributed books to use this feature.

A new event, defabsstobj, provides a new way to introduce single-threaded objects (see stobj and see defstobj). These so-called ``abstract stobjs'' permit user-provided logical definitions for primitive operations on stobjs, for example using an alist-based representation instead of a list-based representation for array fields. Moreover, the proof obligations guarantee that the recognizer is preserved; hence the implementation avoids executing the recognizer, which may be an arbitrarily complex invariant that otherwise would be an expensive part of guard checks. Thanks to Warren Hunt for a request leading us to design and implement this new feature, and thanks to Rob Sumners for a request leading us to implement a related utility, defabsstobj-missing-events. See defabsstobj. Also thanks to Sol Swords for sending an example exhibiting a bug in the initial implementation, which has been fixed.

A new command, :psof <filename>, is like :pso but directs proof replay output to the specified file. For large proofs, :psof may complete much more quickly than :pso. see psof. More generally, a new utility, wof (an acronym for ``With Output File''), directs standard output and proofs output to a file; see wof.

The new macro defnd defines a function with :guard t and disables that function, in analogy to how defund defines with defun and then disables. Thanks to Shilpi Goel for requesting this feature.

The :pl2 command now shows :linear rules; and a new proof-checker command, show-linears (equivalently, sls), is an analogue of the proof-checker show-rewrites (sr) command, but for linear rules. Thanks to Shilpi Goel for requesting this new proof-checker command. Finally, a corresponding new proof-checker command, apply-linear (al), is an analogue of the proof-checker rewrite (r) command, but for linear rules.

The macros add-macro-fn and remove-macro-fn replace macros add-binop and remove-binop, respectively, though the latter continue to work. The new macros allow you to decide whether or not to display calls of binary macros as flat calls for right-associated arguments, e.g., (append x y z) rather than (append x (append y z)). See add-macro-fn.

It is now possible to request that the host Lisp compiler inline calls of specified functions, or to direct that the host Lisp compiler not inline such calls. See defun-inline and see defun-notinline. We thank Jared Davis for several extensive, relevant conversations, and for finding a bug in a preliminary implementation. We also thank others who have engaged in discussions with us about inlining for ACL2; besides Jared Davis, we recall such conversations with Rob Sumners, Dave Greve, and Shilpi Goel.

HEURISTIC IMPROVEMENTS

Reading of ACL2 arrays (see aref1, see aref2) has been made more efficient (as tested with CCL as the host Lisp) in the case of consecutive repeated reads of the same named array. Thanks to Jared Davis and Sol Swords for contributing this improvement.

Slightly modified the induction schemes stored, so that calls of so-called ``guard-holders'' (such as mbe and prog2$ -- indeed, any call of return-last -- and the) are expanded away. In particular, calls of equality variants such as member are treated as their corresponding function calls, e.g., member-equal; see equality-variants. Guard-holders are also now expanded away before storing constraints for encapsulate events, which can sometimes result in simpler constraints.

Improved the performance of dmr (technical note: by modifying raw Lisp code for function dmr-flush, replacing finish-output by force-output).

We now avoid certain rewriting loops. A long comment about this change, including an example of a loop that no longer occurs, may be found in source function expand-permission-result.

Slightly strengthened type-set reasoning at the level of literals (i.e., top-level hypotheses and conclusions). See the comment in ACL2 source function rewrite-atm about the ``use of dwp = t'' for an example of a theorem provable only after this change.

Strengthened the ability of type-set reasoning to make deductions about terms being integers or non-integer rationals. The following example illustrates the enhancement: before the change, no simplification was performed, but after the change, the conclusion simplifies to (foo t). Thanks to Robert Krug for conveying the problem to us and outlining a solution.

(defstub foo (x) t)
(thm ; should reduce conclusion to (foo t)
 (implies (and (rationalp x)
               (rationalp y)
               (integerp (+ x (* 1/3 y))))
          (foo (integerp (+ y (* 3 x))))))

BUG FIXES

Fixed a class of soundness bugs involving each of the following functions: getenv$, get-wormhole-status, cpu-core-count, wormhole-p, random$, file-write-date$, and serialize-read-fn, and (for the HONS version of ACL2) clear-memoize-table and clear-memoize-tables as well as (possible soundness bug) serialize-write-fn. For example, we were able to admit the following events, but that is no longer the case (neither for getenv$ as shown, nor analogously for other functions listed above).

(defthm not-true
  (stringp (cadr (getenv$ "PWD" (build-state))))
  :rule-classes nil)

(defthm contradiction
  nil
  :hints (("Goal"
           :in-theory (disable (getenv$))
           :use not-true))
  :rule-classes nil)

Fixed a soundness bug involving with-live-state, which could cause an error in the use of add-include-book-dir or delete-include-book-dir in a book or its portcullis commands. See with-live-state, as the documentation for this macro has been updated; in particular it is now untouchable (see remove-untouchable) and is intended only for system hackers. Thanks to Jared Davis for reporting a bug in the use of add-include-book-dir after our first attempt at a fix.

Fixed a soundness bug based on the use of skip-proofs together with the little-used argument k=t for certify-book. An example proof of nil appears in a comment in the ACL2 sources, in (deflabel note-5-0 ...).

Fixed a soundness bug that allowed users to define new proof-checker primitive commands. Before this fix, a book proving nil could be certified, as shown in a comment now in the introduction of the table pc-command-table in source file proof-checker-a.lisp.

(Technical change, primarily related to make-event:) Plugged a security hole that allowed books' certificates to be out-of-date with respect to make-event expansions, but not recognized as such. The change is to include the so-called expansion-alist in the certificate's checksum. An example appears in a comment in the ACL2 sources, in (deflabel note-5-0 ...).

Fixed a bug in guard verification due to expanding calls of primitives when translating user-level terms to internal form, so called ``translated terms'' (see term). While we have not observed a soundness hole due to this bug, we have not ruled it out. Before the bug fix, the following event was admissible, as guard verification succeeded (but clearly should not have).

(defun f ()
  (declare (xargs :guard t))
  (car (identity 3)))

While calls of many event macros had been prohibited inside executable code, others should have been but were not. For example, the following was formerly allowed.

(defun foo (state)
  (declare (xargs :mode :program :stobjs state))
  (add-custom-keyword-hint :my-hint (identity nil)))
(foo state) ; Caused hard raw Lisp error!

Fixed an assertion that could occur, for example, after reverting to prove the original goal by induction and generating a goal of NIL. Thanks to Jared Davis for sending us a helpful example to bring this bug to our attention.

It was possible for defstobj to generate raw Lisp code with excessively restrictive type declarations. This has been fixed. Thanks to Warren Hunt for reporting this bug and sending an example that illustrates it. See stobj-example-2 for examples of such raw Lisp code; now, one finds (and fixnum (integer 0 *)) where formerly the type was restricted to (integer 0 268435455).

Fixed a bug in that was ignoring the use of :computed-hint-replacement in certain cases involving a combination of computed hints and custom keyword hints. Thanks to Robert Krug for reporting this bug and sending a very helpful example.

Fixed a bug in the output from defattach, which was failing to list previous events in the message about ``bypassing constraints that have been proved when processing the event(s)''.

(GCL only) Fixed a bug in set-debugger-enable (which was only a bug in GCL, not an issue for other host Lisps).

Fixed ACL2 trace output to indent properly for levels above 99 (up to 9999). Thanks to Warren Hunt for bringing this bug to our attention.

Fixed a bug in the reporting of times in event summaries -- probably one that has been very long-standing! The times reported had often been too small in the case of compound events, notably include-book. Thanks to everyone who reported this problem (we have a record of emails from Eric Smith and Jared Davis on this issue).

Fixed a bug in :expand hints, where the use of :lambdas could prevent other parts of such a hint. For example, the following invocation of thm failed before this fix was made.

(defund foo (x) (cons x x))
(thm (equal (car (foo x)) x)
:hints (("Goal" :expand (:lambdas (foo x)))))

Certain ``program-only'' function calls will now cause hard Lisp errors. (The rather obscure reason for this fix is to support logical modeling of the ACL2 evaluator. A relevant technical discussion may be found in source function oneify-cltl-code, at the binding of variable fail_program-only-safe.)

There was an unnecessary restriction that FLET-bound functions must return all stobjs among their inputs. For example, the following definition was rejected because state was not among the outputs of h. This restriction has been removed.

(defun foo (state)
  (declare (xargs :stobjs state))
  (flet ((h (state) (f-boundp-global 'x state)))
    (h state)))

We fixed a bug, introduced in the preceding release (Version 4.3), in the check for irrelevant formals (see irrelevant-formals). That check had been too lenient in its handling of lambda (LET) expressions, for example allowing the following definition to be admitted in spite of its first formal parameter obviously being irrelevant.

(defun foo (x clk)
  (if (zp clk)
      :diverge
    (let ((clk (1- clk)))
      (foo x clk))))

Fixed a bug in the mini-proveall target in GNUmakefile. The fix includes a slight change to the :mini-proveall command (an extra event at the end). Thanks to Camm Maguire for reporting this bug.

Fixed a bug that occurred when certify-book was called after using set-fmt-soft-right-margin or set-fmt-hard-right-margin to set a small right margin.

Fixed set-inhibit-warnings so that it takes effect for a subsequent include-book event. Thanks to Jared Davis and David Rager for queries that led to this fix.

Hard Lisp errors are now avoided for certain :rewrite rules: those whose equivalence relation is other than equal when the rule is originally processed, but is no longer a known equivalence relation when the rule is to be stored. Thanks to Jared Davis for sending a useful example, a minor variant of which is included in a comment in source function interpret-term-as-rewrite-rule (file defthm.lisp).

Fixed a bug in the ACL2 evaluator (source function raw-ev-fncall), which was unlikely to be exhibited in practice.

Fixed a hard Lisp error that could occur for ill-formed :meta rule-classes, e.g., (:meta :trigger-fns '(foo)).

It is now an error to include a stobj name in the :renaming alist (see defstobj).

Some bogus warnings about non-recursive function symbols have been eliminated for rules of class :type-prescription.

(Allegro CL host Lisp only) Fixed an obsolete setting of compiler variable comp:declared-fixnums-remain-fixnums-switch, which may have been responsible for intermittent (and infrequent) checksum errors encountered while including books during certification of the regression suite.

Fixed a proof-checker bug that could result in duplicate goal names in the case of forced hypotheses. An example showing this bug, before the fix, appears in a comment in the ACL2 sources, in (deflabel note-5-0 ...).

We fixed a bug in a prover routine involved in type-set computations involving linear arithmetic. This bug has been around since at least as far back as Version_3.3 (released November, 2007). We are not aware of any resulting unsoundness, though it did have the potential to weaken the prover. For example, the following is proved now, but was not proved before the bug was fixed.

(thm
 (implies (and (rationalp x)
               (rationalp y)
               (integerp (+ (* 1/3 y) x)))
          (integerp (+ y (* 3 x))))
 :hints (("Goal" :in-theory (disable commutativity-of-+))))

Although all bets are off when using redefinition (see ld-redefinition-action), we wish to minimize negative effects of its use, especially raw Lisp errors. The examples below had caused raw Lisp errors, but no longer.

(defstobj st fld :inline t)
(redef!)
(defstobj st new0 fld)
(u)
(fld st) ; previously an error, which is now fixed

; Fresh ACL2 session:
(redef!)
(defun foo (x) x)
(defmacro foo (x) `(quote ,x))
(u)

; Fresh ACL2 session:
(redef!)
(defmacro foo (x) (cons 'list x))
(defun foo (x) x)

Fixed a bug that could cause hard Lisp errors in an encapsulate event. Thanks to Sol Swords for sending an example that exhibited this bug. Here is a simpler such example; the bug was in how it was checked whether the guard for a guard-verified function (here, g) depends on some function introduced in the signature of the encapsulate (here, the function f).

(encapsulate
 ((f (x) t))
 (local (defun f (x) (declare (xargs :guard t)) x))
 (defun g (x)
   (declare (xargs :guard (if (integerp x) (f x) t)))
   x))

Fixed a bug in mfc-relieve-hyp that we believe could prohibit its use on the last hypothesis. Thanks to Sol Swords for reporting this bug and providing a fix.

The syntax #! (see sharp-bang-reader) was broken after a skipped readtime conditional. For example, the following input line caused an error.

#+skip #!acl2(quote 3)

Fixed a bug in the break-rewrite utility, which was evidenced by error messages that could occur when dealing with free variables. An example of such an error message is the following; we thank Robert Krug for sending us an example that produced this error and enabled us to produce a fix.

HARD ACL2 ERROR in TILDE-@-FAILURE-REASON-PHRASE1:  Unrecognized failure
reason, ((MEM-ARRAY . X86) (ADDR QUOTE 9)).

We fixed an obscure bug that we believe could interfere with defproxy because of an incorrect (declaim (notinline <function>)) form.

CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS

Improvements have been made related to the reading of characters. In particular, checks are now done for ASCII encoding and for the expected char-code values for Space, Tab, Newline, Page, and Rubout. Also, an error no longer occurs with certain uses of non-standard characters. For example, it had caused an error to certify a book after a single portcullis command of (make-event `(defconst *my-null* ,(code-char 0))); but this is no longer an issue. Thanks to Jared Davis for helpful correspondence that led us to make these improvements.

The character encoding for reading from files has been fixed at iso-8859-1. See character-encoding. Thanks to Jared Davis for bringing this portability issue to our attention (as this change arose in order to deal with a change in the default character encoding for the host Lisp, CCL), and pointing us in the right direction for dealing with it. In many cases, the character encoding for reading from the terminal is also iso-8859-1; but this is not guaranteed. In particular, when the host Lisp is SBCL this may not be the case.

Although the HTML documentation is distributed with ACL2, it had not been possible for users to build that documentation without omitting graphics, for example on the ACL2 home page. That has been fixed, as files graphics/*.gif are now distributed.

Compiler warnings are suppressed more completely than they had been before. For example, the following had produced a compiler warning when the host Lisp is CCL, but no longer does so.

(defun f () (car 3))
(trace$ f)

Removed support for ``tainted'' certificates. One reason is that there are rarely incremental releases. A stronger reason is that for the compatibility of a new release is with the previous non-incremental release, it's not particularly relevant whether or not the new release is incremental.

The `make' variable BOOKS can now be defined above the line that includes Makefile-generic. (For relevant background, see books-certification-classic.)

(SBCL only) ACL2 images built on SBCL now have an option, --dynamic-space-size 2000, that can avoid space problems that could previously have caused the session to die.

The default value for variable LISP in file GNUmakefile is now ccl. Thus, if you use `make' in the standard way to build an ACL2 executable, the default host Lisp is ccl rather than gcl.

EMACS SUPPORT

EXPERIMENTAL VERSIONS

For the version supporting the reals, ACL2(r) (see real), the supporting function floor1 has been defined in raw Lisp. This avoids an error such as in the following case.

(defun f () (declare (xargs :guard t)) (floor1 8/3))
(f) ; had caused raw Lisp error, before the fix

Among the enhancements for the parallel version, ACL2(p) (see parallelism), are the following. We thank David Rager for his work in developing ACL2(p) and these improvements in particular.

The macro set-parallel-evaluation has been renamed set-parallel-execution.

Calls of the macro set-waterfall-printing are no longer events, so may not be placed at the top level of books. However, it is easy to create events that have these effects; see set-waterfall-printing. Note that now, :ubt and similar commands do not change the settings for either waterfall-parallelism or waterfall-printing.

The implementation of deflock has been improved. Now, the macro it defines can provide a lock when invoked inside a guard-verified or :program mode function. Previously, this was only the case if the function definition was loaded from raw Lisp, typically via a compiled file.

The underlying implementation for waterfall parallelism (see set-waterfall-parallelism) has been improved. As a result, even the largest proofs in the regression suite can be run efficiently in :resource-based waterfall parallelism mode. Among these improvements is one that can prevent machines from rebooting because operating system limits have been exceeded; thanks to Robert Krug for bringing this issue to our attention.

There is also a new flag for configuring the way waterfall parallelism behaves once underlying system resource limits are reached. This flag is most relevant to :full waterfall parallelism. see set-total-parallelism-work-limit for more information.

The dmr utility has the same behavior in ACL2(p) as it has in ACL2 unless waterfall-parallelism has been set to a non-nil value (see set-waterfall-parallelism), in which case statistics about parallel execution are printed instead of the usual information.

The user can now build the regression suite using waterfall parallelism. See the distributed file acl2-customization-files/README for details, and see unsupported-waterfall-parallelism-features for a disclaimer related to building the regression suite using waterfall parallelism.

When building ACL2 with both the hons and parallelism extensions (what is called ``ACL2(hp)''), the functions that are automatically memoized by the hons extension are now automatically unmemoized and memoized when the user toggles waterfall parallelism on and off, respectively.

Calling set-waterfall-parallelism with a flag of t now results in the same settings as if it were called with a flag of :resource-based, which is now the recommended mode for waterfall parallelism. Thanks to Shilpi Goel for requesting this feature.

The prover now aborts in a timely way in response to interrupts issued during a proof with waterfall parallelism enabled. (This had often not been the case.) Thanks to Shilpi Goel for requesting this improvement.

Among the enhancements for the HONS extension (see hons-and-memoization) are the following.

The compact-print code has been replaced by new serialization routines contributed by Jared Davis. This may improve performance when including books that contain make-events that expand to very large constants. You can also now save objects to disk without going into raw lisp; see serialize for details.

Printing of certain messages has been sped up (by using Lisp function force-output in place of finish-output). Thanks to Jared Davis for contributing this improvement.

Stobj array writes are perhaps twice as fast.

It is now permitted to memoize functions that take user-defined stobjs as inputs, provided that no stobjs are returned. Even if stobjs are returned, memoization is permitted provided the condition is nil, as when profiling (see profile). Thanks to Sol Swords for an observation that led to this improvement and for useful conversations, including follow-up leading us to improve our initial implementation.

Fixes have been made for memoizing with a non-nil value of :ideal-okp. Errors had occurred when memoizing with a :condition other than t for a :logic mode function that had not been guard-verified, even with a non-nil value of :ideal-okp; and after successfully memoizing such a function (without such :condition), it had not been possible to unmemoize it. Thanks to Sol Swords for reporting issues with the :ideal-okp argument of memoize.

If a book defined a function that was subsequently memoized in that book, the function would no longer behaves as memoized upon completion of book certification (unless that certify-book command was undone and replaced by evaluation of a corresponding include-book command). This has been fixed. Thanks to David Rager for pointing out the problem by sending an example.

We now support ACL2(h) built not only on 64-bit CCL but also on all supported host Ansi Common Lisps (i.e., all supported host Lisps except GCL). Thanks to Jared Davis for doing much of the work to make this improvement. Note that performance will likely be best for 64-bit CCL; for some Lisps, performance may be much worse, probably depending in part on the underlying implementation of hash tables.