Re: [Gcl-devel] Re: gcl/acl2

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

> Hi --
> 
> Comments/replies are interspersed.
> 
>    The approach I've just tried is to basically ship the acl2 source tree
>    as is, with certs, into /usr/share/acl2-2.6, and then to push the
>    binaries into /usr/lib/acl2-2.6 and link them to the
>    /usr/share/acl2-2.6 directory.  (include-book ...) works on the
>    precompiled precertified books without warning.  It would seem that as
>    (include-book ) will take a fixed path, a user could simply create
>    another books directory in their home, no?  That's the way I've left
>    it at present -- ordinary users cannot write into
>    /usr/share/acl2-2.6/books. 
> 
> That will often be OK.  But there are times where it is handy to use relative
> pathnames.  For example, if I create a book "foo.lisp" and I want to include
> the top-level arithmetic book, then you're correct that I could use a full
> pathname, e.g., (include-book "/usr/share/acl2-2.6/books/arithmetic/top").
> However, if I can put foo.lisp in ..../books/my-books/, say, then I could
> instead use (include-book "../arithmetic/top").  We encourage users to use
> relative pathnames when they submit books for ACL2 workshops -- in fact I 
> think
> we tell them exactly where the book will wind up (e.g., in
> books/workshops/2002/user-name/support/).  That way, when they ship us their
> contributions, we do not have to edit pathnames.  However, as we discussed
> earlier, someone can always copy books/ to their own space (using "cp -r", or
> perhaps a script).
> 
> The above discussion could be viewed as a deficiency of ACL2.  It has come up
> previously that it would be nice to have a mechanism within ACL2 for 
> specifying
> the main books/ directory.  There are potential subtle logical issues here
> [I'll elaborate if you're interested], but I think it is possible and a good
> idea.  I've put this "main books/ directory" issue on the list of things to
> consider for ACL2 Version 2.8.
> 

I think you may be referring to the connected-book-path variable.  I
looked at it briefly, but it appears to be write protected, so I did
not pursue.  What would be ideal from a package point of view would be
to have system book path which could be set to a different directory
from the build path, perhaps write protected after installation, and a
user book path that would be freely writable and effectively appended
onto the system book path.  I agree that it would be great to support
relative pathnames -- this scenario would allow them, right?

> By the way, I can imagine someone wanting to download ACL2 to a computer at
> work and try it out, without getting sysadmins involved (hence, without root
> priveleges).  Of course, in that case they can just download ACL2 and build it
> the old-fashioned way.
> 

On can also take any .deb, and do 'dpkg --fsys-tarfile foo.deb | tar
xf -' to unpack the tree as a user wherever she has write
permissions.  Or follow the HOWTO-UNPACK-DEBS, and just tar zxf
data.tar.gz.  The path to saved_acl2 would have to be modified in
usr/bin/acl2. 

> I'm interested in the advantages of having ACL2 as a Debian package.  I can
> imagine that one motivation is ease of installation.  Perhaps another is that
> it is generally a good thing for software packages to follow a common
> installation paradigm.  Are there others?
> 

There are quite a few that I can think of, though not all may be
particularly important to every user.  First and foremost is the ease
of administration, as opposed to installation.  Dependency management
(e.g. libraries), smooth upgrades, ensuring synchronization of
certification results with the binaries that produced them, etc.  Then
of course there is also the savings on a multi-user system of
relieving multiple parties from having their own trees, together with
the perpetual uncertainty -- 'Did I change that file in this tree?
What exactly is in here?  I wonder if Joe has compiled this feature in
his tree?', etc. that inevitably comes with user development directly
on the source tree.  Furthermore, each user, and indeed no user, has
to deal with the build dependencies, i.e. configuring and building the
right gcl, etc.  Building and running the lengthy tests once for all
Debian users saves considerable time.  Synchronizing builds across
several architectures shakes out bugs and leads to a more robust
system on any architecture.   Lastly, one can integrate the software
with various system services, the system wide info and html
documentation tools, menus for desktop use, etc.

Take care,

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah