Major Section: BOOKS
Example Book:The first form in a book must be
; This book defines my app function and the theorem that it is ; associative. One irrelevant help lemma is proved first but ; it is local and so not seen by include-book. I depend on the ; inferior book "weird-list-primitives" from which I get ; definitions of hd and tl.
(defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y))
(local (defthm help-lemma (implies (true-listp x) (equal (app x nil) x))))
(defthm app-is-associative (equal (app (app a b) c) (app a (app b c))))
"pkg"is some package name known to ACL2 whenever the book is certified. The rest of the forms in a book are embedded event forms, i.e.,
defthms, etc., some of which may be marked
local. See embedded-event-form. The usual Common Lisp commenting conventions are provided. Note that since a book consists of embedded event forms, we can talk about the ``local'' and ``non-local'' events of a book.
in-package is not an embedded event form, the only
in-package in a book is the initial one. Because
not an embedded event form, a book can never contain a
include-book is an embedded event form, books may
contain references to other books. This makes books structured
When the forms in a book are read from the file, they are read with
current-package set to the package named in the
form at the top of the file. The effect of this is that all symbols
are interned in that package, except those whose packages are given
explicitly with the ``::'' notation. For example, if a book begins
(in-package "ACL2-X") and then contains the form
(defun fn (x) (acl2::list 'car x))then
carare all interned in the
"ACL2-X"package. I.e., it is as though the following form were read instead:
(acl2-x::defun acl2-x::fn (acl2-x::x) (acl2::list 'acl2-x::car acl2-x::x)).Of course,
acl2-x::defunwould be the same symbol as
If each book has its own unique package name and all the names
defined within the book are in that package, then name clashes
between books are completely avoided. This permits the construction
of useful logical worlds by the successive inclusion of many books.
Although it is often too much trouble to manage multiple packages,
their judicious use is a way to minimize name clashes. Often, a
better way is to use
local; see local.
include-book know the definitions of the packages used in a
defpkgs cannot be among the forms? More generally,
how do we know that the forms in a book will be admissible in the
host logical world of an
include-book? See certificate for
answers to these questions.
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.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
(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)))
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
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 created by
certify-book is the compiled version
"my-book.lisp" and will have a name that is assigned by the
host compiler (e.g.,
"my-book.o" in AKCL,
"my-book.sbin" in Lucid).
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
then load the compiled code for the non-local functions defined in
that file. Checks are made to insure 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.
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.
Major Section: BOOKS
Examples: "list-processing" "/usr/home/smith/my-arith"Book names are strings and lists that can be elaborated into file names. We elaborate book names by concatenating the ``connected book directory'' (see cbd) string on the left and some ``extension,'' such as
".lisp", on the right. However, the connected book directory is not added if the book name itself already represents an absolute file name. Furthermore,
certify-booktemporarily reset the connected book directory to be the directory of the book being processed. This allows
include-bookforms to use file names without explicit mention of the enclosing book's directory. This in turn allows books (together with those that they include, using
include-book) to be moved between directories while maintaining their certification and utility. (One does need to be careful about using absolute filenames (see pathname) when of certifying books in worlds that have already included other books; see portcullis.)
You may wish to read elsewhere for details of ACL2 file name
conventions (see pathname), for a discussion of the filename
that is the result of the elaboration described here
(see full-book-name), and for details of the concept of the
connected book directory (see cbd). For details of how
include-book (see include-book) and
(see certify-book) use these concepts, see below.
Often a book name is simply the familiar name of the file.
(See full-book-name for discussion of the notions of
``directory string,'' ``familiar name,'' and ``extension''. These
concepts are not on the guided tour through books and you
should read them separately.) However, it is permitted for book
names to include a directory or part of a directory name. Book
names never include the extension, since ACL2 must routinely tack
several different extensions onto the name during
include-book uses the
".lbin" extensions of the book name.
Book names are elaborated into full file names by
certify-book. This elaboration is sensitive to the
``connected book directory.'' The connected book directory is an
absolute filename string (see pathname) that is part of the
state. (You may wish to see cbd and to
see set-cbd -- note that these are not on the guided tour).
If a book name is an absolute filename string, ACL2 elaborates it simply by appending the desired extension to the right. If a book name is an absolute structured pathname, then it is first converted to an absolute pathname string (see pathname) and ACL2 elaborates the result.
If a book name is a relative filename string, ACL2 appends the
connected book directory on the left (eliminating the excess colon
:) character in the case of the Macintosh file system) and the
desired extension on the right. If a book name is a relative
structured pathname, it is first converted to a relative pathname
string and then ACL2 elaborates the result.
Note that it is possible that the book name includes some partial
specification of the directory. For example, if the connected book
"/usr/home/smith/" then the book name
"project/task-1/arith" is a book name that will be elaborated
"/usr/home/smith/project/task-1/arith.lisp".Also, the structured book name
(:relative "project" "task-1" "arith")will be elaborated the same way. However, the directory separator (which is the character slash (
/) in Unix (trademark of AT&T) and colon (
:) on the Macintosh) may not appear in the final component of a structured book name; for example,
(:relative "project" "task-1/arith")is illegal.
Observe that while the events in this
"arith" book are being
processed the connected book directory will temporarily be set to
"/usr/home/smith/project/task-1/".Thus, if the book requires other books, e.g.,
(include-book "naturals")then it is not necessary to specify the directory on which they reside provided that directory is the same as the superior book.
This inheritance of the connected book directory and its use to
elaborate the names of inferior books makes it possible to move
books and their inferiors to new directories, provided they maintain
the same relative relationship. Moreover, if all arguments to
include-book commands are structured directories, then it is even
possible to move with ease whole collections of books to different
filesystems that use a different operating system than the one under
which the original certification was performed.
".cert" extension of a book, if it exists, is presumed to
contain the most recent certificate for the book.
See certificate (or, if you are on the guided tour, wait until
the tour gets there).
See book-contents to continue the guided tour.
Major Section: BOOKS
Example: ACL2 !>:cbd "/usr/home/smith/"The connected book directory is a nonempty string that specifies a directory as an absolute pathname. (See pathname for a discussion of file naming conventions. Note however that the
cbdis always a string, even though
set-cbdaccepts structured directories.) When
include-bookis given a relative book name it elaborates it into a full book name, essentially by appending the connected book directory string to the left and
".lisp"to the right. (For details, see book-name and also see full-book-name.) Furthermore,
include-booktemporarily sets the connected book directory to the directory string of the resulting full book name so that references to inferior books in the same directory may omit the directory. See cbd for how to set the connected book directory string.
General Form: (cbd)This is a macro that expands into a term involving the single free variable
state. It returns the connected book directory string.
The connected book directory (henceforth called the ``
include-book to elaborate the supplied book name into a
full book name (see full-book-name). For example, in the Unix
(trademark of AT&T) operating system, if the
"/usr/home/smith/" then the elaboration of the book-name
"project/task-1/arith" (to the
".lisp" extension) is
full-book-name is what include-book opens to read the
source text for the book.
cbd may be changed using
set-cbd (see set-cbd).
Furthermore, during the processing of the events in a book,
include-book sets the
cbd to be the directory string of the
full-book-name of the book. Thus, if the
"/usr/home/smith/" then during the processing of events by
cbdwill be set to
"/usr/home/smith/project/task-1/". Note that if
"arith"recursively includes a subbook, say
"naturals", that resides on the same directory, the
include-bookevent for it may omit the specification of that directory. For example,
"arith"might contain the event
(include-book "naturals").In general, suppose we have a superior book and several inferior books which are included by events in the superior book. Any inferior book residing on the same directory as the superior book may be referenced in the superior without specification of the directory.
We call this a ``relative'' as opposed to ``absolute'' naming. The use of relative naming is preferred because it permits books (and their accompanying inferiors) to be moved between directories while maintaining their certificates and utility. Certified books that reference inferiors by absolute file names are unusable (and rendered uncertified) if the inferiors are moved to new directories.
Technical Note and a Challenge to Users:
After elaborating the book name to a full book name,
opens a channel to the file to process the events in it. In some
host Common Lisps, the actual file opened depends upon a notion of
``connected directory'' similar to our connected book directory.
Our intention in always elaborating book names into absolute
filename strings (see pathname for terminology) is to
circumvent the sensitivity to the connected directory. But we may
have insufficient control over this since the ultimate file naming
conventions are determined by the host operating system rather than
Common Lisp (though, we do check that the operating system
``appears'' to be one that we ``know'' about). Here is a question,
which we'll pose assuming that we have an operating system that
calls itself ``Unix.'' Suppose we have a file name, filename, that
begins with a slash, e.g.,
"/usr/home/smith/...". Consider two
successive invocations of CLTL's
(open filename :direction :input)separated only by a change to the operating system's notion of connected directory. Must these two invocations produce streams to the same file? A candidate string might be something like
"/usr/home/smith/*/usr/local/src/foo.lisp"which includes some operating system-specific special character to mean ``here insert the connected directory'' or, more generally, ``here make the name dependent on some non-ACL2 aspect of the host's state.'' If such ``tricky'' name strings beginning with a slash exist, then we have failed to isolate ACL2 adequately from the operating system's file naming conventions. Once upon a time, ACL2 did not insist that the
cbdbegin with a slash and that allowed the string
"foo.lisp"to be tricky because if one were connected to
"/usr/home/smith/"then with the empty
"foo.lisp"is a full book name that names the same file as
"/usr/home/smith/foo.lisp". If the actual file one reads is determined by the operating system's state then it is possible for ACL2 to have two distinct ``full book names'' for the same file, the ``real'' name and the ``tricky'' name. This can cause ACL2 to include the same book twice, not recognizing the second one as redundant.
Major Section: BOOKS
A book, say
"arith", is said to have a ``certificate'' if there
is a file named
"arith.cert". Certificates are created by the
certify-book and inspected by
sums are used to help insure that certificates are legitimate and
that the corresponding book has not been modified since
certification. But because the file system is insecure and check
sums are not perfect it is possible for the inclusion of a book to
cause inconsistency even though the book carries an impeccable
The certificate includes the version number of the certifying ACL2. A book is considered uncertified if it is included in an ACL2 with a different version number.
The presence of a ``valid'' certificate file for a book attests to
two things: all of the events of the book are admissible in a
certain extension of the initial ACL2 logic, and the non-
events of the book are independent of the
(see local-incompatibility). In addition, the certificate
contains the commands used to construct the world in which
certification occurred. Among those commands, of course, are the
defpkgs defining the packages used in the book. When a book is
included into a host world, that world is first extended
by the commands listed in the certificate for the book. Unless that
causes an error due to name conflicts, the extension insures that
all the packages used by the book are identically defined in the
Because the host file system is insecure, there is no way ACL2 can guarantee that the current contents of a book is the same as it was when its certificate was written. That is, between the time a book is certified and the time it is used, it may be modified. Furthermore, certificates can be counterfeited. Check sums (see check-sum) are used to help detect such problems. But check sums provide imperfect security: two different files can have the same check sum.
Therefore, from the strictly logical point of view, one must consider even the inclusion of certified books as placing a burden on the user:
We say that a given execution of
The non-erroneous inclusion of a certified book is consistency preserving provided (a) the objects read by
include-bookfrom the certificate were the objects written there by a
certify-bookand (b) the forms read by
include-bookfrom the book itself are the forms read by the corresponding
include-bookis ``certified'' if a certificate file for the book is present and well-formed and the check sum information contained within it supports the conclusion that the events read by the
include-bookare the ones checked by
certify-book. When an uncertified
include-bookoccurs, warnings are printed or errors are caused. But even if no warning is printed, you must accept burdens (a) and (b) if you use books. These burdens are easier to live with if you protect your books so that other users cannot write to them, you abstain from running concurrent ACL2 jobs, and you abstain from counterfeiting certificates. But even on a single user uniprocessor, you can shoot yourself in the foot by using the ACL2 io primitives to fabricate an inconsistent book and the corresponding certificate.
Note that part (a) of the burden described above implies, in
particular, that there are no guarantees when a certificate is
copied. When books are renamed (as by copying them), it is
recommended that their certificates be removed and the books be
recertified. The expectation is that recertification will go
through without a hitch if relative pathnames are used, though if
the books are moved to a file system with a different underlying
operating system, things will go more easily if structured pathnames
are used as arguments to
include-book. See pathname, which
is not on the guided tour.
Certificate essentially contain two parts, a portcullis and a
keep. See portcullis to continue the guided tour through
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 (:relative "my-arith") 0 nil) ;as above (certify-book "my-arith" t) ;certify from world of existing certificatewhere
General Form: (certify-book book-name k compile-flg)
book-nameis a book name (see book-name),
tor an integer used to indicate your approval of the ``certification world,'' and
compile-flgindicates whether you wish to compile the (functions in the) book.
t, meaning to compile. The second argument
kis actually optional as well; it defaults to
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 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
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 insure 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 the symbol
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
display is the appropriate
k. This number is just the maximum
max -- see command-descriptor -- but unless
certify-book requires that you actually input
the number as a way of reminding you to inspect the world
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
certify-book reads the old certificate to obtain
the portcullis commands and executes them to recreate the
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.