Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1
Matt Kaufmann
J Strother Moore
We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we focus in this paper on those improvements that could benefit users who are aware of them, but that might not be discovered in everyday practice.
bug.tex
\section{Bug fixes}

We have continued to improve ACL2 by eliminating more than 50 bugs.
In this section we mention only a few that may have the most effect on
how people use ACL2.

%########## 5.0

% 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 :DOC WITH-LIVE-STATE, as the documentation for this macro has been updated; in
% particular it is now untouchable (see :DOC 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 :DOC 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)))
% 
% For those who want details about this bug, we analyze how ACL2 generates
% guard proof obligations for this example.  During that process, it
% evaluates ground subexpressions.  Thus, (identity '3) is first simplified
% to '3; so a term must be built from the application of car to '3.
% Guard-checking is always turned on when generating guard proof obligations,
% so now, ACL2 refuses to simplify (car '3) to 'nil.  However, before
% this bug fix, when ACL2 was building a term by applying car to argument
% '3, it did so directly without checking guards; source code function
% cons-term is `smart' that way.  After the fix, such term-building
% reduction is only performed when the primitive's guard is met.

% 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!
% 
% Thus, several event macros (including for example
% add-custom-keyword-hint) may no longer be called inside executable
% code.

% 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 :DOC 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).

%%% See also item ``the times displayed in the summary'' below, which
%%% pertains to certify-book.  We cover that one here as well.

The time reports in event summaries have been much improved.  As far
as we know, they now accurately report runtime (cpu time).  Of course,
you can use the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/TIME$.html}{\underline{\texttt{TIME\$}}}%$
utility for reports of realtime and
runtime that avoid the accounting done by ACL2.

% 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)))

The
\href{http://www.cs.utexas.edu/users/moore/acl2/current/FLET.html}{\underline{\texttt{FLET}}}
construct no longer has any requirements for returning stobjs.

% We fixed a bug, introduced in the preceding release (Version  4.3), in the
% check for irrelevant formals (see :DOC 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 :DOC 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 :DOC 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 :DOC SHARP-BANG-READER) was broken after a skipped
% readtime conditional.  For example, the following input line caused an
% error.
% 
% #+skip #!acl2(quote 3)
% 
% This bug has been fixed.

% 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.

%########## 6.0

% Fixed a soundness bug in defabsstobj based on guards that
% violated single-threadedness restrictions.  Thanks to Sol Swords for bringing
% this bug to our attention and supplying a proof of nil, which we include
% as a comment in source file ld.lisp, in (deflabel note-6-0 ...).  We
% also thank Sol for helpful discussions about guards of functions
% introduced by defabsstobj, which has led us to enhance the
% documentation; see :DOC DEFABSSTOBJ.

% Fixed a soundness bug in defabsstobj based on interrupted updates of
% abstract stobjs.  As part of the fix a new keyword, :PROTECT, has been
% introduced for defabsstobj exports, along with a new top-level
% defabsstobj keyword, :PROTECT-DEFAULT; see :DOC DEFABSSTOBJ.  We do some
% analysis that we expect will avoid the use of :PROTECT in many cases,
% which is fortunate since the use of :PROTECT t may cause a slight
% slowdown in (abstract) stobj updates.  Thanks to Sol Swords for bringing this
% bug to our attention and supplying a proof of nil, which we include as a
% comment in source file other-events.lisp, in the definition of function
% set-absstobj-debug.

%%% The one above is interesting, but not worth a mention since
%%% defabsstobj was only introduced in 5.0.

% Fixed a raw Lisp error that occurred when tracing a stobj resize
% function, thanks to an error report from Warren Hunt, Marijn Heule, and
% Nathan Wetzler.

% Fixed a raw Lisp error that occurred for certain ill-formed signatures, as in
% the following example.
% 
% ACL2 !>(encapsulate
%            (((f (*) => * :guard t)))
%            (local (defun f (x) (consp x))))
% 
% ***********************************************
% ************ ABORTING from raw Lisp ***********
% Error:  value (F (*) => * :GUARD T) is not of the expected type SYMBOL.
% ***********************************************

% The notion of ``error triple'' (see :DOC ERROR-TRIPLES) had been implemented
% ambiguously, with the result that for a stobj, st, the result of
% evaluating the following two forms was the same: (mv nil st state) and
% (mv t st state).  Of course, these are just examples; in general, a
% result of (mv erp val state) was sometimes treated as an error triple
% even when val is a stobj.  Now, (mv erp val state) is an error
% triple only when erp and val are ordinary (non-stobj) values.
% Thanks to Warren Hunt and Marijn Heule for bringing this problem to our
% attention.

% The ``with-error-trace'' utility, wet, now works in the non-error case
% when given a form that returns multiple values.  (Note however that
% STATE will be printed as REPLACED-STATE; and similarly, a
% user-defined stobj, say ST, will be printed as REPLACED-ST.)

%%% See changes.tex.

% Some possible error messages for defabsstobj have been fixed that had
% been ill-formed.  Thanks to Sol Swords for bringing this bug to our
% attention.

% Fixed a bug that sometimes caused the times displayed in the summary for
% certify-book to be smaller than the actual times.

%%% This has been combined with the item above about ``Fixed a bug in
%%% the reporting of times''.

% Fixed a bug in the guards to system functions fmt-char and
% fmt-var, which are no longer :logic-mode, guard-verified
% functions.

% (GCL only) Fixed a bug present in Gnu Common Lisp for
% #u (see :DOC SHARP-U-READER).

%########## 6.1

% A soundness bug has been fixed that exploited the use of expansion files
% (see :DOC BOOK-COMPILED-FILE) together with defstobj.  For an example
% illustrating this bug, see the comment about ``Expansion/Defstobj Bug'' in
% the form (deflabel note-6-1 ...) in ACL2 source file ld.lisp.

% We fixed a soundness bug involving system function canonical-pathname
% and (most likely) other functions in the value of constant
% *unattachable-primitives*.  Thanks to Jared Davis and Sol Swords for
% bringing this bug to our attention by way of an example.  We include a very
% slight variant of that example in a comment within the form
% (deflabel note-6-1 ...) in ACL2 source file ld.lisp.

%%% Note: A fix for the bug above is essentially done (I think) but
%%% not yet in svn, as of 2/6/13.

% (ACL2(h) only) We fixed a soundness bug in the interaction of memoization
% with congruent stobjs, in cases where the :congruent-to field of
% defstobj was not the canonical representative in the congruence class.
% For an example illustrating this bug, see the comment about
% ``memoize/congruent stobj bug'' in the form (deflabel note-6-1 ...)  in
% ACL2 source file ld.lisp.

% Functions defined by defstobj had failed to be compiled when certifying
% books, except in host Lisps that compile on-the-fly (CCL, SBCL).  This has
% been fixed for all host Lisps.  A related change, probably less significant,
% was made for defabsstobj.  Thanks to Sol Swords for reporting bugs that
% turned out to be mistakes in a preliminary implementation of this change.

% Fixed an assertion error involving linear arithmetic.  Thanks to Sol Swords
% for sending an example illustrating the bug (now appearing as a comment in
% ACL2 source function linearize1).

% Fixed a bug that was breaking the ACL2s build mechanism (see :DOC ACL2-SEDAN) by
% causing certain needless evaluation of ``hidden defpkg'' forms in
% certificate files when executing a call of include-book.  The bug
% could also affect rare error messages arising from ill-formed
% certificate files.  Thanks to Harsh Raju Chamarthi for bringing this bug
% to our attention by sending us an example script of the sort that was
% breaking during an ACL2s build.

% Fixed handling of pathnames by some low-level code (system function
% our-truename) that could cause errors, for example for host-Lisp GCL on
% some platforms when environment variable HOME points to a non-existent
% directory.  Thanks to Camm Maguire for bringing this issue to our attention
% and helping with the debugging.

% Fixed a coding bug in generation of stobj resizing functions for a stobj
% named OLD.  The following example illustrates the bug.
% 
% (defstobj old
%   (fld :type (array (unsigned-byte 31) (8))
%         :initially 0 :resizable t))
% (resize-fld 10 old)
% ; The following returned 8 but should have returned 10:
% (fld-length old)

% Fixed a bug in defabsstobj-missing-events (which macroexpanded
% incorrectly).  Thanks to Sol Swords for bringing this bug to our attention.

%%% Maybe the item above is worth mentioning, but I'll skip it since
%%% abstract stobjs were only introduced in 5.0.

changes.tex
\section{Changes to existing features}

There are over 50 release note items about changes to existing features.
Here we list a few and then present a few others in a bit more detail.

\begin{itemize}

\item Functions \texttt{READ-ACL2-ORACLE},
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/READ-RUN-TIME.html}{\underline{\texttt{READ-RUN-TIME}}},
  \texttt{GET-TIMER}, and \texttt{MAIN-TIMER} are no longer
  untouchable; you can call them in your programs.

\item Macros can take an argument named \texttt{STATE}, or which is
  the name of a
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/STOBJ.html}{stobj}.
  However, these variables are not bound to the ``live objects'' as
  you might expect but are treated just like other macro variables.

\item The macros
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/MEMOIZE.html}{\underline{\texttt{MEMOIZE}}}
  and
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/UNMEMOIZE.html}{\underline{\texttt{UNMEMOIZE}}}
  now cause a warning rather than an error in (regular, non-HONS)
  ACL2.

\item The macro
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUND.html}{\underline{\texttt{DEFUND}}}
may now be used without error with
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUND.html}{\underline{PROGRAM}}}
mode specified in an
\href{http://www.cs.utexas.edu/users/moore/acl2/current/XARGS.html}{\underline{\texttt{XARGS}}}
declaration.

\item The functions
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SYS-CALL.html}{\underline{\texttt{SYS-CALL}}}
and
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SYS-CALL-STATUS.html}{\underline{\texttt{SYS-CALL-STATUS}}}
are now
\href{http://www.cs.utexas.edu/users/moore/acl2/current/GUARD.html}{\underline{guard}}-verified
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/LOGIC.html}{\underline{\texttt{LOGIC}}}}
mode functions.

\item The environment variable \texttt{ACL2\_COMPILE\_FLG} provides a
default for
\href{http://www.cs.utexas.edu/users/moore/acl2/current/CERTIFY-BOOK.html}{\underline{\texttt{CERTIFY-BOOK}}};
it was formerly named
\texttt{COMPILE\_FLG}.

\end{itemize}

\noindent {\em Some other changes} \\

%########## 5.0

% 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 :DOC REMOVE-UNTOUCHABLE).

%%% added \item

% 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 :DOC 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.

It has been the case since Version 3.6 (August, 2009) that the
definition of a function symbol can mention that symbol in the guard
and measure.  Now, guards specified in
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ENCAPSULATE.html}{\underline{\texttt{ENCAPSULATE}}}
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SIGNATURE.html}{signatures}
may
similarly refer to the functions being introduced in the same
\texttt{ENCAPSULATE} event.

% The test for redundancy (see :DOC REDUNDANT-EVENTS) of encapsulate
% events has been improved in cases involving redefinition
% (see :DOC 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 :DOC 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 :DOC 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))
% 
% Previously, ACL2 complained that it could not determine the outputs of the
% LET form, as is necessary in order to ensure that STATE is
% returned by it.  ACL2 now works harder to solve this problem as well as the
% analogous problem for MV-LET and, more generally for
% mutual-recursion.  (The main idea is to reverse the order of processing
% the IF branches if necessary.)  We thank Sol Swords for contributing a
% version of the above example and requesting this improvement.

% 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 :DOC 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 :DOC CERTIFY-BOOK.

%%% added \item

% 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 :DOC EQUALITY-VARIANTS for relevant background).  Thanks to Jared Davis for
% reporting this problem by sending the above example.

Some utilities have been improved, so you might want to try them again
even if you gave up on them in the past.  For example, consider
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PL.html}{\underline{\texttt{PL}}}}
applied to a non-symbol.  It didn't work for macro calls, but now it
performs macroexpansion (and other transformations to internal form)
as a first step; and moreover, among the rule classes that it shows is
now the \texttt{:LINEAR} class.  Another utility that has been
improved is
\href{http://www.cs.utexas.edu/users/moore/acl2/current/TOP-LEVEL.html}{\underline{\texttt{TOP-LEVEL}}},
which no longer causes calls of
\href{http://www.cs.utexas.edu/users/moore/acl2/current/LD.html}{\underline{\texttt{LD}}}
to stop.  The ``with-error-trace'' utility,
\href{http://www.cs.utexas.edu/users/moore/acl2/current/WET.html}{\underline{\texttt{WET}}},
has also been improved.  Finally, if you haven't yet tried
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFATTACH.html}{\underline{\texttt{DEFATTACH}}},
because your code seemed to run a bit slowly using attachments,
consider trying again, as efficiency has improved for this utility.

% 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.

%%% Regarding the above item: I expect that we'll talk more generally
%%% about the mechanism for user contribution to verification of
%%% termination and guards for system functions.

% 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 :DOC 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 :DOC SET-GAG-MODE.  (As before, see :DOC 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 :DOC 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.

The abbreviated proof output offered by {\em gag-mode} is now on by
default.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SET-GAG-MODE.html}{\texttt{SET-GAG-MODE}}
for a description of gag-mode.  If you want a bit of control over the
printing of induction schemes and guard conjectures in gag-mode, see
the discussion of \texttt{:GAG-MODE} in :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SET-EVISC-TUPLE.html}{\texttt{SET-EVISC-TUPLE}}.

% An error now occurs if ld is called while loading a compiled book.
% See :DOC 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.]
% 
% 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 :DOC 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.

%%% Already covered above.

% 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))
% 
% After certifying this book and then including it in a new session, the
% behavior occurred that is displayed below; notice the mention of BAR.
% However, if the two forms were submitted directly in the loop, then the error
% message had mentioned FOO instead of BAR.  This discrepancy has been
% eliminated, by rejecting the proposed definition of foo because the name
% in the first argument of throw-nonexec-error was 'bar where now it
% must be 'foo.
% 
% 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 motiviated 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))
% 
% Formerly, evaluation of this form had caused a guard violation in the ACL2
% loop unless guard-checking was off (i.e., set-guard-checking was
% involked with nil or :none), in which case it returned (3 2).
% But we observed evaluation of this form to return (3 2 . 7) in every host
% Lisp on which ACL2 runs (Allegro CL, CCL, CLISP, CMUCL, GCL, LispWorks, and
% SBCL).  Now, ACL2 behaves like these Lisps.

% 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 :DOC 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.)

For a macro \texttt{mac}, you can now add a pair \texttt{(mac . fn)}
to the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/MACRO-ALIASES-TABLE.html}{\underline{\texttt{MACRO-ALIASES-TABLE}}}
even when \texttt{fn} has not been
defined as a function symbol.  This can be useful if you want to
define a set of macros early.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ADD-MACRO-ALIAS.html}{\texttt{ADD-MACRO-ALIAS}}.

%########## 6.0

% Function fmt-to-string and similar functions (see :DOC PRINTING-TO-STRINGS)
% now use the default right margin settings; formerly the right margin had been
% set at 10,000.  If you want the former behavior, you can use the
% :fmt-control-alist, as illustrated below.
% 
% (fmt-to-string "~x0"
%                (list (cons #\0 (make-list 30)))
%                :fmt-control-alist
%                `((fmt-soft-right-margin . 10000)
%                  (fmt-hard-right-margin . 10000)))

When functions such as \texttt{FMT-TO-STRING} (see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PRINTING-TO-STRINGS.html}{printing-to-strings})
was introduced in Version 4.3, it printed with a right margin set to
10,000, but now the default right margin settings are used.  Thus, for
example, the string returned as shown below had no newline characters
in Version 4.3.  We can return to the default behavior as shown.

{\footnotesize
\begin{verbatim}
ACL2 !>(fmt-to-string "~x0"
                      (list (cons #\0 (make-list 20))))
(0
 "
(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
     NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
")
ACL2 !>(fmt-to-string "~x0"
                      (list (cons #\0 (make-list 20)))
                      :fmt-control-alist
                      `((fmt-soft-right-margin . 10000)
                        (fmt-hard-right-margin . 10000)))
(81
 "
(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)")
ACL2 !>
\end{verbatim}
}

% The use of attachments (see :DOC DEFATTACH) has been made more efficient,
% avoiding some low-level checks (Common Lisp `boundp' checks).  Thanks to
% Shilpi Goel for constructing an example that we used to help direct us to
% remove inefficiency.  The following results for that example -- a Fibonacci
% program run on a machine interpreter in raw-mode (see :DOC SET-RAW-MODE) --
% give a sense of the potential speedup, though we note that a full ACL2(h)
% regression showed no significant speedup.
% 
% ; Time before the change:
% ; 0.89 seconds realtime, 0.90 seconds runtime
% 
% ; Time after the change:
% ; 0.75 seconds realtime, 0.75 seconds runtime
% 
% ; Time when cheating to avoid the cost of attachments, by redefining a
% ; function to BE its attachment (so, this gives a lower bound on possible
% ; execution time):
% ; 0.72 seconds realtime, 0.72 seconds runtime

%%% discussed above

% Functions read-acl2-oracle and read-acl2-oracle@par are no longer
% untouchable (see :DOC REMOVE-UNTOUCHABLE).  We reported this change for
% Version_5.0 but it was not made; thanks to Jared Davis for bringing this to
% our attention.  Function get-timer also is no longer untouchable.

%%% added \item

% The function butlast now behaves more reasonably on arguments violating
% its guard.  For example, (butlast '(1 2 3) -1) is now provably equal
% to (1 2 3) instead of to (1 2 3 nil).  Thanks to Jared Davis for
% suggesting a change to the definition of butlast.

% The utilities mfc-ts and mfc-ap (see :DOC EXTENDED-METAFUNCTIONS)
% formerly never used forcing (see :DOC FORCE).  Now, by default, forcing is
% allowed during execution of these functions if and only if it is permitted in
% the rewriting environment where they are called.  Moreover, these and the
% mfc-xx utilities -- mfc-rw, mfc-rw+, and mfc-relieve-hyp
% -- are now macros that take (optional) keyword arguments :forcep and
% :ttreep.  The :forcep argument is :same by default, providing the
% forcing behavior inherited from the environment (as described above); but it
% can be the symbol t or nil, indicating that forcing is to be enabled
% or disabled, respectively.  The :ttree argument is nil by default,
% but when it is t, then a second value is returned, which is a tag-tree.
% See :DOC EXTENDED-METAFUNCTIONS.

The extended metafunctions have been reworked, with improved handling
of forcing and also with the option of returning a tag-tree.  Also, a
unifying substitution has been added to metafunction contexts,
accessed with function \texttt{MFC-UNIFY-SUBST}.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/EXTENDED-METAFUNCTIONS.html}{extended-metafunctions}).

% Many improvements have been made to the tau-system (see :DOC TAU-SYSTEM),
% including support for arithmetic intervals bounded by constants.  Thus, for
% example, (and (<= 0 x) (<= x 15)) is a tau predicate.  The
% documentation has also been improved
% (see :DOC INTRODUCTION-TO-THE-TAU-SYSTEM). Also see :DOC TIME-TRACKER-TAU for
% discussion of how the new time-tracker utility can help discover ways
% to detect slowdown related to the tau-system.

%%% See new.tex for tau.

% The defthm events printed by defabsstobj, namely those that
% remain to be proved, are now given with :rule-classes nil since there is
% probably no intention to use them as rules.  Thanks to Robert Krug for
% suggesting that we consider this change.

% The formal parameters for a macro definition (see :DOC DEFMACRO) may now include
% state and user-defined stobjs.  (However, macro formals may not
% be declared as stobjs; see :DOC XARGS.)  Thanks to Jose Luis Ruiz-Reina for
% raising this issue and to Rob Sumners for helpful conversations -- both of
% these nearly 10 years ago!

%%% added \item

% The utilities defun-inline, defun-notinline, defund-inline,
% and defund-notinline have been simplified, by taking advantage of the
% lifting of restrictions on formal parameters of macro definitions mentioned
% above (involving symbols that happen to be stobj names).  Now, when any
% of the above four utilities is called with a given set of formal parameters,
% those formals will be used not only for the generated defun event but
% also for the generated defmacro event.  (Previously, they had been
% renamed for the defmacro event in order to respect the stobj name
% restriction that no longer exists.)  Thanks to Jared Davis for pointing out
% the value of makig this change.

%%% Skipping this -- see defun-inline etc. in new.tex.

% The events add-invisible-fns and remove-invisible-fns now
% convert arguments as appropriate using the macro-aliases-table.  For
% example, the event (add-invisible-fns append car) is now legal (though
% probably not a good idea), because add-invisible-fns is now sensitive
% to the fact that append maps to binary-append in the
% macro-aliases-table.

% When :pe is applied to a built-in function that does not have a
% defining event, such as symbolp, :pe now gives more useful output
% that points to the documentation instead of printing a call of
% ENTER-BOOT-STRAP-MODE.  Thanks to Anthony Knape for bringing this issue
% to our attention.

% The macros memoize and unmemoize now cause a warning rather than
% an error in ACL2 (and work as before in ACL2(h)).

%%% added \item

% Terms are now parsed into :type-prescription rules in a manner that
% removes let bindings both at the top level and in the conclusion (but
% still not in the hypotheses of the rule).  See :DOC TYPE-PRESCRIPTION.  Thanks to
% Jared Davis for requesting such an enhancement.

% Printing of numbers is now appropriately sensitive to the print radix;
% see :DOC SET-PRINT-RADIX.  Thanks to Shilpi Goel for requesting this enhancement.

Printing of numbers now pays attention to the print radix; see
:DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SET-PRINT-RADIX.html}{\texttt{SET-PRINT-RADIX}}.
For example, before Version 6.0 the final value was printed below as
\texttt{ABCD1234}.  Notice the use of \verb|#u| to allow underscores
in numbers, which is new.

{\footnotesize
\begin{verbatim}
ACL2 !>(set-print-base 16 state)
<state>
ACL2 !>(set-print-radix t state)
<state>
ACL2 !>#uxabcd_1234
#xABCD1234
ACL2 !>
\end{verbatim}
}

% The system function explode-atom no longer includes the radix indicator.
% The new function explode-atom+ may be used for that purpose.

%########## 6.1

% The macro defund now avoids an error when :mode :program has been
% specified in an xargs form of a declare form, for example:
% (defund f (x) (declare (xargs :mode :program)) x).  It does this by
% avoiding the generation of in-theory events in such cases.  Thanks
% to David Rager and Jared Davis for requesting such a change, and for ensuing
% helpful discussions.

%%% added \item

% Added a field :UNIFY-SUBST to metafunction contexts
% (see :DOC EXTENDED-METAFUNCTIONS), accessed with function mfc-unify-subst.
% Thanks to Sol Swords for requesting this enhancement.

%%% added \item

% The functions sys-call and sys-call-status are now
% guard-verified :logic-mode functions.

%%% added \item

% It had been the case that if any supporter of a dependent clause processor
% (see :DOC DEFINE-TRUSTED-CLAUSE-PROCESSOR) is among the ancestors of a given
% formula, then it was illegal to apply functional instantiation
% (see :DOC LEMMA-INSTANCE) to that formula.  Now, this is illegal only if some
% such supporter is in the domain of the functional substitution.

eptcsdata.tex
\providecommand{\firstpage}{5}
\providecommand{\publicationstatus}{R. Gamboa and J. Davis (Eds.): ACL2 Workshop 2013 (ACL2 '13).\\
EPTCS 114, 2013, pp.\ \pageref*{FirstPage}--\pageref{LastPage},
doi:\href{http://dx.doi.org/10.4204/EPTCS.114.1}{10.4204/EPTCS.114.1}}
\pdfoutput=1

heuristic.tex
\section{Heuristic improvements}\label{heuristic}

As ACL2 is a heuristic theorem prover, it orchestrates many techniques
to support effective automation of reasoning.  The large regression
suite, contributed by many users over about 20 years, has helped to
tune the prover heuristics so that they often need relatively little
of our attention.  However, we have made improvements since Version
5.0 that include avoidance of some rewriting loops, two
strengthenings of type-set reasoning, and tweaks to the heuristics for
automatically expanding recursive function calls during proofs by
induction.  

%########## 5.0

% Reading of ACL2 arrays (see :DOC AREF1, see :DOC 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 :DOC EQUALITY-VARIANTS.  Guard-holders are also now expanded away before
% storing constraints for encapsulate events, which can
% sometimes result in simpler constraints.

ACL2 now expands away calls of so-called {\em guard-holders} before
storing induction schemes.  These include
\href{http://www.cs.utexas.edu/users/moore/acl2/current/THE.html}{\underline{\texttt{THE}}}
as well as
all calls of
\href{http://www.cs.utexas.edu/users/moore/acl2/current/RETURN-LAST.html}{\underline{\texttt{RETURN-LAST}}}.
The latter include
\href{http://www.cs.utexas.edu/users/moore/acl2/current/MBE.html}{\underline{\texttt{MBE}}},
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PROG2$.html}{\underline{\texttt{PROG2\$}}},%$
and
\href{http://www.cs.utexas.edu/users/moore/acl2/current/EQUALITY-VARIANTS.html}{\underline{equality-variants}} ---
for example, a call of
\texttt{MEMBER} expands to the corresponding call of
\texttt{MEMBER-EQUAL}.  Such expansion also occurs before storing
constraints generated by
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ENCAPSULATE.html}{\underline{\texttt{ENCAPSULATE}}}
\href{http://www.cs.utexas.edu/users/moore/acl2/current/EVENTS.html}{\underline{events}}.

% 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))))))

%########## 6.0

% We obtained a substantial speedup -- 13% observed for the regression suite,
% and 8% observed for the ACL2(h) regression suite -- by tweaking the
% break-rewrite implementation to eliminate virtually all of its overhead
% when it is not in use (the default, which holds until :brr t is
% evaluated).  Thanks to David Rager for a conversation involving ACL2(p)
% performance statistics that suggested looking at changing break-rewrite
% to boost performance.

We may think of the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/BREAK-REWRITE.html}{\underline{break-rewrite}}
utility as a heuristic, since, when enabled, it chooses debugging
information to display to the user.  This utility had incurred
significant overhead even when disabled, as it is by default.  That
has been fixed, resulting in elimination of more than 10\% of the time
required for an ACL2 regression.

% The heuristics for automatically expanding recursive function calls have been
% changed during proofs by induction.  Now, during induction, more terms that
% suggested the induction scheme are automatically expanded.  Thanks to David
% Rager for providing an example and having discussions with us that spurred us
% to develop this heuristic improvement.

%########## 6.1

% [none]

The remainder of this section discusses a feature introduced in
Version 5.0
that contributes to the set of primary prover heuristics: the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/TAU-SYSTEM.html}{\em{tau
      system}}.
This system is a
decision procedure designed to exploit previously
proved theorems about monadic Boolean functions.  The
tau system was extended and improved in Versions 6.0
and 6.1.

The system mines all the axioms, definitions, and
proved rules (of any
\href{http://www.cs.utexas.edu/users/moore/acl2/current/RULE-CLASSES.html}{rule
class}) relating Boolean
function symbols of one argument.  One might think of
these function symbols as recognizing ``soft types''
such as \texttt{integerp}, \texttt{consp},
\texttt{alistp}, \texttt{n32-bit-numberp}, etc.  The
{\em{tau}} of a term is the set of all such recognizers
known to hold of the value of the term.  The tau of a
term is typically computed in a context specifying the
tau of other terms (typically including variables and
subterms).  For example, if an \texttt{IF} has the test
\texttt{(integerp i)}, then when the tau of the true
branch is computed, the variable \texttt{i} is known to
have a tau that contains \texttt{integerp} and all the
recognizers it is known to imply.

For purposes of the tau system, Boolean monadic
functions are tracked, as are equalities and
inequalities with constants.  As of Version 6.1, the
tau system was extended to track intervals.  For
example, the tau for a term might, in addition to
saying that the value of the term is an integer (and
thus also a rational and not a cons), lies in the
interval between 0 and 15 but is not 3 or 7.

Of special importance are {\em{signature rules}} that
allow the tau system to compute the tau of a function
application by computing the tau of the actuals.  Tau
also tracks other forms of rules that relate the known
predicates, and it allows signatures for the various
values returned by multiple-value functions.  The tau
system also provides a way for the user to define,
verify, and install
``\href{http://www.cs.utexas.edu/users/moore/acl2/current/BOUNDERS.html}{bounder}''
functions which can be
used to compute an interval containing a function's
output from the intervals containing its input.

It is possible to prove certain theorems by tau
reasoning alone.  Such formula are often, informally,
thought of as being mere consequences of ``type
checking.''  The tau system is designed to
recognize such formulas rapidly.  It is thought the tau system,
if properly ``programmed'' with rules, will be helpful
in verifying
\href{http://www.cs.utexas.edu/users/moore/acl2/current/GUARD.html}{\underline{guard}}
conjectures.

The tau documentation has grown extensively since
Version 5.0.  We recommend that the interested reader
see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/INTRODUCTION-TO-THE-TAU-SYSTEM.html}{introduction-to-the-tau-system}.

kaufmann-moore.tex
\documentclass[copyright,creativecommons]{eptcs}
\providecommand{\event}{ACL2 2013} % Name of the event you are submitting to
\usepackage{breakurl}             % Not needed if you use pdflatex only.

% Define \doi, as per http://doi.eptcs.org/:
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}

\usepackage{acl2}
\usepackage{xspace}
\usepackage{graphicx}

\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage{lipsum}
\usepackage{ragged2e}
\usepackage{alltt}
% \usepackage{acl2} included above
\usepackage{rotating}
\usepackage{lscape}
\usepackage{setspace}
\usepackage{array}
\usepackage{verbatim}
\usepackage{fancyvrb}
\usepackage{upquote}
\usepackage{color}
% \usepackage[pdftex]{graphicx}
\newcommand\codeHighlightr[1]{\textcolor[rgb]{1,0,0}{\textbf{#1}}}
\newcommand\codeHighlightg[1]{\textcolor[rgb]{0,1,0}{\textbf{#1}}}
\newcommand\codeHighlightb[1]{\textcolor[rgb]{0,0,1}{\textbf{#1}}}
\newcommand{\SmallSkip}{\vspace{0.5cm}\noindent}

% correct bad hyphenation here
% \hyphenation{op-tical net-works semi-conduc-tor}

\newcommand{\aligned}{{\ensuremath{2^{18}}}-aligned\xspace}

\newcommand{\mycomment}[1]{\ \\ {\bf COMMENT}\ \\ {\em #1}\ \\ {\bf END COMMENT\ \\}}
%\newcommand{\mycomment}[1]{}

\newcommand{\assigned}[1]{\ \\ {\bf ASSIGNED TO:}\ {\em #1}\ \\}

\newcommand{\vComment}[1]{{\codeHighlightb{\sf{\small{#1}}}\rm}}

\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired

\title{Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1}

\author{
    Matt Kaufmann\\
    \institute{Dept. of Computer Science,\\
               University of Texas at Austin}
    \email{kaufmann@cs.utexas.edu}
    \and
    J Strother Moore\\
    \institute{Dept. of Computer Science,\\
               University of Texas at Austin}
    \email{moore@cs.utexas.edu}
    }

\def\titlerunning{Enhancements to ACL2}
\def\authorrunning{Matt Kaufmann and J Strother Moore}

\maketitle

\begin{abstract}

We report on highlights of the ACL2 enhancements introduced in ACL2
releases since the 2011 ACL2 Workshop.  Although many enhancements are
critical for soundness or robustness, we focus in this paper on those
improvements that could benefit users who are aware of them, but that
might not be discovered in everyday practice.

\end{abstract}

% From oldtran/bare_jrnl.tex:
% Note that keywords are not normally used for peerreview papers.
% \begin{IEEEkeywords}
% IEEEtran, journal, \LaTeX, paper, template.
% \end{IEEEkeywords}

% Keywords:
% ACL2
% automated reasoning
% mechanized proof
% new features

% \IEEEpeerreviewmaketitle

\section{Introduction}

This paper discusses ACL2 enhancements introduced in releases made
since the ACL2 Workshop in November, 2011: Versions 5.0 (August, 2012), 6.0
(December, 2012), and 6.1 (expected February, 2013).  We thus discuss
enhancements made after the release of ACL2 Version 4.3 in July, 2011.

The release notes~\cite{release-notes-doc} for those three versions
report approximately 200 enhancements, which typically were made in
direct response to user feedback or were important to soundness or
robustness of the system.  Our goal in this paper is not simply to
rehash the release notes; rather, it is to highlight important
improvements that ACL2 users are not likely to discover by the routine
use of ACL2.  We do not discuss lower-level improvements to the system
that are reported in comments in source file \texttt{ld.lisp} for the
release notes (e.g., \texttt{(deflabel note-5-0 ...)}).  Those who
dive into the ACL2 sources may wish to peruse these; for example, they
will notice that starting in ACL2 6.0, \texttt{defrec} defines a
recognizer predicate.

Because of the maturity of ACL2, many of the improvements pertain to
aspects of ACL2 that may be unfamiliar to novice users.  Our hope,
however, is that this paper will have value to those users as well, by
suggesting new ideas about what can be done with ACL2.

As in a preceding paper of a similar nature in the previous ACL2
workshop ~\cite{DBLP:journals/corr/abs-1110-4673}, we write ``see :DOC'' to
highlight documentation topics.  For example, see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/RELEASE-NOTES.html}{release-notes}
and its subtopics (e.g., see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/NOTE-6-0.html}{note-6-0}
for changes introduced in ACL2 Version 6.0).  Documentation topics are
also referenced implicitly using underlining; for example, the topic
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ADVANCED-FEATURES.html}{\underline{advanced-features}}
provides a handy summary of advanced features of ACL2 in one place.
Each documentation topic reference (of either type) is a hyperlink in
the online version of this paper.

Unlike the preceding paper mentioned above, we choose here to organize
the paper in the way that we have organized the release notes for
several years, as follows.
\begin{itemize}

\item Changes to existing features
\item New features
\item Heuristic improvements
\item Bug fixes
\item Changes at the system level

\end{itemize}

\noindent In each of the five sections corresponding to these topics,
we present a few topics in some detail, but in many cases we simply
note an improvement and point to relevant documentation.

There are typically two other categories: Emacs support and
Experimental/alternate versions.  The former has changed little in the
last few release notes.  As for the latter, there have been
significant improvements to
\href{http://www.cs.utexas.edu/users/moore/acl2/current/HONS-AND-MEMOIZATION.html}{ACL2(h)},
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PARALLELISM.html}{ACL2(p)},
and
\href{http://www.cs.utexas.edu/users/moore/acl2/current/REAL.html}{ACL2(r)};
but for these we live within our space limitations, referring readers
to the release notes.

One outlier, not included in the categories above, is a series of
changes related to licensing and distribution.  For Version 5.0,
changes were made to satisfy University of Texas policies: the license
changed from GPL ``Version 2 or later'' to GPL Version 2, and the
community books~\cite{acl2-books-svn} --- basically, what has been
called the regression suite --- were moved away from the University of
Texas, and are hosted by Google Code.  For Version 6.0 we changed the
license to a BSD-style license, in order to make it easier for
industry groups to take advantage of ACL2.

\subsection*{Acknowledgements}

We thank members of the ACL2 community whose feedback has led us to
continue making improvements to ACL2, including the following, each
mentioned for one or more specific items in the release notes for
Version 5.0, 6.0, or 6.1: Harsh Raju Chamarthi, Jared Davis, Ruben
Gamboa, Shilpi Goel, Dave Greve, David Hardin, Marijn Heule, Warren
Hunt, Anthony Knape, Robert Krug, Camm Maguire, Pete Manolios,
Francisco J. Martin Mateos, David Rager, Jose Luis Ruiz-Reina, Anna
Slobodova, Eric Smith, Rob Sumners, Sol Swords, Sarah Weissman, and
Nathan Wetzler.  We expressly thank Warren Hunt for his continued
support of the use of ACL2, in particular in projects at the
University of Texas.  Finally, we thank the reviewers for helpful
comments, one of which led us to improve :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PROVISIONAL-CERTIFICATION.html}{provisional-certification}
for the next release.

This material is based upon work supported by DARPA under Contract
No. N66001-10-2-4087, by ForrestHunt, Inc., and by the National
Science Foundation under Grant Nos. CCF-0945316 and CNS-0910913.

\input{changes}

\input{new}

\input{heuristic}

\input{bug}

\input{system}

\section{Conclusion}

We have presented an outline of changes to ACL2 in Versions 5.0, 6.0,
and 6.1.  Our focus has been to describe changes that can affect one's
daily use of ACL2 but might otherwise go unnoticed.  Many more changes
(close to 200 altogether) may be found in the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/RELEASE-NOTES.html}{release
  notes} for these three versions, and many changes at a lower level
are described in comments in the source code for those release notes
(\texttt{(deflabel note-5-0 ...)} etc.).

A critical component in the continued evolution of ACL2 is feedback
from the user community.  We hope that you'll keep that feedback
coming!  Another contribution of the user community is the large body
of Community Books~\cite{acl2-books-svn}, which put demands on the
system and help us to test improvements.  Please keep these coming,
too!

\bibliographystyle{eptcs}

\bibliography{kaufmann-moore}

\end{document}

new.tex
\section{New features}

Of the approximately 50 release note items about new features, we list a few
here and then elaborate on a few others below.

\begin{itemize}

\item See :DOC
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/PRINT-SUMMARY-USER.html}{\texttt{PRINT-SUMMARY-USER}}
  for a way to add to what is printed in event summaries.

\item Commands
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PL.html}{\underline{PL}}}
and
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PR.html}{\underline{PR}}}
now have analogues in
the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PROOF-CHECKER.html}{\underline{proof-checker}}.

\item See :DOC
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/PROVISIONAL-CERTIFICATION.html}{provisional-certification}
  for how to certify books in parallel even when they they are ordered
  linearly by
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/INCLUDE-BOOK.html}{\underline{\texttt{INCLUDE-BOOK}}}.

\item ACL2 now supports multiple instances of a stobj (whether
conventional or abstract), known as {\em congruent stobjs}.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFSTOBJ.html}{\texttt{DEFSTOBJ}}
and see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFABSSTOBJ.html}{\texttt{DEFABSSTOBJ}}.

\item Access to the host Lisp's disassembler is now provided in the
  ACL2 loop by the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DISASSEMBLE$.html}{\underline{\texttt{DISASSEMBLE\$}}}
%$
utility.

\item See :DOC
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFTHEORY-STATIC.html}{\texttt{DEFTHEORY-STATIC}}
  for a variant of
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFTHEORY.html}{\underline{\texttt{DEFTHEORY}}}
  that behaves the same when a book containing such an event is
  included, as it does when when the book was certified.

\item See :DOC
  \texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PSOF.html}{PSOF}}
  for a variant of
  \texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PSO.html}{\underline{PSO}}}
  that directs proof output hidden by
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/GAG-MODE.html}{gag-mode}
  to a file.  Also see :DOC
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/WOF.html}{\texttt{WOF}}
  for a general utility for directing output to a file.

\item A new macro,
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFND.html}{\underline{\texttt{DEFND}}}
is just
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFN.html}{\underline{\texttt{DEFN}}}
(i.e.,
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN.html}{\underline{\texttt{DEFUN}}}
with a
\href{http://www.cs.utexas.edu/users/moore/acl2/current/GUARD.html}{\underline{guard}}
of \texttt{T}) plus a
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/DISABLE.html}{\underline{\texttt{disable}}}
  just as
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUND.html}{\underline{\texttt{DEFUND}}}
is
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN.html}{\underline{\texttt{DEFUN}}}
plus a \texttt{DISABLE}.

