saving and restoring your logical state

ACL2 !>:Q
>(make-lib "file")
>(note-lib "file")
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.