		Search-engine friendly clone of the ACL2 documentation.

Sysfile

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 (:kwd . "relpath"). Here, :kwd is a key of the project-dir-alist, bound to some absolute pathname "D/" of a directory, and "relpath" is a string that denotes a pathname relative to directory "D/". Thus, the sysfile (:kwd . "relpath") represents the same pathname as "D/relpath".

(Remark. The name ``sysfile'' was originally coined to suggest ``system file'', suggesting the use of keyword :SYSTEM to indicate a file residing in the community-books. It now extends to (:kwd . "relpath") even for :kwd values other than :SYSTEM. But ``sysfile'' is a convenient name, and it still seems reasonable since ``system file'' can suggest a file of the filesystem.)

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 (:system . "relpath"), where "relpath" is the result of removing the community-books directory from the front of the full-book-name. Here is an example.

; 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 :K with absolute directory name "<dir>", then a full-book-name with prefix "<dir>", say, "<dir>/relpath", is written to a certificate file as (:K . "relpath"). This capability supports relocating book directories; see project-dir-alist for a more complete discussion.