\item New utilities
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/ORACLE-FUNCALL.html}{\underline{\texttt{ORACLE-FUNCALL}}},
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/ORACLE-APPLY.html}{\underline{\texttt{ORACLE-APPLY}}},
  and
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/ORACLE-APPLY-RAW.html}{\underline{\texttt{ORACLE-APPLY-RAW}}},
  provide a sort of higher-order capability, by calling a function
  argument on specified arguments.

\item Both \texttt{INLINE} and \texttt{NOTINLINE} declarations are now
supported for the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/FLET.html}{\underline{\texttt{FLET}}}
utility.

\item See :DOC
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/GC-VERBOSE.html}{\texttt{GC-VERBOSE}}
  for how to control, in some host Lisps, the printing of
  garbage-collection messages.

\item The utility
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ADD-MACRO-FN.html}{\underline{\texttt{ADD-MACRO-FN}}},
which is a replacement for \texttt{ADD-BINOP}, lets you choose whether
macros are to be displayed as flat right-associated calls, for
example, \texttt{(append x y z)} rather than \texttt{(append x (append
  y z))}.

\item The new
  \href{http://www.cs.utexas.edu/users/moore/acl2/current/TIME-TRACKER.html}{\underline{\texttt{TIME-TRACKER}}}
  utility supports annotating your programs to display information
  during a computation about elapsed runtime.

\item The {\em{tau system}} is discussed in Section~\ref{heuristic}.

%% Removing nested stobjs because they aren't likely to make it into 6.1.
%% \item Stobjs may now have fields that are also stobjs (expected in
%%   Version 6.1).
%% I might say more about stobj fields of stobjs later, with an
%% example illustrating stobj-let.

\end{itemize}

\noindent {\em Some other new features} \\

%########## 5.0

% A new ``tau system'' provides a kind of ``type checker.''  See :DOC 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.

%%% added \item pointing to heuristic.tex

% Users may now arrange for additional summary information to be printed at the
% end of events; see :DOC PRINT-SUMMARY-USER.  Thanks to Harsh Raju Chamarthi
% for requesting this feature and participating in a design discussion.

%%% added \item

% 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 :DOC SHARP-U-READER.  Thanks to Jared Davis for requesting this
% capability.

%%% I snuck mention of #u into changes.tex.

% 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 :DOC PROOF-CHECKER-COMMANDS.  Thanks to Pete Manolios for suggesting such
% clarification and capability.

%%% added \item

% 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)))
% 
% Thanks to Jared Davis for requesting this enhancement, in particular for
% calling non-executable functions in the :logic part of an mbe
% call.  Here is Jared's example, which is admissible now but formerly was
% not.
% 
% (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))))

