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 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

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.