File representation using ACL2 project directories
ACL2 supports relocation of book directories so that those books are still treated as certified. See project-dir-alist.
A key data structure to support this feature is the sysfile, which
is a pair of the form
(Remark. The name ``sysfile'' was originally coined to suggest ``system
file'', suggesting the use of keyword
ACL2 rarely generates output that includes sysfiles; they are mostly used in the implementation, for example to denote included books in certificate files. But they are occasionally relevant at the user level; for example see add-include-book-dir.
Finally we discuss the use of sysfiles in certificate files. When
the community-books directory is a prefix of a full-book-name
string, ACL2 may choose to represent that full-book-name as
; full-book-name: "/Users/smith/acl2/acl2/books/std/portcullis.lisp" ; sysfile representation ; (where "/Users/smith/acl2/acl2/books/" is the community-books directory): (:SYSTEM . "std/portcullis.lisp")
This behavior applies to more than the community-books: it applies to the
entire project-dir-alist. If that alist associates keyword