The utility
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN-NX.html}{\underline{\texttt{DEFUN-NX}}}
has been improved, for example by avoiding
\href{http://www.cs.utexas.edu/users/moore/acl2/current/STOBJ.html}{\underline{stobj}}
restrictions in the \texttt{:LOGIC} component of an
\href{http://www.cs.utexas.edu/users/moore/acl2/current/MBE.html}{\underline{MBE}}
call.  Here is an example from Jared Davis that motivated this change;
note the call of function \texttt{MY-IDENTITY} on a stobj even though
\texttt{MY-IDENTITY} was not declared to take a stobj argument.
{\footnotesize
\begin{verbatim}
(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))))
\end{verbatim}
}
\noindent But there now is another way to violate signatures in non-executable
code: by using the utility,
\href{http://www.cs.utexas.edu/users/moore/acl2/current/NON-EXEC.html}{\underline{NON-EXEC}}.
Note that this time, \texttt{MY-IDENTITY} is defined with
\texttt{DEFN} (which is \texttt{DEFUN} with a guard of \texttt{T}),
not by \texttt{DEFUN-NX}.
{\footnotesize
\begin{verbatim}
(defstobj foo (fld))
(defn my-identity (x) x)
(defun my-fld (foo)
  (declare (xargs :stobjs foo))
  (non-exec (my-identity foo)))
\end{verbatim}
}

% 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.

%%% See preceding item.

% 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 :DOC 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.

%%% added \item

% Event summaries now show the names of events that were mentioned in
% hints of type :use, :by, or :clause-processor.
% See :DOC 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 :DOC 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.

%%% Still not really enough book support to make this worth mentioning.

% A new documentation topic provides a guide to programming with state;
% see :DOC 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 :DOC 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 :DOC ACL2-BUILT-INS -- which is a
% subtopic of programming, a topic that in turn has considerably fewer
% direct subtopiics than before.

There have been many improvements to the
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DOCUMENTATION.html}{\underline{documentation}},
but here we focus on two new topics.  The topic
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ADVANCED-FEATURES.html}{\underline{advanced-features}}
summarizes some cool features of ACL2 that might not all be widely
known, yet may be of interest, especially to experienced users.
Another new topic provides a guide to programming with the ACL2
\href{http://www.cs.utexas.edu/users/moore/acl2/current/STATE.html}{\underline{state}};
see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/PROGRAMMING-WITH-STATE.html}{programming-with-state}.

