		Search-engine friendly clone of the ACL2 documentation.

Events

Dump-events

Dump events to a file.

Examples

(include-book "misc/dump-events" :dir :system)
(dump-events "xxx")        ; dump all user events to file xxx
(dump-events "xxx" :x-2)   ; dump the last two events to file xxx
(dump-events "xxx" 2 :x-1) ; dump all events from after command 2
                           ; up through the next-to-last command

General Form

(dump-events dumpfile
             &optional earlier-command-desc later-command-desc)

where the form of the optional command descriptors is explained elsewhere; see command-descriptor. All events strictly after the first command descriptor up through the second, which by default are 0 and :x (thus indicating that all user events should be dumped to the dumpfile), are written to the indicated dumpfile. In addition, an extra form is written to the top of the dumpfile: (in-package "ACL2"). This makes it convenient to use the dumpfile as a source file for ACL2 in a later session.

Each event that was originally executed underneath local will be placed inside local in the dumpfile.

The dumpfile will be overwritten if it already exists.