NOTE4

Major Section:  RELEASE-NOTES

Once again ld only takes one required argument, as the bind-flg has been deleted.

Three commands have been added in the spirit of :pe. :Pe! is similar to :pe but it prints all events with the given name, rather than just the most recent. The command :pf prints the corollary formula corresponding to a name or rune. The command :pl (print lemmas) prints rules whose top function symbol is the given name. See pe!, see pf, and see pl.

Book naming conventions have been changed somewhat. The once-required .lisp extension is now prohibited! Directories are supported, including a notion of ``connected book directory''. See book-name. Also, the second argument of certify-book is now optional, defaulting to 0.

Compilation is now supported inside the Acl2 loop. See comp and see set-compile-fns.

The default color is now part of the Acl2 world; see :doc default-color. Ld-color is no longer an ld special. Instead, colors are events; see the documentation for red, pink, blue, and gold.

A table exists for controlling whether Acl2 prints comments when it forces hypotheses of rules; see :doc force-table. Also, it is now possible to turn off the forcing of assumptions by disabling the definition of force; see force.

The event defconstant is no longer supported, but a very similar event, defconst, has been provided in its place. See defconst.

The event for defining congruence relations is now defcong (formerly, defcon).

Patterns are now allowed in :expand hints. See the documentation for :expand inside the documentation for hints.

We have improved the way we report rules used by the simplifier. All runes of the same type are reported together in the running commentary associated with each goal, so that for example, executable counterparts are listed separately from definitions, and rewrite rules are listed separately from linear rules. The preprocessor now mentions ``simple'' rules; see simple.

The mechanism for printing warning messages for new rewrite rules, related to subsumption, now avoids worrying about nonrecursive function symbols when those symbols are disabled. These messages have also been eliminated for the case where the old rule is a :definition rule.

Backquote has been modified so that it can usually provide predictable results when used on the left side of a rewrite rule.

Time statistics are now printed even when an event fails.

The Acl2 trace package has been modified so that it prints using the values of the Lisp globals *print-level* and *print-length* (respectively).

Table has been modified so that the :clear option lets you replace the entire table with one that satisfies the val and key guards (if any); see table.

We have relaxed the translation rules for :measure hints to defun, so that the the same rules apply to these terms that apply to terms in defthm events. In particular, in :measure hints mv is treated just like list, and state receives no special handling.

The loop-stopper test has been relaxed. The old test required that every new argument be strictly less than the corresponding old argument in a certain term-order. The new test uses a lexicographic order on term lists instead. For example, consider the following rewrite rule.

  (equal
   (variable-update var1
                    val1 (variable-update var2 val2 vs))
   (variable-update var2
                    val2 (variable-update var1 val1 vs)))

  (variable-update u y (variable-update u x vs)).

Messages about events now contain a space after certain left parentheses, in order to assist emacs users. For example, the event

  (defthm abc (equal (+ (len x) 0) (len x)))

  Form:  ( DEFTHM ABC ...)

More tautology checking is done during a proof; in fact, no goal printed to the screen, except for the results of applying :use and :by hints or the top-level goals from an induction proof, are known to Acl2 to be tautologies.

The ld-query-control-alist may now be used to suppress printing of queries; see ld-query-control-alist.

Warning messages are printed with short summary strings, for example the string ``Use'' in the following message.

  Acl2 Warning [Use] in DEFTHM:  It is unusual to :USE an enabled
  :REWRITE or :DEFINITION rule, so you may want to consider
  disabling FOO.

The keyword command :u has been introduced as an abbreviation for :ubt :max. Printing of query messages is suppressed by :u.

The keyword :cheat is no longer supported by any event form.

Some irrelevant formals are detected; see irrelevant-formals.

A bug in the application of metafunctions was fixed: now if the output of a metafunction is equal to its input, the application of the metafunction is deemed unsuccessful and the next metafunction is tried.

An example has been added to the documentation for equivalence to suggest how to make use of equivalence relations in rewriting.

The following Common Lisp functions have been added to Acl2: alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase, string-downcase, string-upcase, and digit-charp-p.

A documentation section called proof-checker has been added for the interactive facility, whose documentation has been slightly improved. See in particular the documentation for proof-checker, verify, and macro-command.