% 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 :DOC 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 :DOC IO.

% A stobj may now be passed as an argument where another stobj is expected
% if the two are ``congruent''.  See :DOC 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.

%%% added \item

% A new top-level utility has been provided that shows the assembly language
% for a defined function symbol; see :DOC 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/).

%%% added \item

% 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 :DOC ADVANCED-FEATURES.  Thanks to Warren
% Hunt and Anna Slobodova for requesting such information.

%%% covered above

% 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.

%%% added \item

% A new event, defabsstobj, provides a new way to introduce
% single-threaded objects (see :DOC STOBJ and see :DOC 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 :DOC DEFABSSTOBJ.  Also thanks to Sol Swords for sending an example exhibiting
% a bug in the initial implementation, which has been fixed.

A new event,
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFABSSTOBJ.html}{\underline{\texttt{DEFABSSTOBJ}}},
provides an interface to conventional single-threaded objects known as
{\em abstract stobjs}~\cite{defabsstobj-paper}.  These can provide
advantages over conventional stobjs in several arenas: execution
speed, proof efficiency, use of symbolic simulation, and modularity of
proof development.

% 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 :DOC PSOF.  More generally,
% a new utility, wof (an acronym for ``With Output File''), directs
% standard output and proofs output to a file; see :DOC WOF.

