restrictions on the forms inside books
Parent topic: BOOKS Home
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.
(in-package "MY-PKG")
(include-book "weird-list-primitives")
(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))))
(in-package "pkg") where
"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., defuns, 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.
Because in-package is not an embedded event form, the only
in-package in a book is the initial one. Because defpkg is
not an embedded event form, a book can never contain a defpkg
form. Because include-book is an embedded event form, books may
contain references to other books. This makes books structured
objects.
When the forms in a book are read from the file, they are read with
current-package set to the package named in the in-package
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
with (in-package "ACL2-X") and then contains the form
(defun fn (x)
(acl2::list 'car x))
then defun, fn, x, and car are 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::defun would be the same symbol as
acl2::defun if the "ACL2-X" package imported acl2::defun.
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.
How does include-book know the definitions of the packages used in a
book, since 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.
how to create, certify, and use a simple book
Parent topic: BOOKS Home
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.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)))
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 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.
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. 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 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 AKCL, "my-book.lbin"
or "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
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 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.
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.
conventions associated with book names
Parent topic: BOOKS Home
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,
include-book and certify-book temporarily reset the connected
book directory to be the directory of the book being processed.
This allows include-book forms 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 certify-book
(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.
For example, include-book uses the ".lisp", ".cert" and
possibly the ".o" or ".lbin" extensions of the book name.
Book names are elaborated into full file names by include-book
and 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
ACL2 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
directory is "/usr/home/smith/" then the book name
"project/task-1/arith" is a book name that will be elaborated
to
"/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.
The ".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.
connected book directory string
Parent topic: BOOKS Home
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
cbd
is always a string, even though :set-cbd accepts structured
directories.) When include-book is 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-book temporarily
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 ``cbd'') is
used by 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 cbd is
"/usr/home/smith/" then the elaboration of the book-name
"project/task-1/arith" (to the ".lisp" extension) is
"/usr/home/smith/project/task-1/arith.lisp". That
full-book-name is what include-book opens to read the
source text for the book.
The 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 cbd is
"/usr/home/smith/" then during the processing of events by
(include-book "project/task-1/arith")the
cbd will 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-book event 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, include-book
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
cbd begin 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 cbd "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.
how a book is known to be admissible and where its defpkgs reside
Parent topic: BOOKS Home
A book, say "arith", is said to have a ``certificate'' if there
is a file named "arith.cert". Certificates are created by the
function certify-book and inspected by include-book.
Certificates contain two parts: a portcullis and a keep.
The portcullis must be raised before the book can be entered.
After a book has been entered, the keep is used to verify that
the entrants were properly identified. Because the file system is
insecure it is possible for the inclusion of a book to cause
inconsistency even though the book carries an impeccable
certificate.
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-local
events of the book are independent of the local ones
(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
host world.
Security:
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 ofThe 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 acertify-bookand (b) the forms read byinclude-bookfrom the book itself are the forms read by the correspondingcertify-book.
include-book is ``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-book are the ones
checked by certify-book. When an uncertified include-book
occurs, 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.
As noted above, certificates are divided into two parts, a portcullis and a keep. See portcullis to continue the guided tour through books.
how to produce a certificate for a book
Parent topic: BOOKS Home
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 certificatewhereGeneral Form: (certify-book book-name k compile-flg)
book-name is a book name (see book-name), k is
either t or an integer used to indicate your approval of the
``certification world,'' and compile-flg indicates whether you
wish to compile the (functions in the) book. Compile-flg
defaults to t, meaning to compile. The second argument k is
actually optional as well; it defaults to 0.
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 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
(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 the symbol t. 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.
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.