[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] one more Debian/ACL2 issue

From: Matt Kaufmann
Subject: [Gcl-devel] one more Debian/ACL2 issue
Date: Tue, 11 Nov 2003 21:16:52 -0600

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 

  ACL2 Error in ( INCLUDE-BOOK 
  ...):  The certificate for the book 
  is ill-formed.  Delete or rename the file 
  and recertify 
  Remember that the certification world for 
  is described in the portcullis of 
  (see :DOC portcullis) so you might want to look at 
  to remind yourself of 
  certification world.

  Form:  ( INCLUDE-BOOK 
  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

-- Matt

reply via email to

[Prev in Thread] Current Thread [Next in Thread]