NOTE-3-5

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 3.4 into the following categories: changes to existing features, new features, heuristic improvements, bug fixes, new and updated books, Emacs support, and experimental hons version. Each change is described in just one category, though of course many changes could be placed in more than one category.

CHANGES TO EXISTING FEATURES

Many improvements have been made to ACL2's ``evisceration'' mechanism for hiding substructures of objects before they are printed, and to related documentation:

o A new documentation topic explains evisc-tuples. See evisc-tuple.

o A new interface, set-evisc-tuple, has been provided for setting the four global evisc-tuples. See set-evisc-tuple.

o A new mode, ``iprinting'', allows eviscerated output to be read back in. See set-iprint.

o Function default-evisc-tuple has been deprecated and will probably be eliminated in future releases; use abbrev-evisc-tuple instead. Also eliminated is the brr-term-evisc-tuple (also the user-brr-term-evisc-tuple). The term-evisc-tuple controls printing formerly controlled by the brr-term-evisc-tuple or user-brr-term-evisc-tuple.

o ACL2 output is done in a more consistent manner, respecting the intention of those four global evisc-tuples. In particular, more proof output is sensitive to the term-evisc-tuple. Again, see set-evisc-tuple.

o A special value, :DEFAULT, may be provided to set-evisc-tuple in order to restore these evisc-tuples to their original settings.

o (Details for heavy users of the evisc-tuple mechanism) (1) There are no longer state globals named user-term-evisc-tuple or user-default-evisc-tuple. (2) Because of the above-mentioned :DEFAULT, if you have referenced state globals directly, you should use accessors instead, for example (abbrev-evisc-tuple state) instead of (@ abbrev-evisc-tuple). (3) For uniformity, set-trace-evisc-tuple now takes a second argument, state.

Improved break-on-error in several ways. First, it breaks earlier in a more appropriate place. Thanks to Dave Greve for highlighting this problem with the existing implementation. Also, break-on-error now breaks on hard errors, not only soft errors (see er, options hard and hard?). Thanks to Warren Hunt and Anna Slobodova for sending an example that showed a flaw in an initial improvement. Finally, new options cause printing of the call stack for some host Common Lisps. See break-on-error. Thanks to Bob Boyer for requesting this feature.

Trace! may now be used in raw Lisp (though please note that all soundness claims are off any time you evaluate forms in raw Lisp!). Thanks to Bob Boyer for feedback that led to this enhancement.

ACL2 now searches for file acl2-customization.lsp in addition to (and just before) its existing search for acl2-customization.lisp; See acl2-customization. Thanks to Jared Davis for suggesting this change, which supports the methodology that files with a .lisp extension are certifiable books (thus avoiding the need to set the BOOKS variable in makefiles; see books-certification-classic).

Improved the error message for illegal declare forms of the form (type (satisfies ...)). Thanks to Dave Greve for sending an example highlighting the issue.

If trace output is going to a file (because open-trace-file has been executed), then a note will be printed to that effect at the time that a call of trace$ or trace! is applied to one or more trace specs.

The notion of redundancy (see redundant-events) has been made more restrictive for mutual-recursion events. Now, if either the old or new event is a mutual-recursion event, then redundancy requires that both are mutual-recursion events that define the same set of function symbols. Although we are not aware of any soundness bugs fixed by this modification, nevertheless we believe that it reduces the risk of soundness bugs in the future.

The definition of trace* has been moved to a book, misc/trace1.lisp. A new version, used in ACL2s, is in book misc/trace-star.lisp. Trace utilities trace$ and trace! are still built into ACL2. [Note: File misc/trace1.lisp was deleted after Version 4.2.]

Certain certificate files will now be much smaller, by printing in a way that takes advantage of structure sharing. Certifying the following example produces a .cert file of over 3M before this change, but less than 1K after the change.

(defun nest (i)
  ;; Makes an exponentially-sized nest of conses i deep.
  (if (zp i)
      nil
    (let ((next (nest (1- i))))
      (cons next next))))