%%% added \item

% 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.

%%% added \item

% 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.

%%% Mentioned :pl2 and :linear in changes.tex.

% 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 :DOC ADD-MACRO-FN.

%%% added \item

% 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 :DOC DEFUN-INLINE and see :DOC 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.

ACL2 now provides a way to direct the host Lisp compiler to inline
calls of a given function.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN-INLINE.html}{\texttt{DEFUN-INLINE}}.
We expect that you can generally use this utility just as you would
use
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN.html}{\underline{\texttt{DEFUN}}}
to define a function.  However, we say a bit more, in part to motivate
our design of this utility.  Fundamentally, \texttt{DEFUN-INLINE} is
simply a macro, as we illustrate by expanding a call of this macro.
{\footnotesize
\begin{verbatim}
ACL2 !>:trans1 (defun-inline f (x)
                 (declare (xargs :guard (consp x)))
                 (integerp (car x)))
 (PROGN (DEFMACRO F (X) (LIST 'F$INLINE X))
        (ADD-MACRO-FN F F$INLINE)
        (DEFUN F$INLINE (X)
               (DECLARE (XARGS :GUARD (CONSP X)))
               (INTEGERP (CAR X))))
ACL2 !>
\end{verbatim}
}
\noindent Notice that \texttt{F} is defined to be a macro whose calls expands to a
corresponding calls of a function, \texttt{F\$INLINE}.  The
invocation of
\href{http://www.cs.utexas.edu/users/moore/acl2/current/ADD-MACRO-FN.html}{\underline{\texttt{ADD-MACRO-FN}}}
arranges that theory functions understand \texttt{F} to mean
\texttt{F\$INLINE} and that proof output will display calls of
\texttt{F\$INLINE} as corresponding calls of \texttt{F}.  But why
didn't we simply support the Common Lisp form \texttt{(declaim (inline
  f))}?  The reason is the support that ACL2 provides for undoing.
