reset the prehistory

(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) (reset-prehistory permanent-p doc-string)

where permanent-p is t or nil, and doc-string is an optional documentation string not beginning with ``:doc-section ...''. 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 with value nil for permanent-p (the default) is always skipped during certify-book and include-book (indeed, whenever ld-skip-proofsp is t). Otherwise one would find the history numbering reset to 0 just by virtue of including (or certifying) a book -- probably not what was intended.

See ubt-prehistory for how to undo a reset-prehistory command that does not have a permanent-p of t.