SERIALIZE-READ

read a serialized ACL2 object from a file
Major Section:  SERIALIZE

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.