|
|
|---|
|
|
|
|---|
Book naming conventions assumed by ACL2
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; 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.
We conclude with a remark about a representation of full book names that is
used in certificate files and make-event expansions. When the
system books directory is a prefix of a full book name, ACL2 may choose to
write a full book name as
; full book name: "/Users/smith/acl2/acl2/books/std/portcullis.lisp" ; alternate representation ; (where "/Users/smith/acl2/acl2/books/" is the system books directory): (:SYSTEM . "std/portcullis.lisp")
Conversely, in some contexts ACL2 will convert