Rebuild
A convenient way to reconstruct your old state
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.
