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.












































































KEEP

how we know if include-book read the correct files 
Major Section:  BOOKS

The certificate (see certificate for general information) of a certified file is divided into two parts, a portcullis and a keep. These names come from castle lore. The keep is the strongest and usually tallest tower of a castle from which the entire courtyard can be surveyed by the defenders. The keep of a book is a list of file names and check sums used after the book has been included, to determine if the files read were (up to check sum) those certified.

Once the portcullis is open, include-book can enter the book and read the event forms therein. The non-local event forms are in fact executed, extending the host theory. That may read in other books. When that has been finished, the keep of the certificate is inspected. The keep is a list of the book names which are included (heritarily through all subbooks) in the certified book (including the certified book itself) together with the check sums of the objects in those books at the time of certification. We compare the check sums of the books just included to the check sums of the books stored in the keep. If differences are found then we know that the book or one of its subbooks has been changed since certification.

See include-book to continue the guided tour through books.












































































PATHNAME

introduction to filename conventions in ACL2 
Major Section:  BOOKS

Although the notion of pathname objects from Common Lisp is not supported in ACL2, nor is the function pathname, nevertheless ACL2 adopts conventions for naming files that are not so different from Common Lisp's conventions, using strings that we'll call ``filename strings'' and (for ACL2 books) certain lists that we'll call ``structured pathnames.'' Some of these strings and lists correspond to ``absolute,'' i.e. complete, descriptions of a file or directory; others are ``relative'' to the current working directory or to the connected book directory (see cbd). The reason we support structured pathnames is to allow books to be transferred between machines running different operating systems (see book-name).

Consider by way of introduction the following examples in the Unix (trademark of AT&T) operating system. The filename string 

"/home/smith/acl2/book-1.lisp"
corresponds to the structured pathname 
(:absolute "home" "smith" "acl2" "book-1.lisp")
and, relative to the connected book directory "/home/smith/" (see cbd), corresponds to the relative filename string 
"acl2/book1.lisp"
and to the relative structured pathname 
(:relative "acl2" "book-1.lisp")
The rest of the discussion focuses on filename strings vs. structured pathnames, with attention to directories vs. files and to absolute vs. relative pathnames.

Filename strings. One way to specify a file in ACL2 is by way of a nonempty string. The form of this string must conform to the requirements of the resident operating system. Thus in the Unix environment, slash (/) is the ``directory separator'': a filename such as "/home/smith/acl2/book-1.lisp" may be read as ``Inside the directory "/home", then inside the directory "smith", then inside the directory "acl2", consider the file "book-1.lisp".'' On the Macintosh, the directory separator is colon (:). Such strings represent a directory when they terminate with the directory separator, and a file otherwise. The directory separator may be obtained as: 

