[Gcl-devel] one more Debian/ACL2 issue

[Matt Kaufmann]

Camm --

I've thought of another issue pertaining to the Debian ACL2 release.  It is
probably only relevant if the user installs locally rather than under
/usr/share/....  I had the impression that this was allowed, since not all
users would have necessary priveleges to do a "proper" installation, but maybe
I'm wrong in which case I guess this email is mostly irrelevant, except that
it would be important to make this restriction clear.

If I'm right that such local installations are allowed, but only then, please
read on....

The directories under usr/share/acl2-2.7/books/ contain .cert files.  It's a
great concept to distribute those files.  The problem is that they contain
references to absolute path names, and they also contain checksums.  So if you
try to edit the pathnames, you'll probably get a checksum error when you try to
use them.  That may be why I got this error (I did a little tracing that
suggests this possibility, though I only gave a quick look):

  ACL2 !>(include-book 
"/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top")


  ACL2 Error in ( INCLUDE-BOOK 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top"
  ...):  The certificate for the book 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.lisp"
  is ill-formed.  Delete or rename the file 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.cert"
  and recertify 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.lisp".
  Remember that the certification world for 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.lisp"
  is described in the portcullis of 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.cert"
  (see :DOC portcullis) so you might want to look at 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.cert"
  to remind yourself of 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top.lisp"'s
  certification world.


  Summary
  Form:  ( INCLUDE-BOOK 
  "/u/kaufmann/temp/acl2/new/usr/share/acl2-2.7/books/arithmetic/top"
  ...)
  Rules: NIL
  Warnings:  None
  Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

  ******** FAILED ********  See :DOC failure  ******** FAILED ********
  ACL2 !>

The point here is: even though it might work out not to edit those pathnames in
the .cert file, still that would be exploiting a hole we might plug some day,
since we really do expect absolute pathnames to be correct.  Speaking of "some
day", we may implement a mechanism that avoids the need for absolute pathnames
in the .cert file, using environment variables.

But for now, maybe it would be better to avoid distributing .cert files.  In
that case all the Makefile* and .acl2 files will be necessary under books/ in
order for the user to easily recertify all the books (i.e., re-create the .cert
files).  This will also involve re-creating the corresponding .o files, so if
you omit .cert files then it's also probably a good idea to leave out the .o
files.

-- Matt