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 (/) are absolute
pathnames. All other pathnames are relative pathnames. An
exception is in the Microsoft Windows operating system, where 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.
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".
