Book naming conventions assumed by ACL2
See pathname for background on ACL2 pathnames.
ACL2 defines a ``full book name'' to be an ``absolute filename string,'' which 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")
This behavior is actually more general: it applies to the entire project-dir-alist. If that alist associates keyword
Conversely, in some contexts ACL2 will convert