Serialize-in-books
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)
(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 (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
certificate files.
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
unsound-read.
