CERTIFY-BOOK

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" t)   ;certify from world of existing certificate

General Form:
(certify-book book-name k compile-flg
              :defaxioms-okp t/nil      ; [default nil]
              :skip-proofs-okp t/nil    ; [default nil]
              )

The two keyword arguments, :defaxioms-okp and :skip-proofs-okp, determine how the system handles the inclusion of defaxiom events and skip-proofs events, respectively, in the book. The value t allows such events, but prints a warning message. The value nil is the default, and causes an error if such an event is found.

For a general discussion of books, see books. Certify-book is akin to what we have historically called a ``proveall'': all the forms in the book are ``proved'' to guarantee their admissibility. More precisely, 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 local incompatibilities (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 :ubt :here afterwards.

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 defpkgs 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 (e.g., with :ubt 1 or just starting a new version of ACL2), defpkg the desired packages, and then invoke certify-book.

The k argument to certify-book must be either a nonnegative integer or else one of the symbols t or ? in the ACL2 package. If k is an integer, then it must be the number of commands that have been executed to create the world in which certify-book was called. One way to obtain this number is by doing :pbt 1 to see all the commands back to the first one. The last command number printed in the :pbt display is the appropriate k. This number is just the maximum command number, :max -- see command-descriptor -- but unless :max is 0, certify-book requires that you actually input the number as a way of reminding you to inspect the world before calling certify-book.

If k is t it means that certify-book should use the same world used in the last certification of this book. K may be t only if you call certify-book in the initial ACL2 world (:max = 0) and there is a certificate on file for the book being certified. (Of course, the certificate is probably invalid.) In this case, certify-book reads the old certificate to obtain the portcullis commands and executes them to recreate the certification world.

Finally, k may be ?, in which case there is no check made on the cerfification world. That is, if k is ? 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 defpkgs 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.

When 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.lbin" or "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.

When certify-book is directed not to produce a compiled file, it will delete any existing compiled file for the book, so as not to mislead 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 that certify-book form was executed. See acl2-defaults-table.

This completes the tour through the documentation of books.