Major Section: BOOKS
The notion of pathname objects from Common Lisp is not supported in
ACL2, nor is the function pathname. However, ACL2 supports file
operations, using conventions for naming files based on those of the
Unix (trademark of AT&T) operating system, so that the character /
is used to terminate directory names. Some file names are ``absolute''
(complete) descriptions of a file or directory; others are
``relative'' to the current working directory or to the connected
book directory (see cbd). We emphasize that even for users of
Windows-based systems or Macintosh computers, ACL2 file names are in
the Unix style. We will call these ACL2 pathnames, often
omitting the ``ACL2.''
Pathnames starting with the directory separator (/) or the tilde
character (~) are absolute pathnames. All other pathnames are relative
pathnames. An exception is in the Microsoft Windows operating system, where
it is illegal for the pathname to start with a tilde character but the drive
may be included, e.g., "c:/home/smith/acl2/book-1.lisp". In fact, the
drive must be included in the portcullis of a book; see portcullis.
Note also that some host Common Lisps will not support pathnames starting
with "~", for example ~smith, though ACL2 will generally support
those starting with "~/" regardless of the host Common Lisp.
Consider the following examples. The filename string
"/home/smith/acl2/book-1.lisp"is an absolute pathname, with top-level directory
"home",
under that the directory "smith" and then the directory
"acl2", and finally, within that directory the file
"book-1.lisp". If the connected book directory is
"/home/smith/" (see cbd), then the filename string above
also corresponds to the relative filename string "acl2/book1.lisp".Finally, we note that (on non-Windows systems) the pathname "~" and
pathnames starting with "~/" are illegal in books being certified.
Otherwise, a subsidiary include-book form would have a different
meaning at certification time than at a later time when the certified book
is included by a different user.
