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 (mv-let (obj state) (serialize-read "my-file") (value `(defconst *my-file* ',obj))))
But this scheme is not particularly efficient.
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-objectis 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
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