NOTE-2-9-3

Major Section:  RELEASE-NOTES

Also see note-2-9-1 and see note-2-9-2 for other changes since the last non-incremental release (Version_2.9).

We fixed a soundness bug that exploited the ability to define :program mode functions that are improperly guarded, and then to use those functions in defconst forms. The fix is to evaluate defconst forms using the same ``safe-mode'' that is used in macroexpansion (see guards-and-evaluation). Here is a proof of nil that succeeded in Allegro Common Lisp (but not, for example, GCL). See also a long comment in source function defconst-fn for an examploe that does not require the use of :set-guard-checking.

:set-guard-checking nil ; execute before certifying the book below


(in-package "ACL2")


(encapsulate
 ()
 (local (defun f1 ()
          (declare (xargs :mode :program))
          (char-upcase (code-char 224))))
 (local (defconst *b* (f1)))
 (defun f1 ()
   (char-upcase (code-char 224)))
 (defconst *b* (f1))
 (defthm bad
   (not (equal *b* (code-char 224)))
   :rule-classes nil))


(defthm ouch
  nil
  :hints (("Goal" :use bad))
  :rule-classes nil)

We fixed a soundness hole due to the fact that the "LISP" package does not exist in OpenMCL. We now explicitly disallow this package name as an argument to defpkg. Thanks to Bob Boyer and Warren Hunt for bringing an issue to our attention that led to this fix.

ACL2 now requires all package names to consist of standard characters (see standard-char-p, none of which is lower case. The reason is that we have seen at least one lisp implementation that does not handle lower case package names correctly. Consider for example the following raw lisp log (some newlines omitted).

>(make-package "foo")
#<"foo" package>
>(package-name (symbol-package 'FOO::A))
"foo"
>(package-name (symbol-package '|FOO|::A))
"foo"
>

Added newline, add-to-set-eql, the-fixnum, and the-fixnum! to *acl2-exports*. Thanks to Jared Davis for bringing these to our attention.

Added a line to acl2.lisp to support CMUCL running on Mac OSX, thanks to a suggestion from Fabricio Chalub Barbosa do Rosario.

The executable scripts for saved ACL2 images now include $*, so that command-line arguments will be passed along.

(For GCL profiling only) Fixed a colon (:) that should have been a semicolon (;) in file save-gprof.lsp. Thanks to David Hardin for pointing out this bug.

The documentation for :elim rules has been expanded and improved, thanks to useful feedback from Hanbing Liu.

Fixed a bug in the guard for function include-book-dir.

For those who want to experiment with an alternate implementation of mv and mv-let, there is now support for under-the-hood implementation of these in terms of raw Lisp functions values and multiple-value-bind, respectively. The regression suite has seen about a 10% speed-up in Allegro CL and about an 8% slowdown in GCL for builds with this change. See the makefile (GNUmakefile) for examples of how to build ACL2 by including the feature, :acl2-mv-as-values. Source file init.lsp has been renamed to init.lisp in support of this change (technical detail: otherwise GCL loads the init file too soon, before its -eval argument is evaluated). Thanks to David Rager for inspiring this change, by pointing out the problematic use of globals by the existing mv implementation from the standpoint of supporting parallel evaluation. This capability is experimental: there is likely to be some remaining work to be done on it.

A change related to the one just above is that we now limit the maximum number of arguments to any call of mv to 32. Thanks to Bob Boyer for raising a question that lead to this change.

Eliminated some compiler warnings in OpenMCL.

In the rtl library (books/rtl/rel4/), functions bits and setbits have had their guards improved (as they had been too restrictive, especially for setbits).

A new function time$ permits timing of forms, by using (under the hood) the host Common Lisp's time utility.

We fixed an infinite loop that could occur during destructor elimination (see elim). Thanks to Sol Swords to bringing this to our attention and sending a nice example, and to Doug Harper for sending a second example that we also found useful.

The method of speeding up GCL-based builds (see note-2-9-2) has changed slightly from Version_2.9.2. Now, in the make command:

  LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

We improved the pretty-printer's handling of keywords. For example, before this change one might see the following printed by ACL2.

(MODIFY TH S :KEY1 VAL1 :KEY2
        (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

(MODIFY TH S
        :KEY1 VAL1
        :KEY2 (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

(GCL ONLY) Evaluation in a break is no longer inhibited by ACL2 when built on top of GCL, so GCL now matches other Common Lisps in this respect.

For ACL2 built on most host Common Lisps, you will see the string [RAW LISP] in the prompt, at least at a break, to emphasize that one is inside a break and hence should probably quit from the break. See breaks.

Jared Davis suggested improvements to lemmas len-update-nth (in source file axioms.lisp) and append-true-listp-type-prescription (in books/meta/term-defuns.lisp), which have been incorporated. The former required a change in books/workshops book 2004/ruiz-et-al/support/q-dag-unification.cert, which has been made.

The proof-checker command rewrite allows further binding of free variables in hypootheses, with new optional argument instantiate-free. Proof-checker command show-rewrites (sr) gives corresponding additional information. Documentation for these commands has been improved; see proof-checker-commands. Thanks to John Matthews and Bill Young for suggestions and feedback leading to these improvements.

Fixed downcase printing so that the package name of a symbol is also downcased. For example, after execution of (defpkg "FOO" nil) and (set-acl2-print-case :downcase), 'foo::ab will print back as the same, rather than as 'FOO::ab.

It is now possible to control the output so that numbers are printed in binary, octal, or hex, though the default is still radix 10. See set-acl2-print-base. Note that in support of this change, built-in functions explode-nonnegative-integer and explode-atom now take an extra print-base argument. Different support for radix conversion may be found in a book newly contributed by Jun Sawada, books/misc/radix.lisp.

Built-in axiom car-cdr-elim is now only an :elim rule. It was formerly both an :elim rule and a :rewrite rule. A new rule, cons-car-cdr, takes the place of the old :rewrite rule, but is instead a hypothesis-free rule that can cause a case split (see source file axioms.lisp). Thanks to Jared Davis for suggesting this change.

Lemmas about alphorder (alphorder-reflexive, alphorder-transitive, alphorder-anti-symmetric, and alphorder-total) are now available. (They had been local in source file axioms.lisp.) Thanks to Serita Nelesen for bringing this issue to our attention.

ACL2 has, for some time, printed a space in the event summary after the open parenthesis for a defthm event, in order to ease backward searching for the original form, for example (defthm bar ...):

Form:  ( DEFTHM BAR ...)

In analogy to include-book, now ld takes the (optional) keyword argument :dir. Thanks to Jared Davis for providing an implementation of this feature and to Eric Smith and Jeff Marshall for requesting this feature.

We fixed a bug in include-book that could cause an error when redefinition is on, for example:

(set-ld-redefinition-action '(:warn! . :overwrite) state)
(include-book "/u/acl2/books/arithmetic/top")

The behavior of include-book now matches the documentation: handling of compiled files for uncertified books will follow the same rules as for certified books. In particular, if you create an object file in raw Lisp for some book, then including that book will load that object file. Thanks to Jared Davis for bringing this issue to our attention.

New documentation explains the interaction of redefinition and redundancy. See redundant-events -- the ``Note About Unfortunate Redundancies'' is new. Thanks to Grant Passmore for providing examples that led us to write this additional documentation.

Solutions to exercises in ``How To Prove Theorems Formally'' (http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms) are now available in distributed book books/misc/how-to-prove-thms.lisp. Also in that directory may be found a new book hanoi.lisp that contains a solution to the Towers of Hanoi problem.

• NOTE-2-9-3-PPR-CHANGE -- change in pretty-printing for ACL2 Version_2.9.3