|
|
|---|
|
|
|
|---|
Avoid some special serialize writing, including for
This function can be used to turn off (or on) the serialize-write capability, which is on by default, for writing certain files during book certification, including certificate files. To use this function during a session:
; Disable the use of serialize-write by book certification: (set-serialize-character-system nil state) ; Re-enable the use of serialize-write by book certification: (set-serialize-character-system #\Z state)
To use this capability when certifying community-books, you can use a suitable ACL2-customization file, for example:
cd books ; \ make basic \ ACL2_CUSTOMIZATION=`pwd`/../acl2-customization-files/no-serialize.lisp
Alternatively, you can put the following form directly into the book:
(make-event (pprogn (set-serialize-character-system nil state) (value '(value-triple nil))))
To control the use of serialize for writes controlled by the user rather than by the system, see with-serialize-character.