Using serialization efficiently in books
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)
(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 (though this is
not the default; see book-hash. 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
Then, during include-book, the make-event expansion 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