A number of events that had been inadvertently disallowed in books are now permitted in books. These are: defcong, defcor, defequiv, defrefinement, defstub, and verify-termination.

NOTE5

Major Section:  RELEASE-NOTES

Acl2 now allows ``complex rationals,'' which are complex numbers whose real parts are rationals and whose imaginary parts are non-zero rationals. See complex.

A new way of handling forced hypotheses has been implemented. Rather than cause a case split at the time the force occurs, we complete the main proof and then embark on one or more ``forcing rounds'' in which we try to prove the forced hypotheses. See forcing-round. To allow us to compare the new handling of force with the old, Version 1.5 implements both and uses a flag in state to determine which method should be used. Do (assign old-style-forcing t) if you want force to be handled as it was in Version 1.4. However, we expect to eliminate the old-style forcing eventually because we think the new style is more effective. To see the difference between the two approaches to forcing, try proving the associativity of append under both settings of old-style-forcing. To get the new behavior invoke:

(thm (implies (and (true-listp a) (true-listp b))
              (equal (append (append a b) c)
                     (append a (append b c)))))

A new :cases hints allows proof by cases. See hints.

Include-book and encapsulate now restore the acl2-defaults-table when they complete. See include-book and see encapsulate.

The guards on many Acl2 primitives defined in axioms.lisp have been weakened to permit them to be used in accordance with lisp custom and tradition.

It is possible to attach heuristic filters to :rewrite rules to limit their applicability. See syntaxp.

A tutorial has been added; see acl2-tutorial.

Events now print the Summary paragraph listing runes used, time, etc., whether they succeed or fail. The format of the ``failure banner'' has been changed but still has multiple asterisks in it. Thm also prints a Summary, whether it succeeds or fails; but thm is not an event.

A new event form skip-proofs has been added; see skip-proofs.

A user-specific customization facility has been added in the form of a book that is automatically included, if it exists on the current directory. See acl2-customization.

A facility for conditional metalemmas has been implemented; see meta.

The acceptable values for ld-skip-proofsp have changed. In the old version (Version 1.4), a value of t meant that proofs and local events are to be skipped. In Version 1.5, a value of t means proofs (but not local events) are to be skipped. A value of 'include-book means proofs and local events are to be skipped. There are two other, more obscure, acceptable values. See ld-skip-proofsp.

In order to turn off the forcing of assumptions, one should now disable the :executable-counterpart of force (rather than the :definition of force, as in the previous release); see force.

The macros enable-forcing and disable-forcing make it convenient to enable or disable forcing. See enable-forcing and see disable-forcing.

The new commands :pr and :pr! print the rules created by an event or command. See pr and see pr!.

The new history commands :puff and :puff* will replace a compound command such as an encapsulate or include-book by the sequence of events in it. That is, they ``puff up'' or ``lift'' the subevents of a command to the command level, eliminating the formerly superior command and lengthening the history. This is useful if you want to ``partially undo'' an encapsulate or book or other compound command so you can experiment. See puff and see puff*.

Theory expressions now are allowed to use the free variable world and prohibited from using the free variable state. See theories, although it is essentially the same as before except it mentions world instead of state. See world for a discussion of the Acl2 logical world. Allowing in-theory events to be state-sensitive violated an important invariant about how books behaved.

Table keys and values now are allowed to use the free variable world and prohibited from using the free variable state. See the note above about theory expressions for some explanation.

The macro for minus, -, used to expand (- x 3) to (+ x -3) and now expands it to (+ -3 x) instead. The old macro, if used in the left-hand sides of rewrite rules, produced inapplicable rules because the constant occurs in the second argument of the +, but potential target terms generally had the constant in the first argument position because of the effect of commutativity-of-+.

A new class of rule, :linear-alias rules, allows one to implement the nqthm package and similar hacks in which a disabled function is to be known equivalent to an arithmetic function. See linear-alias.

A new class of rule, :built-in-clause rules, allows one to extend the set of clauses proved silently by defun during measure and guard processing. See built-in-clauses.

The new command pcb! is like pcb but sketches the command and then prints its subsidiary events in full. See pcb!.

:Rewrite class rules may now specify the :loop-stopper field. See rule-classes and see loop-stopper.

