Serialize
Routines for saving ACL2 objects to files, and later restoring them
We thank Jared Davis for contributing the ``serialization''
routines for saving ACL2 objects in files for later loading.
We implement some routines for writing arbitrary ACL2 objects to files, and
for loading those files later. We usually call these ".sao" files, which
stands for (S)erialized (A)CL2 (O)bject.
Our serialization scheme uses a compact, binary format that preserves
structure sharing in the original object. We optimize for read
performance.
Subtopics
- With-serialize-character
- Control output mode for print-object$
- Unsound-read
- A faster alternative to serialize-read, which is unsound in
general, but may be fine in many common cases.
- Serialize-read
- Read a serialized ACL2 object from a file
- Serialize-in-books
- Using serialization efficiently in books
- Print-compressed
- Wrapper for print-object$ that ensures serialize
compression is enabled (if supported).
- Print-legibly
- Wrapper for print-object$ that ensures serialize
compression is disabled.
- Serialize-write
- Write an ACL2 object into a file
- Set-serialize-character-system
- Avoid some special serialize writing, including for .cert
files
- Serialize-alternatives
- Historic alternatives to the serialize routines.
