[acl2/acl2] 0820d7: Added with-brr-ens, for queries inside :brr to use...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 0820d70d7d4f93ab1b9a7fc8074ee5d90cc6358f
https://github.com/acl2/acl2/commit/0820d70d7d4f93ab1b9a7fc8074ee5d90cc6358f
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2015-11-29 (Sun, 29 Nov 2015)

Changed paths:
M axioms.lisp
M books/misc/bash-bsd.lisp
M books/misc/bash.lisp
M books/misc/records-bsd.lisp
M books/misc/records.lisp
M books/misc/total-order-bsd.lisp
M books/misc/total-order.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M induct.lisp
M other-events.lisp
M other-processes.lisp
M rewrite.lisp

Log Message:
-----------
Added with-brr-ens, for queries inside :brr to use the current prover theory. Fixed a misleading error message about a disabled function for an :induct hint. Global-enabled-structure is untouchable. In books/misc, turned books *-bsd.lisp into reloc_stub books.

Quoting :doc note-7-2:

A new utility, [with-brr-ens], evaluates its argument inside the
[break-rewrite] loop with respect to the theory currently installed
in the theorem prover, thus taking prover [hints] into account.
Thanks to David Rager for requesting a way for utilities such as
[disabledp] :[pr], and :[pe] to display results at the :[brr]
prompt with respect to the current theory of the prover.

ACL2 no longer prints a message for a failed :induct hint (in the
case that [gag-mode] is off), saying that a definition is
[disable]d when that is not the case.

[State] global variable global-enabled-structure is now untouchable
(see [remove-untouchable]).

There is also the following explanatory comment in (defxdoc note-7-2
...) for the second of the three items above.

; Here is an example of the bug, "ACL2 no longer prints a message for a failed
; @(':induct') hint" (which, by the way, was fixed by passing, to
; induct-msg/lose, the pspv to get the ens, rather than using (ens state)).
;
; (set-gag-mode nil)
; (defund foo (x) (if (consp x) (foo (cdr x)) x))
; (thm (equal (foo x) (car (cons y y)))
; :hints (("Goal" :in-theory (enable (:d foo)))
; ("Goal'" :induct (foo x))))
;
; Formerly:
;
; No induction schemes are suggested by the induction hint. (Note that
; FOO (including its :induction rune) is disabled, so it cannot suggest
; an induction scheme. Consider providing an :in-theory hint that enables
; FOO or (:INDUCTION FOO).) Consequently, the proof attempt has failed.
;
; Now:
;
; No induction schemes are suggested by the induction hint. Consequently,
; the proof attempt has failed.

Also, in support of this change, added useful function ens-from-pspv.

In books/misc, turned books *-bsd.lisp into reloc_stub books, now that
xdoc/top no longer has a GNU license.

[GitHub]

Branch: refs/heads/testing