SERIALIZE

routines for saving ACL2 objects to files, and later restoring them

Major Section:  ACL2 Documentation

This documentation topic relates to an experimental extension of ACL2 that supports hons, memoization, and fast alists. See hons-and-memoization. Thanks to 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.

Some Related Topics

SERIALIZE-ALTERNATIVES -- alternatives to the serialize routines
SERIALIZE-IN-BOOKS -- using serialization efficiently in books
SERIALIZE-READ -- read a serialized ACL2 object from a file
SERIALIZE-WRITE -- write an ACL2 object into a file
SET-SERIALIZE-CHARACTER -- See with-serialize-character.
WITH-SERIALIZE-CHARACTER -- control output mode for print-object$

SERIALIZE

Some Related Topics

SERIALIZE-ALTERNATIVES -- alternatives to the serialize routines

SERIALIZE-IN-BOOKS -- using serialization efficiently in books

SERIALIZE-READ -- read a serialized ACL2 object from a file

SERIALIZE-WRITE -- write an ACL2 object into a file

SET-SERIALIZE-CHARACTER -- See with-serialize-character.

WITH-SERIALIZE-CHARACTER -- control output mode for print-object$

WITH-SERIALIZE-CHARACTER -- control output mode for `print-object$`