The rules for how loop-stoppers control permutative rewrite rules have been changed. One effect of this change is that now when the built-in commutativity rules for + are used, the terms a and (- a) are permuted into adjacency. For example, (+ a b (- a)) is now normalized by the commutativity rules to (+ a (- a) b); in Version 1.4, b was considered syntactically smaller than (- a) and so (+ a b (- a)) is considered to be in normal form. Now it is possible to arrange for unary functions be be considered ``invisible'' when they are used in certain contexts. By default, unary-- is considered invisible when its application appears in the argument list of binary-+. See loop-stopper and see set-invisible-fns-alist.

Extensive documentation has been provided on the topic of Acl2's ``term ordering.'' See term-order.

Calls of ld now default ld-error-action to :return rather than to the current setting.

The command descriptor :x has been introduced and is synonymous with :max, the most recently executed command. History commands such as :pbt print a :x beside the most recent command, simply to indicate that it is the most recent one.

The command descriptor :x-23 is synonymous with (:x -23). More generally, every symbol in the keyword package whose first character is #\x and whose remaining characters parse as a negative integer is appropriately understood. This allows :pbt :x-10 where :pbt (:max -10) or :pbt (:here -10) were previously used. The old forms are still legal.

The order of the arguments to defcong has been changed.

The simplifier now reports the use of unspecified built-in type information about the primitives with the phrase ``primitive type reasoning.'' This phrase may sometimes occur in situations where ``propositional calculus'' was formerly credited with the proof.

The function pairlis has been replaced in the code by a new function pairlis$, because Common Lisp does not adequately specify its pairlis function.

Some new Common Lisp functions have been added, including logtest, logcount, integer-length, make-list, remove-duplicates, string, and concatenate. The source file /slocal/src/acl2/axioms.lisp is the ultimate reference regarding Common Lisp functions in Acl2.

The functions defuns and theory-invariant have been documented. See defuns and see theory-invariant.

A few symbols have been added to the list *acl2-exports*.

A new key has been implemented for the acl2-defaults-table, :irrelevant-formals-ok. See set-irrelevant-formals-ok.

The connected book directory, cbd, must be nonempty and begin and end with a slash. It is set (and displayed) automatically upon your first entry to lp. You may change the setting with set-cbd. See cbd.

:oops will undo the last :ubt. See oops.

Documentation has been written about the ordinals. See e0-ordinalp and see e0-ord-<.

The color events -- (red), (pink), (blue), and (gold) -- may no longer be enclosed inside calls of local, for soundness reasons. In fact, neither may any event that sets the acl2-defaults-table. See embedded-event-form.

See ld-keyword-aliases for an example of how to change the exit keyword from :q to something else.

The attempt to install a monitor on :rewrite rules stored as simple abbreviations now causes an error because the application of abbreviations is not tracked.

A new message is sometimes printed by the theorem prover, indicating that a given simplification is ``specious'' because the subgoals it produces include the input goal. In Version 1.4 this was detected but not reported, causing behavior some users found bizarre. See specious-simplification.

:Definition rules are no longer always required to specify the :clique and :controller-alist fields; those fields can be defaulted to system-determined values in many common instances. See definition.

A warning is printed if a macro form with keyword arguments is given duplicate keyword values. Execute (thm t :doc nil :doc "ignored") and read the warning printed.

A new restriction has been placed on encapsulate. Non-local recursive definitions inside the encapsulate may not use, in their tests and recursive calls, the constrained functions introduced by the encapsulate. See subversive-recursions. (Note added in Version 2.3: Subversive recursions were first recognized by us here in Version 1.5, but our code for recognizing them was faulty and the bug was not fixed until Version 2.3.)

The events defequiv, defcong, defrefinement, and defevaluator have been reimplemented so that they are just macros that expand into appropriate defthm or encapsulate events; they are no longer primitive events. See the documentation of each affected event.

The defcor event, which was a shorthand for a defthm that established a corollary of a named, previously proved event, has been eliminated because its implementation relied on a technique we have decided to ban from our code. If you want the effect of a defcor in Version 1.5 you must submit the corresponding defthm with a :by hint naming the previously proved event.

Error reporting has been improved for inappropriate in-theory hints and events, and for syntax errors in rule classes, and for non-existent filename arguments to ld.