(directory-separator (@ operating-system) 'top).
Filename strings may be referred to either as absolute pathnames, which are complete descriptions of the location of a file or directory, or as relative pathnames, which give the location of a file or directory relative to a given (implicit) directory. In Unix, filename strings starting with the directory separator (/) are absolute pathnames, such as the example in the preceding paragraph. All other filename strings are relative pathnames.

For example, the string 

"examples/my-book"
is a relative pathname. If the implicit directory (which for books is the connected book directory; see cbd) is "/home/smith/", then the corresponding absolute pathname is the filename string obtained by concatenating the implicit directory with the relative pathname, 
"/home/smith/examples/my-book"
On the Macintosh the convention is exactly reversed: a string represents an absolute pathname exactly when its first character is not the directory separator (:). Thus, the absolute pathname corresponding to the one displayed just above is 
"home:smith:examples:my-book"
which may be derived from the relative pathname 
":examples:my-book"
and implicit directory 
"home:smith:"
Notice that on the Macintosh, when we concatenate an implicit directory string to a relative pathname string, we must drop the excess colon, since a colon terminates the implicit directory string and also starts the relative pathname.

Structured pathnames. In ACL2, books may be named with filename strings or with structured pathnames, which we now describe. (Note that structured pathnames are only used in the realm of books: for example, although :set-cbd accepts structured pathnames, ld currently only accepts filename strings.) A structured pathname is a list beginning with one of the keywords :absolute or :relative and then continuing with strings, except that :back may appear any number of times between :relative and the first string in the list. Each of the strings represents a subdirectory, except that the last may represent a file. For example, the filename string (in Unix) "/home/smith/acl2/book-1.lisp" represents the same file as does the following structured pathname. 

(:absolute "home" "smith" "acl2" "book-1.lisp")
This is an absolute structured pathname, because it begins with the keyword :absolute. The other type of structured pathname is the relative structured pathname, which begins with the keyword :relative. For example, the following structured pathname corresponds to the relative filename string (in Unix) "examples/my-book": 
(:relative "examples" "my-book")
As mentioned above, relative structured pathnames may also contain any number of occurrences of the keyword :back after the (initial element) :relative and before the first string. This keyword represents the notion of going up one level in the file system (just like ".." in Unix). For example, suppose that the connected book directory (see cbd) can be represented by the following structured pathname. 
(:absolute "home" "smith" "acl2" "examples")
Then the structured pathname 
(:relative :back :back "numbers" "book-2.lisp")
represents the same file as does the following absolute structured pathname. 
(:absolute "home" "smith" "numbers" "book-2.lisp")
Here, the first :back may be thought of as ``cancelling'' the subdirectory "examples" and the second :back may be thought of as ``cancelling'' its parent "acl2", after which we are to continue as specified by the given relative structured pathname.

There is no distinction between files and directories for structured pathnames, but the intention is clear from context. For example, the argument to :set-cbd is a directory, while the argument to include-book is a file (but without the ".lisp" extension (see book-name).

Finally, we note that our notion of structured pathname corresponds to a similar notion of structured directory described in the second edition of Guy Steele's book ``Common Lisp the Language.'' The main difference is that we allow the trivial structured pathname (:relative), but Steele does not.












































































PORTCULLIS

the gate guarding the entrance to a certified book 
Major Section:  BOOKS

The certificate (see certificate for general information) of a certified file is divided into two parts, a portcullis and a keep. These names come from castle lore. The portcullis of a castle is an iron grate that slides up through the ceiling of the tunnel-like entrance. The portcullis of a book insures that include-book does not start to read the book until the appropriate context has been created.

Technically, the portcullis consists of the version number of the certifying ACL2, a list of commands used to create the ``certification world'' and an alist specifying the check sums of all the books included in that world. The portcullis is constructed automatically by certify-book from the world in which certify-book is called, but that world must have certain properties described below. After listing the properties we discuss the issues more leisurely.

Each command in the portcullis must be either a defpkg form or an embedded event form (see embedded-event-form). In addition, we exclude include-book events unless the name of the included book is an absolute filename (see pathname). For example, under Unix (trademark of AT&T) any string supplied to include-book in the portcullis must begin with a slash (/). Since the portcullis commands are recovered automatically by certify-book, this restriction on the form of portcullis commands naturally becomes a restriction on the world in which certify-book may be called. We explain the exclusion after discussing the general issues.

Consider a book to be certified. The book is a file containing event forms. Suppose the file contains references to such symbols as my-pkg::fn and acl2-arith::cancel, but that the book itself does not create the packages. Then a hard Lisp error would be caused merely by the attempt to read the expressions in the book. The corresponding defpkgs cannot be written into the book itself because the book must be compilable and Common Lisp compilers differ on the rules concerning the inline definition of new packages. The only safe course is to make all defpkgs occur outside of compiled files.

More generally, when a book is certified it is certified within some logical world. That ``certification world'' contains not only the necessary defpkgs but also, perhaps, function and constant definitions and maybe even references to other books. When certify-book creates the certificate for a file it recovers from the certification world the commands used to create that world from the initial ACL2 world. Those commands become part of the portcullis for the certified book. In addition, certify-book records in the portcullis the check sums (see check-sum) of all the books included in the certification world.

Include-book presumes that it is impossible even to read the contents of a certified book unless the portcullis can be ``raised.'' To raise the portcullis we must be able to execute (possibly redundantly, but certainly without error), all of the commands in the portcullis and then verify that the books thus included were identical to those used to build the certification world (up to check sum). This raising of the portcullis must be done delicately since defpkgs are present: we cannot even read a command in the portcullis until we have successfully executed the previous ones, since packages are being defined.

Clearly, a book is most useful if it is certified in the most elementary extension possible of the initial logic. If, for example, your certification world happens to contain a defpkg for "MY-PKG" and the function foo, then those definitions become part of the portcullis for the book. Every time the book is included, those names will be defined and will have to be either new or redundant (see redundant-events). But if those names were not necessary to the certification of the book, their presence would unnecessarily restrict the utility of the book.

Recall that we disallow include-book events from the portcullis unless the included book's name is an absolute filename (See pathname). Thus, for example, under the Unix operating system it is impossible to certify a book if the certification world was created with 

ACL2 !>(include-book "arith")
The problem here is that the file actually read on behalf of such an include-book depends upon the then current setting of the connected book directory (see cbd). That setting could be changed before the certification occurs. If we were to copy (include-book "arith") into the portcullis of the book being certified, there is no assurance that the "arith" book included would come from the correct directory. However, by requiring that the include-books in the certification world give book names that begin with slash we effectively require you to specify the full file name of each book involved in creating your certification world. Observe that the execution of 
(include-book "/usr/local/src/acl2/library/arith")
or equivalently (using structured pathnames; see pathname) 
(include-book
  (:absolute "usr" "local" "src" "acl2" "library" "arith"))
does not depend on the current book directory. On the other hand, this requirement -- effectively that absolute file names be used in the certification world -- means that a book that requires another book in its certification world will be rendered uncertified if the required book is removed to another directory. If possible, any include-book command required for a book ought to be placed in the book itself and not in the certification world. The only time this cannot be done is if the required book is necessary to some defpkg required by your book. Of course, this is just the same advice we have been giving: keep the certification world as elementary as possible.

See keep to continue the guided tour of books.












































































SET-CBD

to set the connected book directory 
Major Section:  BOOKS


Example Forms:
ACL2 !>:set-cbd "/usr/home/smith/"
ACL2 !>:set-cbd (:absolute "usr" "home" "smith")
ACL2 !>:set-cbd (:relative :back "smith")
See cbd for a description of the connected book directory. 

General Form:
(set-cbd str)
where str is either a nonempty string that represents the absolute pathname for a directory, or a structured pathname that represents a directory (see pathname). This command sets the connected book directory (see cbd) to the string representing the indicated directory. Thus, this command may determine which files are processed by include-book and certify-book commands typed at the top-level. However, the cbd is also set by those two book processing commands; thus, the setting of the cbd is irrelevant to include-book commands in other books.

Note that if a structured pathname is used for :set-cbd, then it may be absolute or relative. (See pathname for relevant definitions.) However, if a string is used for :set-cbd, it must represent an absolute pathname. We do not support syntax for relative pathnames for use with :set-cbd that is peculiar to particular operating systems, such as ".." in Unix (trademark of AT&T), because we want to be sure to be able to correctly identify the resulting absolute pathname of the :cbd.












































































UNCERTIFIED-BOOKS

invalid certificates and uncertified books 
Major Section:  BOOKS

Include-book has a special provision for dealing with uncertified books: If the file has no certificate or an invalid certificate (i.e., one whose check sums describe files other than the ones actually read), a warning is printed and the book is otherwise processed as though it were certified and had an open portcullis. (For details see books, see certificate, and see portcullis.)

This can be handy, but it can have disastrous consequences.

The provision allowing uncertified books to be included can have disastrous consequences, ranging from hard lisp errors, to damaged memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the logic inconsistent. For example, one of its non-local events might be (defthm t-is-nil (equal t nil)). It is also possible for the inclusion of an uncertified book to cause hard errors or breaks into raw Common Lisp. For example, if the file has been edited since it was certified, it may contain too many open parentheses, causing Lisp to read past ``end of file.'' Similarly, it might contain non-ACL2 objects such as 3.1415 or ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a suitable extension of ACL2's initial world), its uncertified inclusion might cause Lisp errors or inconsistencies! For example, it might mention packages that do not exist in the host world. The portcullis of a certified book insures that the correct defpkgs have been admitted, but if a book is read without actually raising its portcullis, symbols in the file, e.g., acl2-arithmetic::fn, could cause ``unknown package'' errors in Common Lisp. Perhaps the most subtle disaster occurs if the host world does have a defpkg for each package used in the book but the host defpkg imports different symbols than those required by the portcullis. In this case, it is possible that formulas which were theorems in the certified book are non-theorems in the host world, but those formulas can be read without error and will then be quietly assumed.

In short, if you include an uncertified book, all bets are off regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors don't occur, the chances are that deductions after the inclusion of an uncertified book are probably justified in the (possibly inconsistent) logical extension obtained by assuming the admissibility and validity of the definitions and conjectures in the book.