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
consand the symbols used to command ACL2 such as
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:
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
then contains the rest of the forms. Let's call that file
"my-book.lisp". The name is unimportant, except it must end
".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
; 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
defpkgis 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
"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 defaultObserve 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.
certify-book that you acknowledge that there is
one command in this ``certification world'' (namely the
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
"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.
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
"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
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).
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
"my-book" is used during the certification of
"your-book", then the certificate for
the check sum of this version of
"my-book". If a later
(include-book "your-book") finds a version of
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
event, even for a book that appears to have a valid certificate
(they can be forged, after all). (See certificate for further
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.