Technical Note: We now maintain the Third Invariant on type-alists, as described in the Essay on the Invariants on Type-alists, and Canonicality. This change will affect some proofs, for example, by causing a to rewrite more quickly to c when (equiv a b) and (equiv b c) are both known and c is the canonical representative of the three.

NOTE6

Major Section:  RELEASE-NOTES

A new key has been implemented for the acl2-defaults-table, :ignore-ok. See set-ignore-ok.

It is now legal to have color events, such as (red), in the portcullis of a book. More generally, it is legal to set the acl2-defaults-table in the portcullis of a book. For example, if you execute :red and then certify a book, the event (red) will show up in the portcullis of that book, and hence the definitions in that book will all be red (except when overridden by appropriate declarations or events). When that book is included, then as always, its portcullis must first be ``raised,'' and that will cause the default color to become red before the events in the book are executed. As always, the value of acl2-defaults-table immediately after execution of an include-book, certify-book, or encapsulate form will be the same as it was immediately before execution (and hence, so will the default color). See portcullis and, for more about books, see books.

A theory ground-zero has been defined to contain exactly those rules that are enabled when Acl2 starts up. See ground-zero.

The function nth is now enabled, correcting an oversight from Version 1.5.

Customization files no longer need to meet the syntactic restrictions put on books; rather, they can contain arbitrary Acl2 forms. See acl2-customization.

Structured directory names and structured file names are supported; see especially the documentation for pathname, book-name, and cbd.

Acl2 now works with some Common Lisp implementations other than akcl, including Lucid, Allegro, and MCL.

A facility has been added for displaying proof trees, especially using emacs; see proof-tree.

There is a considerable amount of new documentation, in particular for the printing functions fmt, fmt1, and fms, and for the notion of Acl2 term (see term).

It is possible to introduce new well-founded relations, to specify which relation should be used by defun, and to set a default relation. See well-founded-relation.

It is possible to make functions suggest new inductions. See induction.

It is possible to change how Acl2 expresses type-set information; in particular, this affects what clauses are proved when forced assumptions are generated. See type-set-inverter.

A new restriction has been added to defpkg, having to do with undoing. If you undo a defpkg and define the same package name again, the imports list must be identical to the previous imports or else an explanatory error will occur. See package-reincarnation-import-restrictions.

Theory-invariant and set-irrelevant-formals-ok are now embedded event forms.

The command :good-bye may now be used to quit entirely out of Lisp, thus losing your work forever. This command works in akcl but may not work in every Common Lisp.

A theory ground-zero has been added that contains exactly the enabled rules in the startup theory. See ground-zero.

Define-pc-macro and define-pc-atomic-macro now automatically define :red functions. (It used to be necessary, in general, to change color to :red before invoking these.)

For a proof of the well-foundedness of e0-ord-< on the e0-ordinalps, see proof-of-well-foundedness.

Free variables are now handled properly for hypotheses of :type-prescription rules.

When the system is loaded or saved, state is now bound to *the-live-state*.

Certify-book has been modified so that when it compiles a file, it loads that object file.

Defstub has been modified so that it works when the color is hot (:red or :pink).

Several basic, but not particularly commonly used, events have been added or changed. The obscure axiom symbol-name-intern has been modified. The definition of firstn has been changed. Butlast is now defined. The definition of integer-length has been modified. The left-hand side of the rewrite rule rational-implies2 has been changed from (* (numerator x) (/ (denominator x))) to (* (/ (denominator x)) (numerator x)), in order to respect the fact that unary-/ is invisible with respect to binary-*. See loop-stopper.

The `preprocess' process in the waterfall (see hints for a discussion of the :do-not hint) has been changed so that it works to avoid case-splitting. The `simplify' process refuses to force (see force) when there are if terms, including and and or terms, in the goal being simplified.

The function apply is no longer introduced automatically by translation of user input to internal form when functions are called on inappropriate explicit values, e.g., (car 3).

The choice of which variable to use as the measured variable in a recursive definition has been very slightly changed.

NOTE7

Major Section:  RELEASE-NOTES

Include-book now takes (optionally) an additional keyword argument, indicating whether a compiled file is to be loaded. The default behavior is unchanged, except that a warning is printed when a compiled file is not loaded. See include-book.

