Pathname
Introduction to filename conventions in ACL2
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
for how relative pathnames are elaborated to absolute pathnames. 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.
