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.