		Search-engine friendly clone of the ACL2 documentation.

Serialize-write

Write an ACL2 object into a file

General form:

(serialize-write filename obj
                 [:verbosep  {t, nil}])    ; nil by default
 -->
state

In the logic this carries out an oracle read.

Under the hood, we try to save obj into the file indicated by filename, which must be a string. The object can later be recovered with serialize-read. We just return state, and any failures (e.g., file not openable) will result in a hard Lisp error.

Writing objects to disk is generally slower than reading them back in since some analysis is required to convert an object into our serialized object format.

The verbosep flag just says whether to print some low-level details related to timing and memory usage as the file is being written.