• 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-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

• Release-notes

Note-1-9

ACL2 Version 1.9 (Fall, 1996) Notes

By default, when the system is started it is illegal to use the variable state as a formal parameter of a function definition. The aim is to prevent novice users from stumbling into the Byzantine syntactic restrictions on that variable symbol. Use

:set-state-ok t

or, equivalently,

(set-state-ok t)

to switch back to the old default mode. See set-state-ok

Set-state-ok is an event that affects the ACL2 defaults table (see ACL2-defaults-table). Recall that when books are included, the defaults table is restored to its pre-inclusion state. Thus, while a set-state-ok form will permit the book to define a state-using function, it will not permit the user of the book to make such a definition. We recommend putting (set-state-ok t) in any book that defines a state using function.

Books certified under Version 1.8 must be recertified under Version 1.9. See :DOC version.

The simplifier has been made to look out for built-in clauses, whereas in past versions such clauses were only noticed by the ``preprocessor'' at the top of the waterfall. THIS CHANGE MAY PREVENT OLD SCRIPTS FROM REPLAYING! The undesirable side-effect is caused by the fact that :HINTS require you to refer to clauses by their exact name (see goal-spec) and because the new simplifier proves more clauses than before, the goals produced have different names. Thus, if a script uses :HINTS that refer to clauses other than "Goal", e.g., "Subgoal 1.3" then the hint may be applied to a different subgoal than originally intended.

The use of built-in-clauses has been made more efficient. If a set of clauses arise often in a piece of work, it might be advantageous to build them in even if that results in a large set (hundreds?) of built-in clauses. See built-in-clause

Wormholes can now be used in :logic mode functions. See wormhole

It is now possible to provide ``computed hints.'' For example, have you ever wished to say ``in all goals with a name like this, :use that'' or ``if this term is in the subgoal, then :use that''? Well, see computed-hints and the extraordinarily long example in see using-computed-hints.

Hide terms may be rewritten with :rewrite rules about hide. See hide, where we also now explain why hide terms are sometimes introduced into your proof attempts.

A bug that sometimes caused the ``non-lazy IF'' hard error message was fixed.

A bug that sometimes caused a hard error in forward chaining was fixed.

A bug in print-rules (:pr) was fixed.

We report the use of :executable-counterparts in the evaluation of SYNTAXP forms.

Some documentation errors were fixed.

A bug in parent-tree tracking in add-literal-and-pt was fixed.

A bug in ok$, go$ and eval$ was fixed.

Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.