Imagine that you want \texttt{F} to be inline and then you change your
mind --- or maybe \texttt{F} is defined in a book that you include
locally.  How can we arrange for Common Lisp to undo the directive to
inline calls of \texttt{F}?  Sadly, the Common Lisp
language~\cite{Steele:1990:CLL:95411} does not provide for a way to do that.  The best
we can do is to direct \texttt{F} to be \texttt{notinline} --- but
that could defeat the host Lisp's appropriate inlining of some
subsequent definition of \texttt{F}.  Our solution is {\em always} to
direct inlining for functions whose name ends in the string
\texttt{"\$INLINE"}, and to provide the illusion that we are defining
a function \texttt{F} rather than \texttt{F\$INLINE}, using
\texttt{ADD-MACRO-FN} as discussed above.  Note that analogous
considerations hold for utility
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DEFUN-INLINE.html}{\underline{\texttt{DEFUN-NOTINLINE}}}.

%########## 6.0

% Among the new features for system hackers are analogues of system function
% simple-translate-and-eval that do not return state.  (Thanks to
% David Rager for requesting this feature and helpful conversations on its
% implementation.)  This and other low-level changes are typically documented
% in comments in the corresponding release note event, which in this case is
% (deflabel note-6-0 ...).

%%% Too low-level except maybe for system hackers.

% More built-in functions are now guard-verified (and in :logic
% mode).  Furthermore, a mechanism exists for marking yet more built-in
% functions as guard-verified based on books contributed by users; see
% Part II of
% http://www.cs.utexas.edu/users/moore/acl2/open-architecture/.  The
% current state of that enterprise may be viewed by evaluating the constant
% *system-verify-guards-alist*, which associates a community book name with
% a list of functions.  When ACL2 is built in the normal way, each of those
% functions is marked as guard-verified when ACL2 is started up; but a special
% developer build can be used to check that the indicated book, together with
% its sub-books, proves that those functions are guard-verified.

We invite the ACL2 community to help us to convert ACL2 system
functions from
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/PROGRAM.html}{\underline{PROGRAM}}}
mode to
\href{http://www.cs.utexas.edu/users/moore/acl2/current/GUARD.html}{\underline{guard}}-verified
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/LOGIC.html}{\underline{LOGIC}}}
mode.  This mechanism is described in some detail
in an online document~\cite{how-to-make-patches}.
Here, in brief, are the steps to follow; we would be happy to provide
more details leading to improvement of the online document.

\begin{enumerate}

\item Install a local copy of ACL2, and build it using \texttt{make}.