A markup language for documentation strings has been implemented, and many of the source files have been marked up using this language (thanks largely to the efforts of Laura Lawless). See markup. Moreover, there are translators that we have used to provide versions of the ACL2 documentation in info (for use in emacs), html (for Mosaic), and tex (for hardcopy) formats.

A new event defdoc has been implemented. It is like deflabel, but allows redefinition of doc strings and has other advantages. See defdoc.

We used to ignore corollaries when collecting up the axioms introduced about constrained functions. That bug has been fixed. We thank John Cowles for bringing this bug to our attention.

The macro defstub now allows a :doc keyword argument, so that documentation may be attached to the name being introduced.

A new command nqthm-to-acl2 has been added to help Nqthm users to make the transition to ACL2. See nqthm-to-acl2, which also includes a complete listing of the relevant tables.

Many function names, especially of the form ``foo-lst'', have been changed in order to support the following convention, for any ``foo'':

(foo-listp lst) represents the notion (for x in lst always foop x).

Accumulated persistence has been implemented. It is not connected to :brr or rule monitoring. See accumulated-persistence.

:Trigger-terms has been added for :linear rule classes, so you can hang a linear rule under any addend you want. See linear, which has been improved and expanded.

ACL2 now accepts 256 characters and includes the Common Lisp functions code-char and char-code. However, ACL2 controls the lisp reader so that #\c may only be used when c is a single standard character or one of Newline, Space, Page, Rubout, Tab. If you want to enter other characters use code-char, e.g., (coerce (list (code-char 7) (code-char 240) #a) 'string). See characters. Note: our current handling of characters makes the set of theorems different under Macintosh Common Lisp (MCL) than under other Common Lisps. We hope to rectify this situation before the final release of ACL2.

A new table, macro-aliases-table, has been implemented, that associates macro names with function names. So for example, since append is associated with binary-append, the form (disable append) it is interpreted as though it were (disable binary-append). See macro-aliases-table, see add-macro-alias and see remove-macro-alias.

The implementation of conditional metalemmas has been modified so that the metafunction is applied before the hypothesis metafunction is applied. See meta.

The Common Lisp functions acons and endp have been defined in the ACL2 logic.

We have added the symbol declare to the list *acl2-exports*, and hence to the package "ACL2-USER".

A new hint, :restrict, has been implemented. See hints.

It used to be that if :ubt were given a number that is greater than the largest current command number, it treated that number the same as :max. Now, an error is caused.

The table :force-table has been eliminated.

A command :disabledp (and macro disabledp) has been added; see disabledp.

Compilation via :set-compile-fns is now suppressed during include-book. In fact, whenever the state global variable ld-skip-proofsp has value 'include-book.

Here are some less important changes, additions, and so on.

Unlike previous releases, we have not proved all the theorems in axioms.lisp; instead we have simply assumed them. We have deferred such proofs because we anticipate a fairly major changed in Version 1.8 in how we deal with guards.

We used to (accidentally) prohibit the ``redefinition'' of a table as a function. That is no longer the case.

The check for whether a corollary follows tautologically has been sped up, at the cost of making the check less ``smart'' in the following sense: no longer do we expand primitive functions such as implies before checking this propositional implication.

The command ubt! has been modified so that it never causes or reports an error. See ubt!.

ACL2 now works in Harlequin Lispworks.

The user can now specify the :trigger-terms for :linear rules. See linear.

The name of the system is now ``ACL2''; no longer is it ``Acl2''.

The raw lisp counterpart of theory-invariant is now defined to be a no-op as is consistent with the idea that it is just a call of table.

A bug was fixed that caused proof-checker instructions to be executed when ld-skip-proofsp was t.

The function rassoc has been added, along with a corresponding function used in its guard, r-eqlable-alistp.

The in-theory event and hint now print a warning not only when certain ``primitive'' :definition rules are disabled, but also when certain ``primitive'' :executable-counterpart rules are disabled.