(make-event
 `(defconst *big* ',(nest 20)))

Names of symbols are now printed with vertical bars according to the Common Lisp spec. Formerly, if the first character of a symbol name could be the first character of the print representation of a number, then the symbol was printed using vertical bars (|..|) around its name. Now, a much more restrictive test for ``potential numbers'' is used, which can result in fewer such vertical bars. Base 16 is now carefully considered as well; see set-print-base. Thanks to Bob Boyer for requesting this improvement. Note that macros set-acl2-print-base and set-acl2-print-case have been replaced by functions; see set-print-base and see set-print-case.

The ACL2 reader now supports `#.' syntax in place of the `#, syntax formerly supported. Thanks to Bob Boyer for requesting this change. See sharp-dot-reader. NOTE that because of this change, `#.' no longer causes an abort; instead please use (a!) or optionally, if in the ACL2 loop, :a!; see a!.

Some small changes have been made related to gag-mode:

o Gag-mode now suppresses some messages that were being printed upon encountering disjunctive splits from :OR hints. Thanks to Sol Swords for suggesting this improvement.

o ACL2 had printed ``Q.E.D.'' with all output suppressed and gag-mode enabled. Now, ``Q.E.D.'' will be suppressed when PROVE and SUMMARY output are suppressed, even if gag-mode is enabled.

o The use of set-gag-mode had drastic effects on the inhibited output (see set-inhibit-output-lst), basically inhibiting nearly all output (even most warnings) when turning on gag-mode and enabling all output except proof-tree output when turning off gag-mode. Now, set-gag-mode only inhibits or enables proof (PROVE) output, according to whether gag-mode is being turned on or off (respectively). The related utility set-saved-output has also been modified, basically to eliminate :all as a first argument and to allow t and :all as second arguments, for inhibiting prover output or virtually all output, respectively (see set-saved-output).

A defstub event signature specifying output of the form (mv ...) now introduces a :type-prescription rule asserting that the new function returns a true-listp result. Thanks to Bob Boyer for sending the following example, which motivated this change.

(defstub census (*) => (mv * *))
(defn foo (x)
  (mv-let (a1 a2)
          (census x)
          (list a1 a2)))

Improved the efficiency of string-append so that in raw Lisp, it calls concatenate. Thanks to Jared Davis for suggesting this change, including the use of mbe. A minor change was made to the definition of concatenate to support this change, and the lemma append-to-nil was added (see below).

The checksum algorithm used for certificate files of books has been changed. Thanks to Jared Davis for contributing the new code. This change will likely not be noticed unless one is using the experimental hons version of ACL2, where it can greatly speed up book certification and inclusion because of function memoization (of source function fchecksum-obj).

Fewer calls are made to the checksum algorithm on behalf of certify-book and a few other operations. Thanks to Jared Davis for providing data that helped lead us to these changes.

Formatted printing directives ~p, ~q, ~P, and ~Q are deprecated, though still supported. See fmt. Instead, please use ~x, ~y, ~X, and ~Y (respectively). As a by-product, rule names in proof output are no longer hyphenated.

A new keyword, :multiplicity, is available for tracing raw Lisp functions using the ACL2 trace utility. See trace$.

Users may now control whether or not a slow array access results in a warning printed to the screen (which is the default, as before), and if so, whether or not the warning is followed by a break. See slow-array-warning.

On linux-like systems (including Mac OS X and SunOS), :comp will now write its temporary files into the "/tmp" directory, which is the value of state global 'tmp-dir. You can change that directory with (assign tmp-dir "<your_temp_directory_path>").

The messages printed for uncertified books have been enhanced. Thanks to Jared Davis for requesting such an improvement.

A function definition that would be redundant if in :logic mode is now considered redundant even if it (the new definition) is in :program mode. That is, if a definition is ``downgraded'' from :logic to :program mode, the latter (:program mode) definition is considered redundant. Previously, such redundancy was disallowed, but we have relaxed that restriction because of a scenario brought to our attention by Jared Davis: include a book with the :logic mode definition, and then include a book with the :program mode definition followed by verify-termination. Thanks, Jared.

The ACL2 reader no longer accepts characters other than those recognized by standard-char-p except for #\Tab, #\Page, and #\Rubout (though it still accepts strings containing such characters). As a result, no make-event expansion is allowed to contain any such unacceptable character or string. Thanks to Sol Swords for sending an example that led us to make this restriction. A simple example is the following book:

(in-package "ACL2")
(defconst *my-null* (code-char 0))
(make-event `(defconst *new-null* ,*my-null*))

ACL2 now collects up guards from declare forms more as a user might expect, without introducing an unexpected ordering of conjuncts. We thank Jared Davis for sending us the following illustrative example, explained below.

(defun f (x n)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (= (length x) n)))
           (type string x)
           (ignore x n))
  t)

(and (natp n)
     (= (length x) n)
     (stringp x))

Modified close-output-channel to try to do a better job flushing buffers. Thanks to Bob Boyer for helpful correspondence.

The notion of ``subversive recursion'' has been modified so that some functions are no longer marked as subversive. See subversive-recursions, in particular the discussion elaborating on the notion of ``involved in the termination argument'' at the end of that documentation topic.

Formerly, :type-prescription rules for new definitions inside encapsulate forms were sometimes added as constraints. This is no longer the case. See also discussion of the ``soundness bug in the forming of constraints'', which is related.

NEW FEATURES

It is now possible to affect ACL2's termination analysis (and resulting induction analysis). Thanks to Peter Dillinger for requesting this feature. The default behavior is essentially unchanged. But for example, the following definition is accepted by ACL2 because of the use of the new :ruler-extenders features; See ruler-extenders.

  (defun f (x)
    (declare (xargs :ruler-extenders :all))
    (cons 3
          (if (consp x)
              (f (cdr x))
            nil)))

The following lemma was added in support of the improvement to string-append described above:

(defthm append-to-nil
  (implies (true-listp x)
           (equal (append x nil)
                  x)))

A mechanism has been provided for users to contribute documentation. See managing-acl2-packages for an example, which contains a link to an external web page on effective use of ACL2 packages, kindly provided by Jared Davis. ACL2 documentation strings may now link to external web pages using the new symbol, ~url; see markup. Of course, those links appear in the web version of the documentation, but you made need to take a bit of action in order for these to appear as links in the Emacs Info version; see documentation.

Added intersectp (similar to intersectp-eq and intersectp-equal).

The user now has more control over how ACL2 prints forms; See print-control. Thanks to Bob Boyer for useful discussions leading to this enhancement.

Some Common Lisp implementations only allow the syntax pkg-name::expression when expression is a symbol. The ACL2 reader has been modified to support a package prefix for arbitrary expressions; see sharp-bang-reader. Thanks to Hanbing Liu for a query that led to this feature and to Pascal J. Bourguignon for suggesting an implmentation.

Ill-formed documentation strings need not cause an error. See set-ignore-doc-string-error. Thanks to Bob Boyer for requesting this feature.

Type declarations are now permitted in let* forms; see let*, see declare, and see type-spec.

(For Lisp programmers) Macro with-live-state has been provided for programmers who refer to free variable STATE, for example with macros that generate uses of STATE, and want to avoid compiler warnings when evaluating in raw Lisp. For example, the following form can be submitted either inside or outside the ACL2 loop to get the desired effect (see doc-string): (with-live-state (f-put-global 'doc-prefix " " state)). For another example use of this macro, see the definition of trace$ (ACL2 source file other-events.lisp).

(System hackers only) Added :redef- to undo the effect of :redef+. See redef-.

Function random$ is a built-in random number generator. See random$. Thanks to Sol Swords for requesting this feature and providing an initial implementation.

HEURISTIC IMPROVEMENTS

Sped up guard generation for some functions with large if-then-else structures in their bodies. Thanks to Sol Swords for sending an illustrative example.

Sped up guard generation in some cases by evaluating ground (variable-free) subexpressions. Thanks to Bob Boyer for sending a motivating example: (defn foo (x) (case x ((1 2) 1) ((3 4) 3) ... ((999 1000) 999))).

Modified slightly a heuristic association of ``size'' with constants, which can result in significant speed-ups in proofs involving constants that are very large cons trees.

Added a restriction in the linear arithmetic procedure for deleting polynomial inequalities from the linear database. Formerly, an inequality could be deleted if it was implied by another inequality. Now, such deletion requires that certain heuristic ``parent tree'' information is at least as restrictive for the weaker inequality as for the stronger. Thanks to Dave Greve for bringing a relevant example to our attention and working with us to figure out some surprising behavior, and to Robert Krug for making a key observation leading to the fix.

(GCL especially) Improved compiled code slightly by communicating to raw Lisp the output type when a function body is of the form (the character ...). This tiny improvement will probably only be observed in GCL, if at all.

Applied a correction suggested by Robert Krug to the variant of term-order used in parts of ACL2's arithmetic reasoning.

BUG FIXES

Fixed bugs in the handling of flet expressions, one of which had the capability of rendering ACL2 unsound. Thanks to Sol Swords for pointing out two issues and sending examples. One example illustrated how ACL2 was in essence throwing away outer flet bindings when processing an inner flet. We have exploited that example to prove a contradiction, as follows: this book was certifiable before this fix.

(in-package "ACL2")

(defun a (x)
  (list 'c x))

; Example from Sol Swords, which failed to be admitted (claiming that
; function A is undefined) without the above definition of A.
(defun foo1 (x y)
   (flet ((a (x) (list 'a x)))
     (flet ((b (y) (list 'b y)))
       (b (a (list x y))))))

(defthm not-true
  (equal (foo1 3 4)
         '(b (c (3 4))))
  :hints (("Goal"
           :in-theory
           (disable (:executable-counterpart foo1))))
  :rule-classes nil)

(defthm contradiction
  nil
  :hints (("Goal" :use not-true))
  :rule-classes nil)

:trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)

Fixed a subtle soundness bug in the forming of constraints from deduced type prescriptions. As a result, when ACL2 prints a warning message labeling encapsulated functions as ``subversive'', ACL2 will no longer deduce :type-prescription rules for those functions. Examples that exploit the bug in ACL2 Version_3.4 may be found in comments in ACL2 source function convert-type-set-to-term (file other-processes.lisp) and especially in function putprop-type-prescription-lst (file defuns.lisp). For more on the general issue of ``subversive recursions,'' see subversive-recursions.)

Fixed a soundness bug in the handling of inequalities by the type-set mechanism, which was using the inequality database inside the body of a lambda.

Fixed a long-standing soundness bug in compress1 and compress2, whose raw Lisp code gave the logically incorrect result in the case of a single entry other than the header, where that entry mapped an index to the default value. Also fixed soundness bugs in compress1, in the case of :order >, where the raw Lisp code could drop the header from the result or, when the input alist had entries in ascending order, fail to return an alist in descending order. For example, the following book certified successfully.

(in-package "ACL2")
(defthm true-formula-1
  (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                  :DEFAULT 1 :NAME A :ORDER <)
                         (1 . 1)))
         '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                    :DEFAULT 1 :NAME A :ORDER <)))
  :hints (("Goal" :in-theory (disable (compress1))))
  :rule-classes nil)
(defthm ouch-1
  nil
  :hints (("Goal" :use true-formula-1))
  :rule-classes nil)
(defthm true-formula-2
  (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                  :DEFAULT NIL :NAME A :ORDER >)
                         (1 . 1)
                         (2 . 2)))
         '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                    :DEFAULT NIL :NAME A :ORDER >)
           (2 . 2)
           (1 . 1)))
  :hints (("Goal" :in-theory (disable (compress1))))
  :rule-classes nil)
(defthm ouch-2
  nil
  :hints (("Goal" :use true-formula-2))
  :rule-classes nil)
(defthm true-formula-3
  (equal (compress1 'a '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                                  :NAME A :ORDER >)
                         (1 . B)
                         (0 . A)))
         '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                    :NAME A :ORDER >)
           (1 . B)
           (0 . A)))
  :hints (("Goal" :in-theory (disable (compress1))))
  :rule-classes nil)
(defthm ouch-3
  nil
  :hints (("Goal" :use true-formula-3))
  :rule-classes nil)

Fixed a soundness bug involving measured subsets and verify-termination, by changing verify-termination so that it uses make-event. See verify-termination, in particular the discussion about make-event near the end of that documentation topic. Peter Dillinger first raised the idea to us of making such a change; when we found this soundness bug, we were certainly happy to do so!

Fixed a bug that could cause a hard Lisp error but not, apparently, unsoundness. The bug was in the lack of attention to the order of guard and type declarations when checking for redundancy. In the following example, the second definition was redundant during the first pass of the encapsulate form. The second definition, however, was stored on the second pass with a guard of (and (consp (car x)) (consp x)), which caused a hard Lisp error when evaluating (foo 3) due to a misguided attempt to evaluate (car 3) in raw Lisp. The fix is to restrict redundancy of definitions so that the guard and type declarations must be in the same order for the two definitions.

(encapsulate
 ()
 (local (defun foo (x)
          (declare (xargs :guard (consp x)))
          (declare (xargs :guard (consp (car x))))
          x))
 (defun foo (x)
   (declare (xargs :guard (consp (car x))))
   (declare (xargs :guard (consp x)))
   x))
; Now we get a hard Lisp error from evaluation of the guard of foo:
(foo 3)

Fixed a bug in the guard violation report for function intern-in-package-of-symbol. Thanks to Dave Greve for bringing this bug to our attention.

Made a change to allow certain hints, in particular certain :clause-processor hints, that had previously caused errors during termination proofs by viewing the function being defined as not yet existing. Thanks to Sol Swords for bringing this issue to our attention with a nice example.

ACL2 now properly handles interrupts (via control-c) issued during printing of the checkpoint summary. Previously it was possible on some platforms to make ACL2 hang when interrupting both during a proof and during the ensuing printing of the checkpoint summary. Thanks to Jared Davis and Sol Swords for bringing this problem to our attention.

Fixed a bug that was preventing, inside some book "b", the use of a :dir argument to include-book that refers to a directory defined using add-include-book-dir earlier in the book "b". (We found this ourselves, but we thank John Cowles for observing it independently and sending us a nice example.)

(GCL and CCL only) Fixed a bug in certain under-the-hood type inferencing. Thanks to Sol Swords for sending an example using stobjs defined with the :inline keyword, along with a helpful backtrace in CCL, and to Gary Byers for his debugging help.

Fixed a bug in print-gv, which was mishandling calls of functions with more than one argument.

Fixed a bug in the handling of AND and OR terms by the proof-checker command DV, including numeric (``diving'') commands. Thanks for Mark Reitblatt for bringing this problems to our attention with a helpful example.

Fixed printing of goal names resulting from the application of :OR hints so that they aren't ugly when working in other than the "ACL2" package. Thanks to Sol Swords for bringing this issue to our attention.

Fixed proof-tree printing so that interrupts will not cause problems with hiding ordinary output because of incomplete proof-tree output. Thanks to Peter Dillinger for pointing out this issue.

Fixed a hard error that could be caused by mishandling a forced hypothesis during forward-chaining. Thanks to Peter Dillinger for bringing this bug to our attention by sending a useful example.

Fixed a bug that could cause simplifications to fail because of alleged ``specious simplification.'' This bug could appear when deriving an equality from the linear arithmetic database, and then attempting to add this equality to the current goal's hypotheses when it was already present. Thanks to Eric Smith for sending a helpful example (in July 2005!) that helped us debug this issue.

Fixed a bug in processing of :type-set-inverter rules.

Fixed a bug that was causing an error, at least for an underlying Lisp of CCL (OpenMCL), when ec-call was applied to a term returning multiple values. Thanks to Sol Swords for sending an example that brought this bug to our attention.

Fixed handling of array orders to treat keyword value :order :none correctly from an array's header. Previously, there were two problems. One problem was that :order :none was treated like the default for :order, <, while :order nil was treated in the manner specified by :order :none (see arrays). Now, both :order :none and :order nil are treated as :order nil had been treated, i.e., so that there is no reordering of the alist by compress1. The other problem with this case of :order was that the :maximum-length field of the header was not being respected: the length could grow without bound. Now, as previously explained (but not previously implemented) -- see arrays -- a compress1 call made on behalf of aset1 causes a hard error if the header of the supplied array specifies an :order of :none or nil.

An ignorable declare form had caused an error in some contexts when it should have been allowed. In particular, this problem could arise when using an ignorable declaration at the top level in a defabbrev form. It could also arise upon calling verify-termination when the corresponding defun form contained an ignorable declaration at the top level. These bugs have been fixed.

Contrary to existing documentation (see make-event-details), the value of ``ld special variable'' ld-skip-proofsp was always set to nil during make-event expansion, not merely when the make-event form has a non-nil value for keyword parameter :check-expansion. This has been fixed. Thanks to Sol Swords for bringing this issue to our attention.

We have disallowed the certification of a book when not at the top-level, either directly in the top-level loop or at the top level of ld. Before this restriction, the following would certify a book with a definition such as (defun foo (x) (h x)) that calls function h before defining it, if the certification was by way of the form such as:

(er-progn (defun h (x) x) (certify-book "my-book"))

Printing with fmt directive ~c now works properly even when the print-base is other than 10. Thanks to Sol Swords for reporting this bug and providing a fix for it.

(SBCL, CMUCL, and CCL only) Fixed a bug in sys-call-status in the case that the underlying Common Lisp is SBCL, CMUCL, or CCL (OpenMCL). Thanks to Jun Sawada for bringing this bug to our attention and providing a fix.

Fixed a bug that was preventing local defstobj events in encapsulate events. Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug evidenced by error message ``Unexpected form in certification world'', which could result from attempting to certify a book after evaluating an encapsulate form with a local defmacro. Thanks to Jared Davis for pointing out this bug and sending the example:

(encapsulate
 ()
 (local (defmacro foo (x) `(table foo 'bar ,x)))
 (local (foo 3)))

Formerly, evaluating a trace$ form inside a wormhole such as the break-rewrite loop could leave the user in a bad state after returning to the top level, in which that function could not be untraced. This has been fixed. Note however that when you proceed from a break in the break-rewrite loop, the tracing state will be the same as it was when you entered that break: all effects of calling trace$ and untrace$ are erased when you proceed from the break.

A :guard of (and) is no longer ignored. Thanks to Sol Swords for bringing this bug to our attention.

A bug has been fixed that could result in needlessly weak induction schemes in the case that a recursive call is made in the first argument of prog2$. This has been fixed by including prog2$ as a default ruler-extender in the new ruler-extenders feature (see above, and see ruler-extenders). For details on this bug see Example 11 in distributed book books/misc/misc2/ruler-extenders-tests.lisp.

(For CCL/OpenMCL on Windows) ACL2 should now build on CCL (OpenMCL) on Windows. Thanks to David Rager for bringing this issue to our attention and helping with a fix that worked for CCL 1.2, and to the CCL team for improving handling of Windows-style filenames in CCL 1.3.

NEW AND UPDATED BOOKS

See http://code.google.com/p/acl2-books/wiki/BooksSince34 for a list of books in Version 3.5 of ACL2 but not Version 3.4.

Run the shell command

svn log -r 94:HEAD

Here are just a few highlights.

Thanks largely to Jared Davis, many Makefiles have been improved to do automatic dependency analysis. See books-certification-classic for how to get your own Makefiles to do this by adding a line: -include Makefile-deps.

Libraries books/arithmetic-4/ and books/rtl/rel7/ have been eliminated from the default book certification (make regression), in favor of new libraries books/arithmetic-5/ and books/rtl/rel8/ contributed by Robert Krug and Hanbing Liu, respectively. They and Jun Sawada have arranged the compatibility of these libraries; i.e., it is possible to evaluate both of the following in the same session:

(include-book "arithmetic-5/top" :dir :system)
(include-book "rtl/rel8/lib/top" :dir :system)

Library books/rtl/rel1/ is no longer certified by default (though it is still distributed in support of ACL2(r); see real).

EMACS SUPPORT

Slightly modified Control-t e (defined in emacs/emacs-acl2.el) to comprehend the notion of an ``ACL2 scope'', and added Control-t o to insert a superior encapsulate defining such a scope. See the Emacs documentation for Control-t e (generally obtained after typing Control-h k).

Modified distributed file emacs/emacs-acl2.el so that if you put the following two forms in your ~/.emacs file above the form that loads emacs/emacs-acl2.el, then Emacs will not start up a shell. Thanks to Terry Parks for leading us to this modification.

(defvar acl2-skip-shell nil)
(setq acl2-skip-shell t)

EXPERIMENTAL HONS VERSION

Bob Boyer and others have contributed numerous changes for the experimental ``hons'' version of ACL2 (see hons-and-memoization).

The ACL2 state can now be queried with (@ hons-enabled) so that a result of t says that one is in the experimental hons version, while nil says the opposite.