introduction to filename conventions in ACL2 Major Section:
BOOKS   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   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 bo