SERIALIZE-IN-BOOKS

Major Section:  SERIALIZE

Our serialize scheme was developed in order to allow very large ACL2 objects to be loaded into books. Ordinarily this is carried out using serialize-read within a make-event, e.g.,

  (make-event (mv-let (obj state)
                      (serialize-read "my-file")
                      (value `(defconst *my-file* ',obj))))

But this scheme is not particularly efficient.

During certify-book, the actual call of serialize-read is carried out, and this is typically pretty fast. But then a number of possibly inefficient things occur.

- The ACL2 function bad-lisp-object is run on the resulting object. This is memoized for efficiency, but may still take considerable time when the file is very large.

- The checksum of the resulting object is computed. This is also memoized, but as before may still take some time.

- The object that was just read is then written into book.cert, essentially with serialize-write. This can take some time, and results in large certifiate files.

Then, during include-book, the make-event expansion of is loaded. This is now basically just a serialize-read.

The moral of the story is that using serialize will only help your certify-book time, and it only impacts a portion of the overall time.

To avoid this overhead, we have developed an UNSOUND alternative to serialize-read, which is available only by loading an additional book. So, if the above scheme is not performing well for you, you may wish to see the community book serialize/unsound-read.