Saving-event-data
Save data stored for subsidiary events
Warning: This is a low-level system utility that may change
somewhat over time. For more details, see the ACL2 source code.
General Forms:
(saving-event-data form)
; See Further information below for keyword options for these two:
(runes-diff book-name)
(old-and-new-event-data book-name)
where form is any form that evaluates to an error-triple and
book-name is a file ending with ".lisp". See below for typical
usage.
A common problem is that a book whose certification formerly succeeded now
has a certification failure. In that case, the failure is often caused by a
proof failure; then one may wish for information on what has changed from the
previous, successful proof attempt and the new, failing proof attempt. Here
is a procedure for obtaining such information. After that we discuss some
variations on that procedure.
Finding runes that were used only previously, or only now
Here we discuss a procedure for discovering, given a book BOOK.lisp,
which runes were used in a previous successful proof but not in the new
failed proof attempt, or vice-versa.
The procedure described here requires certain “event-data”
information to have been written by a previous certification of
BOOK.lisp. Such writing of event-data can be accomplished by providing
certify-book the keyword argument :write-event-data t. Writing
of event-data by certify-book can also be accomplished by setting
environment variable ACL2_WRITE_EVENT_DATA to a non-empty value, though
that is overridden if certify-book keyword argument
:write-event-data is explicitly supplied the value, nil. See build::custom-certify-book-commands for discussion about how a
cert-flags comment can set certify-book keyword values when using
the cert.pl utility.
When certify-book writes event-data under either condition above
(keyword argument or environment variable), it writes it to
BOOK@event-data.lsp. That file includes entries of the form (name
. alist), where alist is an event-data alist — see get-event-data — where each entry corresponds to one of the following
event types, possibly generated by a macro or make-event call.
- defthm
- defun
- verify-guards
- thm
One (name . alist) entry is written for each such event, in the order
in which the events were encountered during the proof pass of certification.
Normally name is the name of the event, but it is nil in the case of
a thm event.
Suppose that you have file BOOK@event-data.lsp as discussed above,
that is, from having previously certified BOOK.lisp when writing
event-data. Also suppose that you now have a copy of BOOK.lisp (maybe
the same one, maybe not) for which certification has failed, possibly using a
different ACL2 version than the first, and let EV be the event that
caused the failure; assume that's because of a proof failure. Below are steps
that allow you to see which rules (actually, runes) were used in the
proof attempt for the first event but not the second, or vice-versa. That
information might help you to repair the proof, for example by enabling or
disabling a rule whose enabled status has changed after the successful
certification, or by proving a rule that was in an included book during the
successful certification but has since been deleted.
Step 1. Load the portcullis commands:
(ld "BOOK.port")
Step 2. Execute the following command, which will presumably end
with a failed proof for the event, EV.
(saving-event-data (ld "BOOK.lisp"))
Step 3. See which runes were used in the old proof and not the new,
and vice-versa, respectively:
(runes-diff "BOOK.lisp")
An example is in community-books file
books/demos/event-data/test1.lisp, which has comments that lead through a
variant of the steps above. File test1-input.lsp in that directory
actually carries out that process, resulting in output displayed in log file
test1-log.txt in that directory. Here is the output of a runes-diff
call shown both in that log file and in a comment in file
test1-input.lsp. It shows that a type-prescription rule, named
true-listp-append, was used in the original proof but not the failed
proof (which made the ld call of Step 2 above without first
performing Step 1, which would have introduced that type-prescription rule).
This output also shows that the new (failed) proof attempt used many runes not
used in the previous proof — not surprisingly, since without the rule
true-listp-reverse the prover made a desperate attempt involving
destructor elimination and induction.
((:OLD ((:TYPE-PRESCRIPTION TRUE-LISTP-REVERSE)))
(:NEW ((:DEFINITION ALISTP)
(:DEFINITION ATOM)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART REVERSE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ALISTP))))
A second, analogous set of three files is in that same directory; just
replace "test1" by "test2" in the filenames.
Further information
The runes-diff utility is intended to serve as an example of a class
of such query utilities. It is a macro that expands to a corresponding
function call.
ACL2 !>:trans1 (runes-diff "BOOK.lisp")
(RUNES-DIFF-FN "BOOK.lisp" NIL NIL NIL 'RUNES-DIFF
STATE)
ACL2 !>
Runes-diff-fn is actually quite simple.
Function: runes-diff-fn
(defun runes-diff-fn (book-string name namep dir ctx state)
(er-let*
((old/new (old-and-new-event-data-fn
book-string name namep dir ctx state)))
(let* ((old (car old/new))
(new (cdr old/new))
(old-runes (get-event-data-1 'rules old))
(new-runes (get-event-data-1 'rules new))
(old-diff (set-difference-equal old-runes new-runes))
(new-diff (set-difference-equal new-runes old-runes)))
(value (list (list :old old-diff)
(list :new new-diff))))))
It is simple because the real work is carried out using a more complex
function, old-and-new-event-data-fn. That function returns a pair
(old . new), where old and new are event-data alists for the
failed event (called EV above). Then runes-diff-fn only needs to
pick out the RULES fields and form the set-differences.
The macro old-and-new-event-data provides a convenient interface to
old-and-new-event-data-fn.
ACL2 !>:trans1 (old-and-new-event-data "BOOK.lisp")
(OLD-AND-NEW-EVENT-DATA-FN "BOOK.lisp"
NIL NIL NIL 'OLD-AND-NEW-EVENT-DATA
STATE)
ACL2 !>
Both runes-diff and old-and-new-event-data have keyword arguments
that allow one to choose a specific name for a failed event — the most
recent event with that name, rather than EV — and a directory for
the given filename, which may be a string or a keyword representing a project
directory (see project-dir-alist). The "test2" files mentioned
above have an example in which the name nil is supplied to specify the
thm event most recently preceding the failed event (actually it's the
only one preceding the failed event).
General Forms:
(runes-diff book-string &key name dir)
(old-and-new-event-data book-string &key name dir)
If you want to use these programmatically, call the corresponding
"-FN" versions, where namep is t to represent the case that a
name is provided, else nil.
General Forms:
(runes-diff-fn book-string name namep dir ctx state)
(old-and-new-event-data book-string name namep dir ctx state)
