gcl-devel
[Top][All Lists]
Advanced

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

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


From: Matt Kaufmann
Subject: Re: [Gcl-devel] Re: gcl/acl2
Date: Sun, 17 Nov 2002 12:48:30 -0600 (CST)

Hi --

As usual, comments/replies are interspersed.

   To: Matt Kaufmann <address@hidden>
   Cc: address@hidden, address@hidden, address@hidden,
      address@hidden
   From: Camm Maguire <address@hidden>
   Date: 17 Nov 2002 13:13:58 -0500

   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?

Yes, that's the idea.  J and I need to think through the details, though.

   > 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. 

Thanks.  Perhaps it would be useful to add a comment about
'dpkg --fsys-tarfile foo.deb | tar xf -
to HOWTO-UNPACK-DEBS, for those who do not want to be root (and, mention that
you have to be root to do the normal installation).  But maybe Debian users
know that stuff.

   > 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.

Thanks for the discussion.  Perhaps the reason these issues haven't yet arisen
much (as far as I know) is that we have a relatively small collection of ACL2
users:  About 120 addresses on the acl2 mailing list, but probably at most 40
active users (perhaps a rather smaller number who use ACL2 on a regular
basis).  So if/when the ACL2 community grows, the investment of time you are
making now may pay off even more than in the near term.  If ACL2 is to become a
Debian package (as it is now becoming, thanks to you), I'm glad someone as
knowledgeable as you is taking on the task!

Thanks --
-- Matt

   Take care,

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




reply via email to

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