introduction to filename conventions in ACL2
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 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

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 the connected book directory is "/home/smith/" (see cbd), then the filename string above also corresponds to the relative filename string "acl2/book1.lisp".