Major Section: BOOKS
Examples: (certify-book "my-arith" 3) ;certify in a world with 3 commands (certify-book "my-arith") ;certify in a world with 0 commands (certify-book "my-arith" 0 nil) ;as above, but do not compile (certify-book "my-arith" 0 t) ;as above, but compile (certify-book "my-arith" 0 :all) ;as above, but compile exececutable ; counterparts too (certify-book "my-arith" t) ;certify from world of old certificatewhere
General Form: (certify-book book-name k compile-flg :defaxioms-okp t/nil ; [default nil] :skip-proofs-okp t/nil ; [default nil] :save-expansion :save/t/nil ; [default nil] :ttags ttags ; [default nil] )
book-nameis a book name (see book-name),
tor an integer used to indicate your approval of the ``certification world.''
Compile-flgindicates whether you wish to compile the (functions in the) book.
t, meaning to compile;
nilmeans do not compile.
The second argument
k is optional as well; it defaults to
Two keyword arguments,
how the system handles the inclusion of
defaxiom events and
skip-proofs events, respectively, in the book. The value
such events, but prints a warning message. The value
nil is the default,
and causes an error if such an event is found.
The keyword argument
:ttags may normally be omitted. A few constructs,
used for example if you are building your own system based on ACL2, may
require it. See defttag for an explanation of this argument.
To advanced users only: in the rare case that you are willing to add to
compilation time in return for compiling the executable counterparts of
functions defined in the book, you may supply a value of
compile-flg. This setting is useful for compiling a book whose functions
are called during macroexpansion, because evaluation during macroexpansion is
done in a ``safe mode'' that avoids calling raw Lisp functions
The keyword argument
:save-expansion controls whether or not a so-called
``book expansion'' file is written, obtained by appending the string
"@expansion.lsp" to the end of the book name. See make-event for
discussion of the book expansion; in a nutshell,
generate forms that replace them in the book expansion. Book expansion is
:save-expansion are both
Otherwise, the values of
:save-expansion cause the
book expansion to be created only when a
make-event form occurs in a
book (i.e., only if there is some expansion), or if at least one executable
counterpart is to be compiled (see preceding paragraph). If the book
expansion is created, then it is deleted after compilation if
nil. Finally, if
:save, then the book expansion file is created in all cases, and is not
For a general discussion of books, see books.
is akin to what we have historically called a ``proveall'': all the
forms in the book are ``proved'' to guarantee their admissibility.
certify-book (1) reads the forms in the book,
confirming that the appropriate packages are defined in the
certification world; (2) does the full admissibility checks on
each form (proving termination of recursive functions, proving
theorems, etc.), checking as it goes that each form is an embedded
event form (see embedded-event-form); (3) rolls the world
back to the initial certification world and does an
include-book of the book to check for
(see local-incompatibility); (4) writes a certificate
recording not only that the book was certified but also recording
the commands necessary to recreate the certification world (so
the appropriate packages can be defined when the book is included in
other worlds) and the check sums of all the books involved
(see certificate); (5) compiles the book if so directed (and
then loads the object file in that case). The result of executing a
certify-book command is the creation of a single new event, which
is actually an
include-book event. If you don't want its
included events in your present world, simply execute
Certify-book requires that the default defun-mode
(see default-defun-mode) be
logic when certification is
attempted. If the mode is not
logic, an error is signalled.
An error will occur if
certify-book has to deal with any
uncertified book other than the one on which it was called. For
example, if the book being certified includes another book, that
subbook must already have been certified.
Certification occurs in some logical world, called the
``certification world.'' That world must contain the
needed to read and execute the forms in the book. The commands
necessary to recreate that world from the ACL2 initial
world will be copied into the certificate created for the
book. Those commands will be re-executed whenever the book is
included, to ensure that the appropriate packages (and all other
names used in the certification world) are correctly defined. The
certified book will be more often usable if the certification
world is kept to a minimal extension of the ACL2 initial
world. Thus, before you call
certify-book for the first
time on a book, you should get into the initial ACL2 world
:ubt 1 or just starting a new version of ACL2),
defpkg the desired packages, and then invoke
k argument to
certify-book must be either a nonnegative integer
or else one of the symbols
? in the
ACL2 package. If
is an integer, then it must be the number of commands that have been
executed after the initial ACL2 world to create the world in which
certify-book was called. One way to obtain this number is by doing
:pbt :start to see all the commands back to the first one.
t it means that
certify-book should use the same
world used in the last certification of this book.
K may be
only if you call
certify-book in the initial ACL2 world and there is
a certificate on file for the book being certified. (Of course, the
certificate is probably invalid.) In this case,
the old certificate to obtain the portcullis commands and
executes them to recreate the certification world.
k may be
?, in which case there is no check made on the
certification world. That is, if
? then no action related to
the preceding two paragraphs is performed, which can be a nice convenience
but at the cost of eliminating a potentially valuable check that the
certification world may be as expected.
If you have a certified book that has remained unchanged for some
time you are unlikely even to remember the appropriate
for it. If you begin to change the book, don't throw away its
certificate file just because it has become invalid! It is an
important historical document until the book is re-certified.
certify-book is directed to produce a compiled file, it
calls the Common Lisp function
compile-file on the original source
file. This creates a compiled file with an extension known to ACL2,
e.g., if the book is named
"my-book" then the source file is
"my-book.lisp" and the compiled file under AKCL will be
"my-book.o" while under Lucid it will be
"my-book.sbin". The compiled file is then loaded. When
include-book is used later on
"my-book" it will
automatically load the compiled file, provided the compiled file has
a later write date than the source file. The only effect of such
compilation and loading is that the functions defined in the
book execute faster. See guard for a discussion of the issues.
certify-book is directed not to produce a compiled file, it
will delete any existing compiled file for the book, so as not to
include-book into loading the now outdated compiled file.
After execution of a
certify-book form, the value of
acl2-defaults-table is restored to what it was immediately before
certify-book form was executed.
This completes the tour through the documentation of books.