\item Develop a book that includes
\href{http://www.cs.utexas.edu/users/moore/acl2/current/VERIFY-TERMINATION.html}{\underline{\texttt{VERIFY-TERMINATION}}}
and
\href{http://www.cs.utexas.edu/users/moore/acl2/current/VERIFY-GUARDS.html}{\underline{\texttt{VERIFY-GUARDS}}}
forms for one or more system functions.  For simplicity we assume here
that there is a single such function, \texttt{FN}.

\item When necessary, modify ACL2 definitions in your copy, for
  example by replacing some calls of \texttt{NULL} by corresponding
  calls of \texttt{ENDP} or by adding or modifying guard
  declarations.  Rebuild your local copy of ACL2 using \texttt{make}.

\item Email us your ACL2 changes and your book, and we will do what is
  necessary in order to incorporate your book into the ACL2 community
  books~\cite{acl2-books-svn} and your changes into the ACL2 sources.

\item Henceforth, the default build of ACL2 will accordingly mark
  \texttt{FN} as a guard-verified \texttt{:LOGIC} mode function.

\end{enumerate}
\noindent We, the ACL2 developers, will check each release that such
proofs still go through, using a build that leaves \texttt{FN} in
\texttt{:PROGRAM} mode.

% Metatheorems (see :DOC META) may now have additional hypotheses, called
% ``meta-extract hypotheses'', that allow metafunctions to depend on the
% validity of certain terms extracted from the context or the logical
% world.  See :DOC META-EXTRACT.  Thanks to Sol Swords for providing an initial
% implementation, together with very helpful discussions as well as a community
% book, books/clause-processors/meta-extract-user.lisp, that extends the
% power of meta-extract hypotheses.

If you have written
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/META.html}{\underline{META}}}
rules or
\texttt{:\href{http://www.cs.utexas.edu/users/moore/acl2/current/CLAUSE-PROCESSOR.html}{\underline{CLAUSE-PROCESSOR}}}
rules, you may have been frustrated that your meta functions and
clause processor functions could not assume the correctness of prover
computations, for example as performed using \texttt{MFC-TS} (see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/EXTENDED-METAFUNCTIONS.html}{extended-metafunctions}).
A new mechanism, designed with Sol Swords, now provides such a
capability; see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/META-EXTRACT.html}{meta-extract}).
The community book
%% I'm not going to underline the book name -- doesn't seem to be a
%% point to underlining other than :doc topics.
\href{https://acl2-books.googlecode.com/svn/trunk/clause-processors/meta-extract-simple-test.lisp}{\texttt{clause-processors/meta-extract-simple-test.lisp}} provides illustrative examples.

% New utilities oracle-funcall, oracle-apply, and
% oracle-apply-raw call a function argument on specified arguments.
% Thanks to Jared Davis for requesting this utility.

%%% added \item

% A new utility makes it convenient to track time spent inside specified
% function calls or, more generally, during specified evaluation.
% See :DOC TIME-TRACKER.

%%% added \item

% New runic designators make it easy to refer to macro names when building
% theories.  Thus, for example, the object (:i append) may be used in
% theory expressions to designate the rune (:induction binary-append).
% See :DOC THEORIES.  Thanks to Jared Davis for a useful discussion leading to this
% enhancement.

ACL2 rule names, or
\href{http://www.cs.utexas.edu/users/moore/acl2/current/RUNE.html}{\underline{rune}s},
form the basis of ACL2
\href{http://www.cs.utexas.edu/users/moore/acl2/current/THEORIES.html}{\underline{theories}}.
But runes do not take into account
\href{http://www.cs.utexas.edu/users/moore/acl2/current/MACRO-ALIASES-TABLE.html}{\underline{macro
    aliases}}
for function symbols.  For example, \texttt{(:definition
  binary-append)} is a rune, and you can use \texttt{append} in a
theory expression to abbreviate the set of runes,
\texttt{\{(:definition binary-append), (:induction binary-append)\}};
but you cannot use \texttt{(:definition append)} in a theory
expression.  Now, however, you can use \texttt{(:d append)} in a
theory expression to designate the rune \texttt{(:definition
  binary-append)}.  There are four new such abbreviation mechanisms,
as follows, where \texttt{symb} is a symbol and \texttt{symb'} is the
macro-aliases dereference of \texttt{symb}; e.g.,
\texttt{binary-append} is the macro-aliases dereference of
\texttt{append}, while \texttt{car} is the macro-aliases dereference
of itself.
\begin{itemize}

\item \texttt{(:d symb . r)} designates the rune
  \texttt{(:definition symb' . r)}.

\item \texttt{(:e symb . r)} designates the rune
  \texttt{(:executable-counterpart symb' . r)}.

\item \texttt{(:i symb . r)} designates the rune
  \texttt{(:induction symb' . r)}.

\item \texttt{(:t symb . r)} designates the rune
  \texttt{(:type-prescription symb' . r)}.

\end{itemize}

% Defabsstobj events now take an optional :congruent-to keyword
% argument, much like defstobj.  Thanks to Sol Swords for requesting this
% feature and for suggesting a very nice optimization that avoids the need to
% prove additional lemmas.

%%% included in previously-added \item

% Flet may now include inline and notinline declarations.  Thanks
% to Jared Davis for requesting this feature.

%%% added \item

% The utility gc-verbose controls printing of messages by the garbage
% collector, for certain host Lisps.  See :DOC GC-VERBOSE.  Thanks to Shilpi Goel
% for requesting this utility.

%%% added \item

% Added definitions of functions nat-listp and acl2-number-listp.
% Thanks to Harsh Raju Chamarthi for requesting these additions.  Many
% community books had varying definitions of these functions; these additions
% guarantee that all books must agree on how these two functions are
% defined.  (Some community books have been changed in order that they remain
% certifiable, given these additions.)  Note that a few built-in
% :forward-chaining rules were modified in order to accommodate these
% additions, and the definition of integer-listp was modified to call
% eq instead of equal, like the other such definitions.

% See :DOC GET-COMMAND-SEQUENCE for a new utility that returns a list of
% commands between two given command descriptors.

%########## 6.1

% A new utility, set-splitter-output, can direct the prover to give
% information about case splits.  See :DOC SET-SPLITTER-OUTPUT.  Thanks to many
% ACL2 users, most recently David Rager, for requesting such a capability.
% Also thanks to David Rager and Jared Davis for helpful discussions.

Take a new look at ACL2 output when you have large case splits, which
in the past could be difficult to debug.  Now, "Splitter Notes" can
help you locate sources of your case splits.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/SPLITTER.html}{splitter}.

system.tex
\section{Changes at the system level}

In this section we pick a few additions and improvements that are
outside the realm of what one might normally think of as ``ACL2
features''.

%########## 5.0

% 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 :DOC 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.

The character encoding for reading from files --- and for some host
Lisps also for reading from the terminal --- is now iso-8859-1, also
known as latin-1.  See :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/CHARACTER-ENCODING.html}{character-encoding}.

% 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.

You can now build the ACL2
\href{http://www.cs.utexas.edu/users/moore/acl2/current/DOCUMENTATION.html}{\underline{documentation}}
locally (using \texttt{make DOC}).  Previously, the graphics had been
omitted when doing so.

% 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 :DOC BOOK-MAKEFILES.)

% (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.

%########## 6.0

% The state global variable 'distributed-books-dir has been renamed
% 'system-books-dir.  On a related note, the documentation now refers
% to ``community books'' rather than ``distributed books'', and there is a
% corresponding new documentation topic; see :DOC COMMUNITY-BOOKS.

% Fixed a bug in the implementation of wet (which is actually in the
% community book books/misc/wet.lisp).

%%% See changes.tex.

% A directory, interface/, is no longer part of the ACL2 distribution.
% Rather, it is a subdirectory of the ACL2 community books.  Thus, if you fetch
% those books in the usual way (see the installation instructions on the ACL2
% home page), you will find a directory books/interface/.  Subdirectory
% emacs/ of that interface directory provides Emacs support for
% proof-trees as well an acl2-mode.  This change has been reflected in
% ACL2 file emacs/emacs-acl2.el, so users will probably not be impacted if
% they load that file into Emacs.

% The community books file books/Makefile-generic now causes, by default, a
% backtrace to be printed when there is a raw Lisp error.

% Some changes have been made to how regressions are run, i.e., to how the
% community books are certified.  (1) The standard regression now includes
% community books directory books/centaur.  To skip these (for example, a
% Windows system has encountered difficulty with them even after installing
% Perl), include ACL2_CENTAUR=skip with your `make' command.  (2) A new
% `make' (or environment) variable, ACL2_JOBS, specifies the number of
% parallel jobs to run, serving as a replacment for the -j argument of
% `make' that works for all community books, including those under directory
% centaur; see :DOC BOOK-MAKEFILES.  (3) It is no longer necessary to do an
% ACL2(h) regression in order to build a copy of the documentation generated by
% Jared Davis's xdoc utility at books/xdoc-impl/manual/preview.html; a
% vanilla ACL2 regression will build this manual.  (4) It is no longer
% necessary to set the ACL2 environment variable for ACL2(h) regressions if
% you want to use the executable saved_acl2h in the ACL2 sources directory.

If you want to run a parallel regression using `make', you should now
avoid the `\texttt{-j}' option.  Instead, use \texttt{ACL2\_JOBS=$n$}
where $n$ is the maximum number of jobs to run in parallel.  This
change is in support of including the \texttt{centaur/} books in such
regressions.  (Those books had formerly only been certified in
regressions done for ACL2(h); see :DOC
\href{http://www.cs.utexas.edu/users/moore/acl2/current/HONS-AND-MEMOIZATION.html}{hons-and-memoization}.)
Note that you should still use `\texttt{-j}' if you are certifying
books residing in a particular directory, rather than doing a full
regression.

% The ACL2 home page now has a search utility for documentation and books.
% Thanks to Shilpi Goel and David Rager for feedback on a preliminary version
% of this utility.

The search button near the top of the
\href{http://www.cs.utexas.edu/users/moore/acl2/}{ACL2 home page} will
lead you to two search utilities: one for the documentation, and one
for the community books.

% (only for SBCL with 64-bit ACL2(h)) The value of SBCL command line option
% --dynamic-space-size for ACL2(h) on 64-bit platforms has been increased
% from 2000 to 16000 (as explained in a comment in the ACL2 source definition
% of *sbcl-dynamic-space-size*).

%########## 6.1

% The books/ directory no longer needs to exist in order to build an ACL2
% executable.  Thanks to Robert Krug for pointing out that the installation
% instructions had suggested that this was already the case.

kaufmann-moore.bbl
\begin{thebibliography}{1}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{misc}{acl2-books-svn}
\bibitem{acl2-books-svn}
\bibinfo{author}{The~{ACL2} \surnamestart community\surnameend}:
  \emph{\bibinfo{title}{{{ACL2} Community Books}}}.
\newblock \bibinfo{note}{See URL \url{https://code.google.com/p/acl2-books/}}.

\bibitemdeclare{inproceedings}{defabsstobj-paper}
\bibitem{defabsstobj-paper}
\bibinfo{author}{Shilpi \surnamestart Goel\surnameend}, \bibinfo{author}{Warren
  \surnamestart A.~Hunt\surnameend, Jr.} \& \bibinfo{author}{Matt \surnamestart
  Kaufmann\surnameend} (\bibinfo{year}{2013}): \emph{\bibinfo{title}{Abstract
  Stobjs and Their Application to ISA Modeling}}.
\newblock In: {\sl \bibinfo{booktitle}{Proceedings 11th International Workshop
  on the ACL2 Theorem Prover and its Applications}}.

\bibitemdeclare{misc}{release-notes-doc}
\bibitem{release-notes-doc}
\bibinfo{author}{Matt \surnamestart Kaufmann\surnameend} \&
  \bibinfo{author}{J~Strother \surnamestart Moore\surnameend}:
  \emph{\bibinfo{title}{{ACL2} documentation topic: {RELEASE-NOTES}}}.
\newblock \bibinfo{note}{See URL
  \url{http://www.cs.utexas.edu/users/moore/acl2/current/RELEASE-NOTES.html}}.

\bibitemdeclare{misc}{how-to-make-patches}
\bibitem{how-to-make-patches}
\bibinfo{author}{Matt \surnamestart Kaufmann\surnameend} \&
  \bibinfo{author}{J~Strother \surnamestart Moore\surnameend}:
  \emph{\bibinfo{title}{Instructions for modifying {ACL2} system code}}.
\newblock \bibinfo{note}{See URL
  \url{http://www.cs.utexas.edu/users/moore/acl2/open-architecture/how-to-make%
-patches.txt}}.

\bibitemdeclare{inproceedings}{DBLP:journals/corr/abs-1110-4673}
\bibitem{DBLP:journals/corr/abs-1110-4673}
\bibinfo{author}{Matt \surnamestart Kaufmann\surnameend} \&
  \bibinfo{author}{J~Strother \surnamestart Moore\surnameend}
  (\bibinfo{year}{2011}): \emph{\bibinfo{title}{How Can I Do That with ACL2?
  Recent Enhancements to ACL2}}.
\newblock In \bibinfo{editor}{David \surnamestart Hardin\surnameend} \&
  \bibinfo{editor}{Julien \surnamestart Schmaltz\surnameend}, editors: {\sl
  \bibinfo{booktitle}{ACL2}}, {\sl
  \bibinfo{series}{EPTCS}}~\bibinfo{volume}{70}, pp. \bibinfo{pages}{46--60}.
\newblock \urlprefix\url{http://dx.doi.org/10.4204/EPTCS.70.4}.

\bibitemdeclare{book}{Steele:1990:CLL:95411}
\bibitem{Steele:1990:CLL:95411}
\bibinfo{author}{Guy~L. \surnamestart Steele\surnameend, Jr.}
  (\bibinfo{year}{1990}): \emph{\bibinfo{title}{Common LISP: the language (2nd
  ed.)}}.
\newblock \bibinfo{publisher}{Digital Press}, \bibinfo{address}{Newton, MA,
  USA}.

\end{thebibliography}
