|
|
|---|
|
|
|
|---|
Some possible ways to work around certify-book failures
This topic provides some ideas for how to deal with certify-book failures. Ideally, this topic will continue to grow over time.
Stack overflows may show up as follows.
*********************************************** ************ ABORTING from raw Lisp *********** ********** (see :DOC raw-lisp-error) ********** Error: Stack overflow on value stack. ***********************************************
When this occurs during book certification, it could be during an attempt to handle large objects, in particular by the serialize writer or by a memoized version of the check for ``bad'' objects. These two potential causes can be remedied by first evaluating the following forms, respectively.
(set-serialize-character-system nil state) (set-bad-lisp-consp-memoize nil)
If the large object is in an event in the book under certification, then you may need to avoid printing it, as follows.
(set-inhibit-output-lst '(proof-tree event))
Other failures of