REBUILD

a convenient way to reconstruct your old state 
Major Section:  OTHER


Examples:
ACL2 !>(rebuild "project.lisp")
ACL2 !>(rebuild "project.lisp" t)
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.