Support for moving project directories (also
This topic describes the
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
We start below by introducing the
The way to establish the
Such a line associates the project name
The projects file is read when ACL2 starts up. ACL2 creates the
If the keyword
The values of the environment variables mentioned above,
There are the following two effects of the association of a keyword
Consider first the default case, where there is a single association in the
project-dir-alist: :SYSTEMis 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-alistassociates :SYSTEMwith "<dir>", the relocated community books will still be treated as certified.
The case of
:SYSTEMdescribed above generalizes naturally, as follows. Let Sbe a set of books certified with a given project-dir-alist, each of which includes only other books in S. (For example, Scontains just the community books directory in the special case above.) Also assume that the absolute pathname of every book in Shas 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 :Kmapped to directory "<dir>"in the original project-dir-alist(the one at certification time), the new project-dir-alistshould map :Kto the directory "<dir2>"to which "<dir>"was moved.
:dirkeyword 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 :Kis bound to "<dir>"using add-include-book-dir or add-include-book-dir!.
:K1and :K2are keywords bound in the project-dir-alistto "<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 :K1is a prefix of the value of :K2— when creating a new ACL2_PROJECTSdirectory to reflect relocation of these directories of books. The actual requirement is that directories under the old value of :K2need to be moved to the same relative locations under the new value of :K2, and all other directories under the old value of :K1need 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-alistwill be created as described above if environment variable ACL2_PROJECTSis set; also, if environment variable ACL2_SYSTEM_BOOKSis set, then the existing project-dir-alistwill be modified to map :SYSTEMto the value of ACL2_SYSTEM_BOOKS.
(Already noted above) No duplicates. There must be no duplicate keys or duplicate directory names in the
No overlap. No keyword may be bound with add-include-book-dir or add-include-book-dir! that is also bound in the
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 Bthat is moved, then of course it remain in Bafter the move. That is certainly fine, unless one expects this pathname to change as Bis 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.