Major Section: MISCELLANEOUS
Examples: ACL2 !>:Q >(make-lib "file") ... >(note-lib "file") >(LP) ACL2 !>
To save the current ACL2 logical world to a file, exit ACL2 with :q
and invoke (make-lib "file") in Common Lisp. This creates a file
"file.lib" and a file "file.lisp". The latter will be compiled.
It generally takes half an hour to save an ACL2 logical world and
creates a 20Mb file. All things considered it is probably better to
just save your core image.
To restore such a saved ACL2 world, invoke (note-lib "file") from
Common Lisp, and then enter ACL2 with (lp). We do not save the io
system, the stacks, or the global table, hence bindings of your
globals will not be restored.
This save/restore mechanism is a temporary expedient. We know of
faster mechanisms, mechanisms that consume less disk space, and
mechanisms that provide more functionality. We don't know of good
compromises between these various desirable features.