Changes in Version 3.0 since Version 2.9.4
Fixed a bug in cw-gstack that was causing a hard error when attempting to report on a forced assumption. Thanks to Jared Davis for pointing this out and sending an example that helped us to determine a fix.
Added set-backchain-limit to the set of legal events that can be placed in encapsulate forms and books. Thanks to John Cowles for bringing this issue to our attention.
Fixed a bug that broke
Guard verification now evaluates ground subexpressions (those with no free variables) when computing the guard conjecture for the body of a function. Thanks to Jared Davis for useful conversations leading to this change. See verify-guards, in particular its ``Note on computation of guard conjectures and evaluation'' near the end of that topic, for more details.
Added a warning when a theory-invariant is redefined. Thanks to Jared Davis for suggesting a warning in this case and providing an informative example. Also, theory-invariants are now maintained more completely, as they are checked at the end of every event except for events executed on behalf of an include-book or the second pass of an encapsulate.
Fixed the handling of runic designators to match their specification (see theories), so that disabling the name of a defthm event disables all rules generated for that event.
(For those who do numerous builds using feature
Arranged that traced functions (see trace$) are automatically untraced when events are undone (for example see ubt), at least for most underlying Common Lisp implementations.
The macro defun-sk now creates non-executable functions, which allows stobjs to be used where they had previously been prohibited. More generally, the user now has control over declare forms to be used by the underlying defun'd function; see defun-sk. Thanks to Sandip Ray for pointing out the need for such a modification.
Constraints for functional instantiation now use the original definition rather than a simplified (``normalized'') version of it.
Fixed a bug that caused the prompt to stay the same when guard-checking is off (see set-guard-checking) and raw-mode is changed (see set-raw-mode).
Lemma names in directory
Fixed proof-tree output so that failed non-proof events do not cause the proof-tree to be re-printed. Thus for example, if you have already advanced the checkpoint marker, it will not be reset by subsequent failed non-proof events. Thanks to Pete Manolios and Peter Dillinger for bringing this bug to our attention.
Fixed a bug that was preventing the printing of stobj fields as constants instead of numbers in certain cases. (Note that this bug only affected printing, not soundness.) Thanks to Eric Smith for bringing this problem to our attention and providing the following example (which now works fine).
(defstobj st fld1 fld2) (in-theory (disable update-nth)) (defund run (st) (declare (xargs :stobjs (st))) ;adding this didn't seem to help.. st) ;works great; *fld1* prints as *fld1* (thm (equal (update-nth *fld1* 'abc st) (car (cons x y)))) ;*fld1* gets printed as 0, presumably because the call to run intervenes. (thm (equal (update-nth *fld1* 'abc (run st)) (car (cons x y))))
The macro progn now allows the use of macros defined within its bodies even when at the event level, as illustrated by the following example.
(progn (defmacro my-defun (&rest args) `(defun ,@args)) (my-defun g (x) x))
Thanks to Anna Slobodova for bringing this issue to our attention. A related change is that all arguments of progn must now be embedded event forms (see embedded-event-form), so use er-progn instead if this is not the case.
The change to progn mentioned above also fixes a bug in handling local events inside a progn that is inside an encapsulate or in a book. For example, the following form formerly caused an error.
(encapsulate () (defun foo (x) x) (progn (local (defun bar (x) x)) (defun abc (x) x)))
We fixed two bugs in
(include-book "foo") (defthm test-thm (equal x x) :rule-classes nil)
If we now execute
A new event, make-event, provides something like macros that take
state. For example, one can use it to put tests into certified books, do
proof search, and generate new function names. Many examples appear in
In support of make-event, which is described in the preceding
We fixed a soundness bug that did not correctly detect local events. For example, the following event was admitted.
(encapsulate () (local (encapsulate () (local (progn (program))) ; or, (local (with-output :off summary (program))) (set-irrelevant-formals-ok t) (defun foo (x) (declare (xargs :measure (acl2-count x))) (1+ (foo x))))) (defthm inconsistent nil :hints (("Goal" :use foo)) :rule-classes nil))
A new value for guard checking,
In the course of adding the guard-checking value
The ACL2 hyper-card has been enhanced, thanks to David Rager, with a
listing of ``Useful EMACS Commands'' to match comments in
Users contributed books following the
Made some improvements to
(Only OpenMCL and, with feature
The default stack size has been increased for several lisps.
(Very technical) A restriction has been weakened on the use of local stobjs under a call of an ACL2 evaluator (
The notion of ``ancestor'' has been changed slightly. This notion is used
by extended metafunctions and break-rewrite (see extended-metafunctions and see brr@), and also with backchain limits
(see backchain-limit and see set-backchain-limit). Basically,
each time a hypothesis is encountered during application of a rewrite
rule, that hypothesis is pushed (after instantiating and negating) onto the
current list of ancestors before it is rewritten. However, hypotheses of the
Termination and induction analysis now continue through both arguments of prog2$, not just the second. (Normally, the gathering up of if tests stops at function calls; but it continued through the second argument of prog2$, and now it will continue through both arguments.) Thanks to Sol Swords for discussion leading to this change.
The ACL2 distribution is now kept on the http server rather than the ftp server (but the home page has not been moved). Thanks to Robert Krug for letting us know that some ACL2 users have found it inconvenient to fetch ACL2 using ftp.