• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
            • Note-2-6-proofs
            • Note-2-6-new-functionality
            • Note-2-6-other
            • Note-2-6-rules
            • Note-2-6-guards
            • Note-2-6-system
            • Note-2-6-proof-builder
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Note-2-6

Note-2-6-other

ACL2 Version 2.6 Notes on Other (Minor) Changes

Warning strings are now case-insensitive. See set-inhibit-warnings.

ACL2 causes a warning when an in-theory hint or event causes a 0-ary function's definition to be disabled but its :executable-counterpart to be enabled.

A minor modification has been made to defstobj that can have a positive impact on performance in Allegro Common Lisp. (For Lisp hackers: the stobj name was formerly declared special, and that was disabling Allegro's tail-merging routing for compilation of some recursive functions using stobjs.) The downside is that stobj names can no longer be evaluated in raw Lisp. However, raw Lisp is not the right place to be evaluating ACL2 forms anyhow; see set-raw-mode. We thank Rob Sumners for bringing this issue to our attention.

Before Version 2.6, there has been the following problem with defstub and encapsulate in the case that the current package is not the ACL2 package. If a signature was specified using the symbol =>, then that symbol had to have been imported into the current package from the ACL2 package when the current package was defined. There are no longer any package restrictions on the use of =>. Thanks to John Cowles for bringing this problem to our attention.

Bugs in defun-sk have been fixed. Defun-sk forms introducing functions of no arguments were failing to be admitted, for example: (defun-sk always-p1 () (forall (x) (p1 x))). Thanks to John Cowles for bringing this problem to our attention. Also, defun-sk failed on an example in the documentation (see tutorial4-defun-sk-example), as pointed out by Matyas Sustik; this bug has been fixed as well.

The trace mechanism has been fixed to handle stobjs, and to avoid the printing of so-called enabled structures.

The brr command :type-alist now produces more readable output.

An include-book of an uncertified book no longer loads an associated compiled file.

We added a few checks to make sure that the underlying lisp is suitable, for example checking that the reader is case-insensitive and reads in symbols with upper-case names where appropriate.

We now warn when forcing (see force) or immediate force mode (see immediate-force-modep) change state between enabled and disabled. Also see enable-immediate-force-modep and see disable-immediate-force-modep for information about these new macros, which may be used to control immediate force mode.

We have eliminated the use of a low-level raw Lisp constant, *most-recent-multiplicity*. Our test suite saw a speed-up of approximately 2% as a result for an ACL2 image built on GCL (but no significant speed-up for an ACL2 image built on Allegro Common Lisp). We thank Rob Sumners for suggesting this improvement.

Fixnum declarations are now realized as (signed-byte 29) instead of (signed-byte 27). We check that the underlying Common Lisp recognizes objects of type (signed-byte 29) as fixnums, with the exception of CLISP, which is said to have an efficient bignum implementation.

A new documentation topic functional-instantiation-example illustrates functional instantiation.

A bug has been fixed in the monitoring of runes (see monitor). Thanks to Dave Greve for sending an example that clearly showed the problem.

A warning is now issued when it is detected that a :type-prescription rule may not be as strong as it appears because it is not sufficient to prove itself by type reasoning.

An error is caused for rules of class :meta when the function symbol IF is among the :trigger-fns. (IF was ignored anyhow; the point of this change is to avoid misleading the user.)

A minor bug has been fixed in :pr, evident for example if this command was applied to IF.

A minor hole in :set-bogus-mutual-recursion-ok did not permit the acceptance of mutual-recursion forms that include constant function definitions. This has been fixed. Thanks to Eric Smith for coming up with a simple example illustrating the problem.

The temporary files "TMP.lisp" and "TMP1.lisp" written out by :comp are now written to the connected book directory (see cbd).

Previously, the Allegro compiler was not eliminating tail recursion for executable counterparts of functions, because of the way one of its flags had been set. As a result, calls of functions whose guards had not been verified could run out of stack space when this was not necessary. This situation has been fixed.

Executable counterparts could have slow array accesses. This has been fixed (specifically, constants are no longer replaced with their values in the definitions of executable counterparts).

Various improvements have been made to the documentation. Thanks in particular to Eric Smith for pointing out a numbers of places where fixes were in order.

File "mcl-acl2-startup.lisp" has been updated, thanks to feedback from Philippe Georgelin.

Inefficiencies in GCL fixnum computations were remedied for macros +f and *f. Thanks to Rob Sumners for pointing out this issue.