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.
