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