[Top][All Lists]
[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
- Re: [Gcl-devel] Re: gcl/acl2, (continued)
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12
- Message not available
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2,
Matt Kaufmann <=
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17