The modified version of trace provided by ACL2, for use in raw Lisp, has been modified so that the lisp special variable *trace-alist* is consulted. This alist associates, using eq, values with their print representations. For example, initially *trace-alist* is a one-element list containing the pair (cons state '|*the-live-state*|).

The system now prints an observation when a form is skipped because the default color is :red or :pink. (Technically: when-cool has been modified.)

Additional protection exists when you submit a form to raw Common Lisp that should only be submitted inside the ACL2 read-eval-print loop.

Here is a complete list of the changes in function names described near the top of this note, roughly of the form

foo-lst --> foo-listp

symbolp-listp    --> symbol-listp
list-of-symbolp-listp  --> symbol-list-listp
                       {for consistency with change to symbol-listp}
rational-lst     --> rational-listp
                     {which in fact was already defined as well}
integer-lst      --> integer-listp
character-lst    --> character-listp
stringp-lst      --> string-listp
32-bit-integer-lst   --> 32-bit-integer-listp
typed-io-lst     --> typed-io-listp
open-channel-lst --> open-channel-listp
readable-files-lst   --> readable-files-listp
written-file-lst --> written-file-listp
read-file-lst    --> read-file-listp
writeable-file-lst   --> writable-file-listp
                     {note change in spelling of ``writable''}
writeable-file-lst1  --> writable-file-listp1
pseudo-termp-lst     --> pseudo-term-listp
hot-termp-lst --> hot-term-listp {by analogy with pseudo-term-listp}
weak-termp-lst   --> weak-term-listp
weak-termp-lst-lst   --> weak-termp-list-listp
ts-builder-case-lstp -> ts-builder-case-listp
quotep-lst       --> quote-listp
termp-lst        --> term-listp
instr-lst        --> instr-listp
spliced-instr-lst    --> spliced-instr-listp
rewrite-fncallp-lst  --> rewrite-fncallp-listp
every-occurrence-equiv-hittablep1-lst -->
            every-occurrence-equiv-hittablep1-listp
some-occurrence-equiv-hittablep1-lst  -->
            some-occurrence-equiv-hittablep1-listp
            {by analogy with the preceding, even though it's a
             ``some'' instead of ``all'' predicate]
almost-quotep1-lst   --> almost-quotep1-listp
ffnnames-subsetp-lst --> ffnnames-subsetp-listp
boolean-lstp     --> boolean-listp
subst-expr1-lst-okp  --> subst-expr1-ok-listp

NOTE8

Major Section:  RELEASE-NOTES

See note8-update for yet more recent changes.

Guards have been eliminated from the ACL2 logic. A summary is contained in this brief note. Also see defun-mode and see set-guard-checking.

Guards may be included in defuns as usual but are ignored from the perspective of admission to the logic: functions must terminate on all arguments.

As in Nqthm, primitive functions, e.g., + and car, logically default unexpected arguments to convenient values. Thus, (+ 'abc 3) is 3 and (car 'abc) is nil. See programming, and see the documentation for the individual primitive functions.

In contrast to earlier versions of ACL2, Version 1.8 logical functions are executed at Nqthm speeds even when guards have not been verified. In versions before 1.8, such functions were interpreted by ACL2.

Colors have been eliminated. Two ``defun-modes'' are supported, :program and :logic. Roughly speaking, :program does what :red used to do, namely, allow you to prototype functions for execution without any proof burdens. :Logic mode does what :blue used to do, namely, allow you to add a new definitional axiom to the logic. A global default-defun-mode is comparable to the old default color. The system comes up in :logic mode. To change the global defun-mode, type :program or :logic at the top-level. To specify the defun-mode of a defun locally use

(declare (xargs :mode mode)).

The prompt has changed. The initial prompt, indicating :logic mode, is

ACL2 !>

ACL2 p!>

Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function ``should'' have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. If a guard is specified, as with xargs :guard, then it is ``verified'' at defun-time (unless you also specify xargs :verify-guards nil). Guard verification means what it always has: the input guard is shown to imply the guards on all subroutines in the body. If the guards of a function are verified, then a call of the function on inputs satisfying the guard can be computed directly by Common Lisp. Thus, verifying the guards on your functions will allow them to execute more efficiently. But it does not affect their logical behavior and since you will automatically get Nqthm speeds on unverified logical definitions, most users will probably use guards either as a specification device or only use them when execution efficiency is extremely important.

Given the presence of guards in the system, two issues are unavoidable. Are guards verified as part of the defun process? And are guards checked when terms are evaluated? We answer both of those questions below.

Roughly speaking, in its initial state the system will try to verify the guards of a defun if a :guard is supplied in the xargs and will not try otherwise. However, guard verification in defun can be inhibited ``locally'' by supplying the xargs :verify-guards nil. ``Global'' inhibition can be obtained via the :set-verify-guards-eagerness. If you do not use the :guard xargs, you will not need to think about guard verification.

We now turn to the evaluation of expressions. Even if your functions contain no guards, the primitive functions do and hence you have the choice: when you submit an expression for evaluation do you mean for guards to be checked at runtime or not? Put another way, do you mean for the expression to be evaluated in Common Lisp (if possible) or in the logic? Note: If Common Lisp delivers an answer, it will be the same as in the logic, but it might be erroneous to execute the form in Common Lisp. For example, should (car 'abc) cause a guard violation error or return nil?

The top-level ACL2 loop has a variable which controls which sense of execution is provided. To turn ``guard checking on,'' by which we mean that guards are checked at runtime, execute the top-level form :set-guard-checking t. To turn it off, do :set-guard-checking nil. The status of this variable is reflected in the prompt.

ACL2 !>

ACL2 >

ACL2 !>(car 'abc)

ACL2 >(car 'abc)

Note that whether or not guards are checked at runtime is independent of whether you are operating in :program mode or :logic mode and whether theorems are being proved or not. (Although it must be added that functions defined in :program mode cannot help but check their guards because no logical definition exists.)

Version 1.8 permits the verification of the guards of theorems, thus insuring that all instances of the theorem will evaluate without error in Common Lisp. To verify the guards of a theorem named name execute the event

(verify-guards name).

Caveat about verify-guards: implies is a function symbol, so in the term (implies p q), p cannot be assumed true when q is evaluated; they are both evaluated ``outside.'' Hence, you cannot generally verify the guards on a theorem if implies is used to state the hypotheses. Use if instead. In a future version of ACL2, implies will likely be a macro.

See sum-list-example.lisp for a nice example of the use of Version 1.8. This is roughly the same as the documentation for guard-example.

We have removed the capability to do ``old-style-forcing'' as existed before Version 1.5. See note5.

NOTE: Some low level details have, of course, changed. One such change is that there are no longer two distinct type prescriptions stored when a function is admitted with its guards verified. So for example, the type prescription rune for binary-append is now

(:type-prescription binary-append)

(:type-prescription binary-append . 1)
(:type-prescription binary-append . 2)

Nqthm-style forcing on linear arithmetic assumptions is no longer executed when forcing is disabled.

Functional instantiation now benefits from a trick also used in Nqthm: once a constraint generated by a :functional-instance lemma instance (see lemma-instance) has been proved on behalf of a successful event, it will not have to be re-proved on behalf of a later event.

1+ and 1- are now macros in the logic, not functions. Hence, for example, it is ``safe'' to use them on left-hand sides of rewrite rules, without invoking the common warning about the presence of nonrecursive function symbols.

A new documentation section file-reading-example illustrates how to process forms in a file.

A new proof-checker command forwardchain has been added; see acl2-pc::forwardchain.

It is now possible to use quantifiers. See defun-sk and see defchoose.

There is a new event set-inhibit-warnings, which allows the user to turn off warnings of various types. see set-inhibit-warnings.

An unsoundness relating encapsulate and :functional-instance hints has been remedied, with a few small effects visible at the user level. The main observable effect is that defaxiom and non-local include-book events are no longer allowed in the scope of any encapsulate event that has a non-empty signature.

When certify-book is called, we now require that the default defun-mode (see default-defun-mode) be :logic. On a related note, the default defun-mode is irrelevant to include-book; the mode is always set to :logic initially, though it may be changed within the book and reverts to its original value at the conclusion of the include-book. A bug in include-book prevented it from acting this way even though the documentation said otherwise.

The documentation has been substantially improved. A new section ``Programming'' contains documentation of many useful functions provided by ACL2; see programming. Also, the documentation has been ``marked up'' extensively. Thus in particular, users of Mosaic will find many links in the documentation.

The symbols force, mv-nth, and acl2-count have been added to the list *acl2-exports*.

We now permit most names from the main Lisp package to be used as names, except for names that define functions, macros, or constants. See name.

We have changed the list of imports from the Common Lisp package to ACL2, i.e., the list *common-lisp-symbols-from-main-lisp-package*, to be exactly those external symbols of the Common Lisp package as specified by the draft Common Lisp standard. In order to accommodate this change, we have renamed some ACL2 functions as shown below, but these and other ramifications of this change should be transparent to most ACL2 users.

warning      --> warning$
print-object --> print-object$

Proof trees are no longer enabled by default. To start them up, :start-proof-tree.

We have added the capability of building smaller images. The easiest way to do this on a Unix (trademark of AT&T) system is: make small.

Here we will put some less important changes, additions, and so on.

We have added definitions for the Common Lisp function position (for the test eql), as well as corresponding versions position-equal and position-eq that use tests equal and eq, respectively. See position, see position-equal, and see position-eq.

The defthm event rational-listp-implies-rationalp-car no longer exists.

We fixed a bug in the hint mechanism that applied :by, :cases, and :use hints to the first induction goal when the prover reverted to proving the original goal by induction.

We fixed a bug in the handling of (set-irrelevant-formals-ok :warn).

In support of removing the old-style forcing capability, we deleted the initialization of state global old-style-forcing and deleted the definitions of recover-assumptions, recover-assumptions-from-goal, remove-assumptions1, remove-assumptions, and split-on-assumptions, and we renamed split-on-assumptions1 to split-on-assumptions.

The special value 'none in the proof-checker commands claim and = has been replaced by :none.

A bug in the handling of hints by subgoals has been fixed. For example, formerly a :do-not hint could be ``erased'' by a :use hint on a subgoal. Thanks go to Art Flatau for noticing the bug.

The functions weak-termp and weak-term-listp have been deleted, and their calls have been replaced by corresponding calls of pseudo-termp and pseudo-term-listp. The notion of pseudo-termp has been slightly strenthened by requiring that terms of the form (quote ...) have length 2.

Performance has been improved in various ways. At the prover level, backchaining through the recognizer alist has been eliminated in order to significantly speed up ACL2's rewriter. Among the other prover changes (of which there are several, all technical): we no longer clausify the input term when a proof is interrupted in favor of inducting on the input term. At the IO level, we have improved performance somewhat by suitable declarations and proclamations. These include technical modifications to the macros mv and mv-let, and introduction of a macro the-mv analogous to the macro the but for forms returning multiple values.

The function spaces now takes an extra argument, the current column.

A bug in the proof-checker equiv command was fixed.

The function intersectp has been deleted, because it was essentially duplicated by the function intersectp-equal.

We now proclaim functions in AKCL and GCL before compiling books. This should result in somewhat increased speed.

The function repeat has been eliminated; use make-list instead.

The proof-checker command expand has been fixed so that it eliminates let (lambda) expressions when one would expect it to.

A new primitive function, mv-nth, has been introduced. Mv-nth is equivalent to nth and is used in place of nth in the translation of mv-let expressions. This allows the user to control the simplification of mv-let expressions without affecting how nth is treated. In that spirit, the rewriter has been modified so that certain mv-nth expressions, namely those produced in the translation of (mv-let (a b c)(mv x y z) p), are given special treatment.

A minor bug in untranslate has been fixed, which for example will fix the printing of conjunctions.

Translate now takes a logicp argument, which indicates whether it enforces the restriction that :program mode functions do not occur in the result.

The modified version of trace provided by ACL2, for use in raw Lisp, has been modified so that the lisp special variable *trace-alist* has a slightly different functionality. This alist associates, using eq, symbols with the print representations of their values. For example, initially *trace-alist* is a one-element list containing the pair (cons 'state '|*the-live-state*|). Thus, one may cons the pair (cons '*foo* "It's a FOO!") on to *trace-alist*; then until *foo* is defined, this change will have no effect, but after for example

(defconst *foo* 17)

Trace also traces the corresponding logic function.

Proof-tree display has been improved slightly in the case of successful proofs and certain event failures.

The function positive-integer-log2 has been deleted.

The macro skip-proofs now prints a warning message when it is encountered in the context of an encapsulate event or a book. See skip-proofs.

Some functions related to the-fn and wormhole1 now have defun-mode :program, but this change is almost certain to be inconsequential to all users.