BOOK-CONTENTS

restrictions on the forms inside books 
Major Section:  BOOKS


Example Book:


; 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))))
The first form in a book must be (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.












































































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. 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.












































































BOOK-NAME

conventions associated with book names 
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, 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 a relative filename string, ACL2 appends the connected book directory on the left and the desired extension on the right.

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".

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. 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.












































































CBD

connected book directory string 
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.) 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 set-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, 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.












































































CERTIFICATE

how a book is known to be admissible and where its defpkgs reside 
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 function certify-book and inspected by include-book. Check 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 certificate.

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-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:

The non-erroneous inclusion of a certified book is consistency preserving provided (a) the objects read by include-book from the certificate were the objects written there by a certify-book and (b) the forms read by include-book from the book itself are the forms read by the corresponding certify-book.

We say that a given execution of 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. 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 books.












































































CERTIFY-BOOK

how to produce a certificate for a book 
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 "my-arith" t)   ;certify from world of existing certificate


General Form:
(certify-book book-name k compile-flg
              :defaxioms-okp t/nil      ; [default t]
              :skip-proofs-okp t/nil    ; [default t]
              )
where 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.

The two keyword arguments, :defaxioms-okp and :skip-proofs-okp, determine how the system handles the inclusion of defaxiom events and skip-proofs events, respectively, in the book. The value t allows such events, but prints a warning message. The value nil causes an error if such an event is found.

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.












































































FULL-BOOK-NAME

book naming conventions assumed by ACL2 
Major Section:  BOOKS

For this discussion we assume that the resident operating system is Unix (trademark of AT&T), but analogous remarks apply to other operating systems supported by ACL2, in particular, the Macintosh operating system where `:' plays roughly the role of `/' in Unix; see pathname.

ACL2 defines a ``full book name'' to be an ``absolute filename string,'' that may be divided into contiguous sections: a ``directory string'', a ``familiar name'' and an ``extension''. See pathname for the definitions of ``absolute,'' ``filename string,'' and other notions pertaining to naming files. Below we exhibit the three sections of one such string: 

"/usr/home/smith/project/arith.lisp"


"/usr/home/smith/project/"           ; directory string
                        "arith"      ; familiar name
                             ".lisp" ; extension
The sections are marked by the rightmost slash and rightmost dot, as shown below. 
"/usr/home/smith/project/arith.lisp"
                        |     |
                        slash dot
                        |     |
"/usr/home/smith/project/"           ; directory string
                        "arith"      ; familiar name
                             ".lisp" ; extension
The directory string includes (and terminates with) the rightmost slash. The extension includes (and starts with) the rightmost dot. The dot must be strictly to the right of the slash so that the familiar name is well-defined and nonempty.

If you are using ACL2 on a system in which file names do not have this form, please contact the authors and we'll see what we can do about generalizing ACL2's conventions.