Serialize-read
Read a serialized ACL2 object from a file
General form:
(serialize-read filename
[:hons-mode {:always, :never, :smart}] ; :smart by default
[:verbosep {t, nil}]) ; nil by default
-->
(mv obj state)
In the logic this is an oracle read.
Under the hood, we try to read and return a serialized object from a file
that was presumably created by serialize-write. On success we return
the contents of the file. Any failures (e.g., file not found, bad file
contents, etc.) will result in a hard Lisp error.
The filename should be a string that gives the path to the file.
The hons-mode controls how whether to use hons or cons
to restore the object. The default mode is :smart, which means that
conses that were normed at the time of the file's creation should be
restored with hons. But you can override this and insist that hons
is to :always or :never be used, instead.
Why would you use :never? If your object previously had a lot of
honses, but you no longer have any need for them to be normed, then using
:never may sometimes be a lot faster since it can avoid hons calls.
On the other hand, if you are going to hons-copy some part of the
file's contents, then it is likely faster to use :smart or :always
instead of first creating normal conses and then copying them to build
honses.
The :verbosep flag just controls whether to print some low-level
details related to timing and memory usage as the file is being read.
