Reset-prehistory
Reset the prehistory
Examples:
(reset-prehistory) ; restart command numbering at 0
(reset-prehistory nil) ; same as above
(reset-prehistory t) ; as above except also disable ubt-prehistory
General Forms:
(reset-prehistory)
(reset-prehistory permanent-p)
where permanent-p is t or nil. After execution of this
command, ACL2 will change the numbering provided by its history
utilities so that this reset-prehistory command (or the top-level
compound command containing it, which for example might be an include-book) is assigned the number 0. The only way to undo this command is
with command ubt-prehistory. However, even that is disallowed if
permanent-p is t.
Note that the second argument of certify-book, which specifies the
number of commands in the certification world (i.e., since ground-zero), is
not sensitive to reset-prehistory; rather, it expects the number of
commands since ground-zero. To see such commands, :pbt
:start.
A reset-prehistory event for which parameter permanent-p has the
default value of nil is always skipped when any of the following
conditions holds: during certify-book; during include-book or
the second pass of encapsulate (indeed, whenever ld special
'ld-skip-proofsp has value 'include-book); or when
state global 'skip-reset-prehistory has a non-nil value. Thus,
we avoid resetting the history numbering to 0 when including or certifying a
book, since that would probably not be what was intended.
See ubt-prehistory for how to undo a reset-prehistory command
that does not have a permanent-p of t. See disable-ubt for a
variant of (reset-prehistory t) that does not change command numbering
and is used by the break-rewrite utility. Like disable-ubt,
reset-prehistory is never redundant.
