BOOK-EXAMPLE

how to create, certify, and use a simple book 
Major Section:  BOOKS

Suppose you have developed a sequence of admissible events which you want to turn into a book. We call this ``publishing'' the book. This note explains how to do that.

A key idea of books is that they are ``incremental'' in the sense that when you include a book in a host logical world, the world is incrementally extended by the results established in that book. This is allowed only if every name defined by the incoming book is either new or is already identically defined. See redundant-events. This is exactly the same problem faced by a programmer who wishes to provide a utility to other people: how can he make sure he doesn't create name conflicts? The solution, in Common Lisp, is also the same: use packages. While books and packages have a very tenuous formal connection (every book must start with an in-package), the creation of a book is intimately concerned with the package issue. Having motivated what would otherwise appear as an unnecessary fascination with packages below, we now proceed with a description of how to publish a book.

Just to be concrete, let's suppose you have already gotten ACL2 to accept the following sequence of commands, starting in the ACL2 initial state. 

   (defpkg "ACL2-MY-BOOK"
           (union-eq *common-lisp-symbols-from-main-lisp-package*
                     *acl2-exports*))
   (in-package "ACL2-MY-BOOK")
   (defun app (x y)
     (if (consp x) (cons (car x) (app (cdr x) y)) y))
   (defun rev (x)
     (if (consp x) (app (rev (cdr x)) (list (car x))) nil))
   (defthm rev-app-hack
     (equal (rev (app a (list x))) (cons x (rev a))))
   (defthm rev-rev
     (implies (acl2::true-listp x) (equal (rev (rev x)) x)))
Observe that the first form above defines a package (which imports the symbols defined in CLTL such as if and cons and the symbols used to command ACL2 such as defun and defthm). The second form selects that package as the current one. All subsequent forms are read into that package. The remaining forms are just event forms: defuns and defthms in this case.

Typically you would have created a file with Emacs containing these forms and you will have submitted each of them interactively to ACL2 to confirm that they are all admissible. That interactive verification should start in ACL2's initial world -- although you might, of course, start your sequence of events with some include-books to build a more elaborate world.

The first step towards publishing a book containing the results above is to create a file that starts with the in-package and then contains the rest of the forms. Let's call that file "my-book.lisp". The name is unimportant, except it must end with ".lisp". If there are events that you do not wish to be available to the user of the book -- e.g., lemmas you proved on your way toward proving the main ones -- you may so mark them by enclosing them in local forms. See local. Let us suppose you wish to hide rev-app-hack above. You may also add standard Lisp comments to the file. The final content of "my-book.lisp" might be: 

 ; This book contains my app and rev functions and the theorem
 ; that rev is its own inverse.

   (in-package "ACL2-MY-BOOK")
   (defun app (x y)
     (if (consp x) (cons (car x) (app (cdr x) y)) y))
   (defun rev (x)
     (if (consp x) (app (rev (cdr x)) (list (car x))) nil))

 ; The following hack is not exported.
   (local (defthm rev-app-hack
     (equal (rev (app a (list x))) (cons x (rev a)))))

   (defthm rev-rev
     (implies (acl2::true-listp x) (equal (rev (rev x)) x)))
The file shown above is the book. By the time this note is done you will have seen how to certify that the book is correct, how to compile it, and how to use it in other host worlds. Observe that the defpkg is not in the book. It cannot be: Common Lisp compilers disagree on how to treat new package definitions appearing in files to be compiled.

Since a book is just a source file typed by the user, ACL2 provides a mechanism for checking that the events are all admissible and then marking the file as checked. This is called certification. To certify "my-book.lisp" you should first get into ACL2 with an initial world. Then, define the package needed by the book, by typing the following defpkg to the ACL2 prompt: 

ACL2 !>(defpkg "ACL2-MY-BOOK"
               (union-eq *common-lisp-symbols-from-main-lisp-package*
                         *acl2-exports*))
Then execute the command: 
ACL2 !>(certify-book "my-book" 1 t) ; the `t' is in fact the default
Observe that you do not type the ".lisp" part of the file name. For purposes of books, the book's name is "my-book" and by the time all is said and done, there will be several extensions in addition to the ".lisp" extension associated with it.

The 1 tells certify-book that you acknowledge that there is one command in this ``certification world'' (namely the defpkg). To use the book, any prospective host world must be extended by the addition of whatever commands occurred before certification. It would be a pity to certify a book in a world containing junk because that junk will become the ``portcullis'' guarding entrance to the book. The t above tells certify-book that you wish to compile "my-book.lisp" also (but see compilation for an exception). Certify-book makes many checks but by far the most important and time-consuming one is that it ``proves'' every event in the file.

When certify-book is done it will have created two new files. The first will be called "my-book.cert" and contains the ``certificate'' attesting to the admissibility of the events in "my-book.lisp". The certificate contains the defpkg and any other forms necessary to construct the certification world. It also contains various check sums used to help you keep track of which version of "my-book.lisp" was certified.

The second file that may be created by certify-book is the compiled version of "my-book.lisp" and will have a name that is assigned by the host compiler (e.g., "my-book.o" in GCL, "my-book.fasl" in SBCL). Certify-book will also load this object file. When certify-book is done, you may throw away the logical world it created, for example by executing the command :u.

To use the book later in any ACL2 session, just execute the event (include-book "my-book"). This will do the necessary defpkg, load the non-local events in "my-book.lisp" and then may load the compiled code for the non-local functions defined in that file. Checks are made to ensure that the certificate file exists and describes the version of "my-book.lisp" that is read. The compiled code is loaded if and only if it exists and has a later write date than the source file (but see compilation for an exception).

Since include-book is itself an event, you may put such forms into other books. Thus it is possible for the inclusion of a single book to lead to the inclusion of many others. The check sum information maintained in certificates helps deal with the version control problem of the referenced books. I.e., if this version of "my-book" is used during the certification of "your-book", then the certificate for "your-book" includes the check sum of this version of "my-book". If a later (include-book "your-book") finds a version of "my-book" with a different check sum, an error is signalled. But check sums are not perfect and the insecurity of the host file system prevents ACL2 from guaranteeing the logical soundness of an include-book event, even for a book that appears to have a valid certificate (they can be forged, after all). (See certificate for further discussion.)

This concludes the example of how to create, certify and use a book. If you wish, you could now review the documentation for book-related topics (see books) and browse through them. They'll probably make sense in this context. Alternatively, you could continue the ``guided tour'' through the rest of the documentation of books. See book-name, following the pointer given at the conclusion.