Major Section: OTHER
Examples: ACL2 !>(rebuild "project.lisp") ACL2 !>(rebuild "project.lisp" t) ACL2 !>(rebuild "project.lisp" t :dir :system) ACL2 !>(rebuild "project.lisp" :all) ACL2 !>(rebuild "project.lisp" :query) ACL2 !>(rebuild "project.lisp" 'lemma-22)
Rebuild allows you to assume all the commands in a given file or
list, supplied in the first argument. Because
rebuild processes an
arbitrary sequence of commands with
t, it is
unsound! However, if each of these commands is in fact admissible,
then processing them with
rebuild will construct the same logical
state that you would be in if you typed each command and waited
through the proofs again. Thus,
rebuild is a way to reconstruct a
state previously obtained by proving your way through the commands.
The second, optional argument to
rebuild is a ``filter''
(see ld-pre-eval-filter) that lets you specify which commands
to process. You may specify
:query, or a new logical name.
:all both mean that you expect the entire file or list to be
:query means that you will be asked about each command
in turn. A new name means that all commands will be processed as
long as the name is new, i.e.,
rebuild will stop processing commands
immediately after executing a command that introduces name.
will also stop if any command causes an error. You may therefore
wish to plant an erroneous form in the file, e.g.,
(mv t nil state),
(see ld-error-triples), to cause
rebuild to stop there. The
(i-am-here) is such a pre-defined form. If you do not specify
rebuild will query you for one.
Inspection of the definition of
rebuild, e.g., via
will reveal that it is just a glorified call to the function
See ld if you find yourself wishing that
rebuild had additional
If you supply the above ``filter'' argument, then you may also supply the
:dir, which is then passed to
ld; see ld.