How to create, certify, and use a simple book
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
; 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
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
When certify-book is done it will have created two new files. The
first will be called
The second file that may be created by certify-book is the compiled
To use the book later in any ACL2 session, just execute the event
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 book-hash information
maintained in certificates helps deal with the version control problem
of the referenced books. I.e., if this version of
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.