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
hons version. Each change is described in just one
category, though of course many changes could be placed in more than one
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.
default-evisc-tuplehas been deprecated and will probably be eliminated in future releases; use
abbrev-evisc-tupleinstead. 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-tuplein 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-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-tuplenow takes a second argument,
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
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
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 book-makefiles).
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! is applied to one or more trace
The notion of redundancy (see redundant-events) has been made more
mutual-recursion events. Now, if either the old or new
event is a
mutual-recursion event, then redundancy requires that both
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,
A new version, used in ACL2s, is in book
trace! are still built into
Certain certificate files will now be much smaller, by printing in a way
that takes advantage of structure sharing. Certifying the following example
.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))))Thanks to Sol Swords for providing the above example and to him as well as to Bob Boyer, Jared Davis, and Warren Hunt for encouraging development of this improvement. We have also applied this improvement to the printing of function definitions to files on behalf of
(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
been replaced by functions; see set-print-base and see set-print-case.
The ACL2 reader now supports `
#.' syntax in place of the `
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
: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
:ORhints. Thanks to Sol Swords for suggesting this improvement.
o ACL2 had printed ``
Q.E.D.'' with all output suppressed and
gag-modeenabled. Now, ``
Q.E.D.'' will be suppressed when
SUMMARYoutput are suppressed, even if
o The use of
set-gag-modehad 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-treeoutput when turning off gag-mode. Now,
set-gag-modeonly inhibits or enables proof (
PROVE) output, according to whether gag-mode is being turned on or off (respectively). The related utility
set-saved-outputhas also been modified, basically to eliminate
:allas a first argument and to allow
:allas second arguments, for inhibiting prover output or virtually all output, respectively (see set-saved-output).
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
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
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
deprecated, though still supported. See fmt. Instead, please use
~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),
now write its temporary files into the
"/tmp" directory, which is the
'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
: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
(though it still accepts strings containing such characters). As a result,
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*))For this book, a call of
certify-bookformerly broke during the compilation phase, but if there was no compilation, then a call of
include-bookbroke. Now, the error occurs upon evaluation of the
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,
(defun f (x n) (declare (xargs :guard (and (stringp x) (natp n) (= (length x) n))) (type string x) (ignore x n)) t)Formerly, a guard was generated for this example by unioning the conjuncts from the
:guardonto a list containing the term
(string x)generated from the
typedeclaration, resulting in an effective guard of:
(and (natp n) (= (length x) n) (stringp x))The guard of this guard failed to be verified because
(stringp x))now comes after the call
(length x). With the fix, contributions to the guards are collected up in the order in which they appear. So in the above example, the effective guard is the specified
:guard; the contribution
(stringp x)comes later, and is thus dropped since it is redundant. NOTE by the way that if
:stobjsare specified in the same
xargsform, then for purposes of collecting up the effective guard as described above,
:stobjswill be treated as through it comes before the
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.
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.
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;
intersectp (similar to
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
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
(with-live-state (f-put-global 'doc-prefix " " state)).
For another example use of this macro, see the definition
trace$ (ACL2 source file
(System hackers only) Added
redef- to undo the effect of
redef+. See redef-.
random$ is a built-in random number generator. See random$.
Thanks to Sol Swords for requesting this feature and providing an initial
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
(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
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.
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")Sol's second example, below, pointed to a second bug related to computing output signatures in the presence of nested
(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)
fletexpressions, which we have also fixed: this form failed before the fix.
: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
especially in function
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
Fixed a long-standing soundness bug in
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
default value. Also fixed soundness bugs in
the case of
:order >, where the raw Lisp code could drop the
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
(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 so that it uses
See verify-termination, in particular the discussion about
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
(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
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
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
: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
OR terms by the
DV, including numeric (``diving'') commands.
Thanks for Mark Reitblatt for bringing this problems to our attention with a
Fixed printing of goal names resulting from the application of
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
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
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
Fixed a bug that was causing an error, at least for an underlying Lisp of CCL
ec-call was applied to a term returning multiple
values. Thanks to Sol Swords for sending an example that brought this bug to
Fixed handling of array orders to treat keyword value
correctly from an array's
header. Previously, there were two problems.
One problem was that
:order :none was treated like the default for
:order nil was treated in the manner specified
: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
declare form had caused an error in some contexts when
it should have been allowed. In particular, this problem could arise when
ignorable declaration at the top level in a
form. It could also arise upon calling
verify-termination when the
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
make-event expansion, not merely when the
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
Before this restriction, the following would certify a book with a definition
(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"))But a subsequent
"my-book"would then fail, because
his not defined at the top level.
~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
defstobj events in
encapsulate events. Thanks to Jared Davis for bringing this bug to our
Fixed a bug evidenced by error message ``Unexpected form in certification
world'', which could result from attempting to certify a book after
encapsulate form with a local
defmacro. Thanks to
Jared Davis for pointing out ths 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
untrace$ are erased when you proceed from the break.
(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
(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
to see all changes to
svn log -r 94:HEAD
books/since the release of Version 3.4.
Here are just a few highlights.
Thanks largely to Jared Davis, many
Makefiles have been improved to do
automatic dependency analysis. See book-makefiles for how to get your own
Makefiles to do this by adding a line:
books/rtl/rel7/ have been
eliminated from the default book certification (
make regression), in
favor of new libraries
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)
books/rtl/rel1/ is no longer certified by default (though it is
still distributed in support of ACL2(r); see real).
Control-t e (defined in
comprehend the notion of an ``ACL2 scope'', and added
Control-t o to
insert a superior
encapsulate defining such a scope. See the Emacs
Control-t e (generally obtained after typing
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).
state can now be queried with
(@ hons-enabled) so that a
t says that one is in the experimental
hons version, while
nil says the opposite.