		Search-engine friendly clone of the ACL2 documentation.

Project-dir-alist

Support for moving project directories (also :dir arguments)

This topic describes the project-dir-alist, which supports the relocation of book directories so that their books are still treated as certified. Each such directory is treated as a project, which is represented by a keyword. In particular, the keyword, :SYSTEM, represents the community-books as such a project. The project-dir-alist also provides one way to interpret the :dir keyword argument of include-book and ld.

It is theoretically possible to undermine soundness by using this capability inappropriately (see below for some discussion of appropriate usage). For the utmost security, perform a fresh certification of your entire collection of books without using this capability. See certificate, specifically the discussion there about placing a ``burden'' on the user.

To see the project-dir-alist in your session, evaluate the form (project-dir-alist (w state)).

We start below by introducing the project-dir-alist and explaining how to set it up. Next we describe its effects. We conclude by discussing some details, limitations, and restrictions.

What is the project-dir-alist and how is it established?

The project-dir-alist is an association list that maps keywords to directory names. If we map keyword :K to directory "<dir>", we say that the project name K is associated with project directory "<dir>".

The way to establish the project-dir-alist is to set environment variable ACL2_PROJECTS to the name of a file, which we will call the ``projects file''. The projects file may have lines of the following form, where we write :K to denote an arbitrary keyword and "<dir>" to denote a directory name inside double-quotes.

:K "<dir>"

Such a line associates the project name K with the project directory "dir". Each remaining line in a projects file should either be blank (i.e., contain only whitespace) or else be a comment line, that is, a line for which the first non-whitespace character is a semicolon (;).

The projects file is read when ACL2 starts up. ACL2 creates the project-dir-alist by using each line as above to associate the keyword :K with the directory represented by "<dir>", which may be a relative or absolute pathname. Relative pathnames are interpreted with respect to the directory of the projects file.

If the keyword :SYSTEM is not specified in the projects file, then the project-dir-alist will additionally include a pair that associates :SYSTEM with the community-books directory, which is generally the books/ subdirectory of your ACL2 distribution. That value for :SYSTEM can be overridden either by specifying it explicitly with :SYSTEM in the projects file or by setting environment variable ACL2_SYSTEM_BOOKS to that value — where if both overrides are used, they must not conflict.

The values of the environment variables mentioned above, ACL2_PROJECTS and ACL2_SYSTEM_BOOKS, are pathnames that can be either relative or absolute. A relative pathname is interpreted with respect to the directory in which ACL2 is invoked. The final character need not be ``/''; if it's not, then that character will be added at the end before adding to the project-dir-alist.

The project-dir-alist must have no duplicate keys and no duplicate directory names.

Effects of the project-dir-alist

There are the following two effects of the association of a keyword :K with a directory "<dir>" in the project-dir-alist.

(1) :K specifies a project directory that may be moved.

Consider first the default case, where there is a single association in the project-dir-alist: :SYSTEM is associated with the community-books directory. Suppose that the community books and their certificates are moved to a new directory, "<dir>". Then if you run ACL2 in an environment where the project-dir-alist associates :SYSTEM with "<dir>", the relocated community books will still be treated as certified.

The case of :SYSTEM described above generalizes naturally, as follows. Let S be a set of books certified with a given project-dir-alist, each of which includes only other books in S. (For example, S contains just the community books directory in the special case above.) Also assume that the absolute pathname of every book in S has a prefix among the directories in that project-dir-alist. Then all books in S, along with their certificate files, can be moved and those books will still be considered to be certified in any ACL2 session with a suitable project-dir-alist, as follows. For every keyword :K mapped to directory "<dir>" in the original project-dir-alist (the one at certification time), the new project-dir-alist should map :K to the directory "<dir2>" to which "<dir>" was moved.

(2) :K can be used as a :dir keyword, to reference "<dir>".

The optional :dir keyword argument of include-book and ld can have value :K, in which case the pathname argument is interpreted with respect to "<dir>". This behavior is the same as when :K is bound to "<dir>" using add-include-book-dir or add-include-book-dir!.

Additional details

Prefixes. Suppose :K1 and :K2 are keywords bound in the project-dir-alist to "<dir1>" and "<dir2>", respectively, where "<dir1>" is a prefix of "<dir2>" (hence is stricly shorter, since duplicates are disallowed, as noted above). Then it may be simplest to maintain that property — that the value of :K1 is a prefix of the value of :K2 — when creating a new ACL2_PROJECTS directory to reflect relocation of these directories of books. The actual requirement is that directories under the old value of :K2 need to be moved to the same relative locations under the new value of :K2, and all other directories under the old value of :K1 need to be moved to the same relative locations under the new value of :K1.

Save-exec. By default, an executable created with save-exec will have an unchanged project-dir-alist. However, a new project-dir-alist will be created as described above if environment variable ACL2_PROJECTS is set; also, if environment variable ACL2_SYSTEM_BOOKS is set, then the existing project-dir-alist will be modified to map :SYSTEM to the value of ACL2_SYSTEM_BOOKS.

Additional Limitations and Restrictions

(Already noted above) No duplicates. There must be no duplicate keys or duplicate directory names in the project-dir-alist.

No overlap. No keyword may be bound with add-include-book-dir or add-include-book-dir! that is also bound in the project-dir-alist.

Avoid using absolute pathnames in books. Consider a form that contains an absolute pathname, such as (defconst *c* "/u/home/jones/bk"). If that form is in a book B that is moved, then of course it remain in B after the move. That is certainly fine, unless one expects this pathname to change as B is moved. That said, an absolute pathname that extends a project directory is OK in an include-book form among the portcullis commands for a book, in the following sense: it is replaced in that book's certificate by referencing the project's keyword name to avoid using an absolute pathname.

Subtopics

Sysfile: File representation using ACL2 project directories