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 ld-skip-proofsp 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 t, :all, :query, or a new logical name.
t and :all both mean that you expect the entire file or list to be
processed. :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. Rebuild
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
form (i-am-here) is such a pre-defined form. If you do not specify
a filter, rebuild will query you for one.
Inspection of the definition of rebuild, e.g., via :pc rebuild-fn,
will reveal that it is just a glorified call to the function ld.
See ld if you find yourself wishing that rebuild had additional
functionality.
If you supply the above ``filter'' argument, then you may also supply the
keyword argument :dir, which is then passed to ld; see ld.
