[acl2/acl2] 7056f0: Fixed bugs (one is probably soundness) in properly...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 7056f01c7b2bbe9c377946c5a4edc2572271956e
https://github.com/acl2/acl2/commit/7056f01c7b2bbe9c377946c5a4edc2572271956e
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2017-08-16 (Wed, 16 Aug 2017)

Changed paths:
M acl2-init.lisp
M axioms.lisp
M books/misc/check-acl2-exports.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Fixed bugs (one is probably soundness) in properly recognizing supporting defabsstobj events. Added get-enforce-redundancy. Increase sbcl dynamic space size.

Quoting :doc note-7-5:

The check for the requisite theorems supporting a [defabsstobj] event
included a case where the check was too weak, and it also could
cause an unexpected assertion. The first of these could probably
cause unsoundness. Thanks to Sol Swords for finding these issues
and providing fixes.

New function get-enforce-redundancy queries the [world] on whether
redundancy is being enforced. Thanks to Eric Smith for requesting
this feature.

The probably-soundness bug was in source function obviously-equiv-terms.

When saving an SBCL-based ACL2 executable, --dynamic-space-size is now
32000, formerly 24000. Quoting a new comment in the ACL2 sources:

; On August 16, 2017 we found that 24,000 was insufficient to build
; books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.cert, so we
; increased to 32,000. (Note: this was based on the x86isa books as of a few
; days earlier. Even if the increase to 32,000 was not necessary, it seems a
; good idea to accommodate even the previous version.)

[GitHub]

Branch: refs/heads/testing