[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: address@hidden
[Gcl-devel] Re: address@hidden
Tue, 11 Nov 2003 12:43:42 -0600
Hi, Camm --
Thank you for your emails. I'm much clearer now on what's going on. I've
obtained http://people.debian.org/~camm/atl2_2.7-8_i386.deb and
http://people.debian.org/~camm/acl2-doc_2.7-8_all.deb, and looked through them
(after using the suggested ar and tar commands). Below are some issues.
I think most of these issues stem from the re-organization of files in the
Debian binary and doc distributions from our original organization. The cost
of that re-organization is the time spent dealing with these issues, and I
don't know how that balances against advantages of doing so. Given that there
are probably relatively few Debian/ACL2 users, it might be worth considering
leaving some file locations unchanged even if that's not totally the "Debian
way". I realize that this whole "debianizing" thing is probably kind of odd
for ACL2, for example since "book" .lisp files serve as source, data,
and documentation. Thanks for your efforts.
First of all, the easy part. Among the list I sent you before, here are the
only issues that seem to remain.
[Minor] File acl2-sources/books/Makefile has three extra lines starting with #
above the .PHONY target that don't seem to do anything.
You added the following near the top of
acl2-sources/doc/EMACS/acl2-doc-emacs.info, just below the two "Written by"
lines. Should we add this when generating that file?
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
I also had mentioned the following issue, but I'm guessing that it's part of
the whole emacsen story, which I know nothing about (and don't need to know
anything about) -- if so, then please ignore.
In acl2-sources/interface/emacs/acl2-interface.el, you changed
(load "acl2-interface-functions.el") to
(load "acl2-interface-functions"). By loading the .el file, aren't we less
sensitive to emacs changes? Is there any advantage to loading the .elc file
(which I presume is why you made the change)?
Now I'll turn to the new stuff.
I am trusting that etc/emacs/site-start.d/50acl2.el works OK. A very quick
glance suggests that it could well be derived from corresponding ACL2 emacs
The directory usr/share/acl2-2.7/ corresponds to what we usually call
acl2-sources/. I notice that you have included the new proof-checker-b.lisp,
which is fine, although some sort of banner or other modification would be good
when starting up the ACL2 executable (as already discussed). But there are
files missing here that are in acl2-sources/. Some of these may be in the
documentation distribution, and the .html files probably aren't needed. But
I'm not used to thinking about what is needed and what isn't, since we have
been content with our existing distribution methodology for so long that I
haven't thought about such questions.
emacs/ [moved to usr/share/emacs/site-lisp/acl2/]
For example, TAGS can be handy for perusing ACL2 source files (which, as you
know, provide a sort of documentation). For another example, saved/ is needed
if anyone ever wants to re-build ACL2, but the Makefile is missing anyhow --
perhaps your answer is that this is a binary release, so it's not suitable for
I guess the whole binary idea is that they fetch ACL2 once and for all until a
new release. I think that's OK. But currently, I can someone a little patch
to try and it's no big deal for them to edit a source file, type "make", and
see what happens. That happens only rarely, so this isn't a big deal, but
perhaps it's a reason to go ahead and include init.lsp, Makefile, and saved/.
LICENSE does not appear anywhere in
http://people.debian.org/~camm/acl2-doc_2.7-8_all.deb, which seems problematic
The "not suitable for rebuilding" comment above leads me to another issue.
Users may decide to modify distributed books for their own purposes -- not
terribly likely, but certainly an option to them currently. However, this does
not seem to be such a viable option for users of the binary distribution. For
one thing, the .o files are now links to files in usr/lib/acl2-2.7/books, so if
they are re-created.... well, maybe that's not a problem. But consider the
In usr/share/acl2-2.7/books/, although every Makefile is present (I think),
lots of Makefile support is missing. In particular, the .acl2 files are
missing, all certify.lsp files are missing (although ./certify-numbers.lisp is
present), and ./Makefile-generic and ./Makefile-subdirs are missing. Other
things missing under usr/share/acl2-2.7/books/ include the following, which
also seem to be missing from the documentation distribution, except for the
All README files
cli-misc/ [This is minor, but why not leave it?]
A number of files are missing from usr/share/acl2-2.7/interface/, listed
below. I haven't thought about this stuff in years, and I doubt anyone is
using it, so I don't want to put any time into "rationalizing" this -- but on
the other hand I'd like to keep it around just in case someone wants to use it
and finds that it actually does work.
emacs [moved to usr/share/emacs/site-lisp/acl2/]
README [moved to documentation??]
I believe that usr/share/emacs/site-lisp/acl2/ contains everything that was
formerly in emacs/ and interface/emacs/, except doc-notes.txt. That file may
well be obsolete, but I'm not sure, so for simplicity I'd like to keep it
The file usr/share/man/man1/acl2.1 contains the following text. But it
doesn't mention that Postscript and on-line format are also available.
Perhaps J and I need to advertise that more clearly.
This manual page was written for the Debian GNU/Linux distribution
because the original program does not have a manual page. Instead, it
has documentation in the GNU Info format as well as in html format.
From: Camm Maguire <address@hidden>
Date: 10 Nov 2003 21:16:31 -0500
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
Hi Matt! My apologies for the confusion!
Debian package versions follow the 'upstream' software version after a
dash '-'. In the distribution now is 2.7-7. This is now many months
old, and suffers from the ia64 stability problems, in addition to a
number if issues you've raised for me in earlier email. (one of which
is the use of directory names involving acl2-2.6 :-)). All files from
packages.debian.org refer to this version.
The new version I'd like to upload, perhaps after a little
modification, is the one at
Debian *source* packages come in three files, and .orig.tar.gz (which
is identical with your own tarball release, or should be), Debian
specific patches to this source (i.e acl2_2.7-8.diff.gz), and a
description file (i.e. acl2_2.7-8.dsc). These files are unpacked and
built on a variety of architectures (11 as of this moment !), and
compiled into binary packages, installable on the user's system
without additional reference to the source package. These are the
.deb files, each of which carry an architecture specific prefix,
On *any* linux system, one can unpack and inspect a .deb as follows:
1) ar x .....deb
2) tar zxf data.tar.gz
One then has a local tree of all the files that would be installed by
the package. It is therefore a good idea to do this in an empty
Matt Kaufmann <address@hidden> writes:
> P.S. Regarding my comment:
> >> This is embarrassing, but I'm quite confused.
> OK, I'm a little clearer now that it's the next morning, I see that I
> ACL2 following Jun Sawada's instructions (sorry for the misguided email
> 8. Download ACL2 source and patch file from the Debian site. Go to
> and download acl2_2.7.orig.tar.gz and acl2_2.7-7.diff.gz.
> I have comments comparing acl2_2.7.orig.tar.gz and the released ACL2 2.7,
> are included below. But I suspect that you want comments on
> http://www.debian.org/people/~camm/acl2_2.7.8_i386.deb, which is quite
> different from the above, for example because of the missing Makefile. So
> let me know how I should think of the organization of acl2_2.7.8_i386.deb,
> I'll send further comments.
Please let me know if the above is any clearer. I can't remember
exactly right now, but it seems likely the main Makefile is only
required for compiling acl2, and is not therefore included in the
final binary package .deb file. Note that I do include acl2 source
files, as these are used by end-users of acl2 as well.
> Comments on acl2_2.7.orig.tar.gz downloaded from
I'll keep these comments in case they are still relevant to the new
package, but I believe many of them are fixed in the proposed 2.7-8
> Delete acl2-sources/books/textbook/chap3/programs.cert1
> I view acl2-sources/debian/ as yours, not part of ACL2, so I didn't really
> at it, though I noticed that acl2-sources/debian/acl2 points to ACL2 2.6,
> File acl2-sources/books/Makefile has three extra lines starting with #
> the .PHONY target that don't seem to do anything.
> You added the following near the top of
> acl2-sources/doc/EMACS/acl2-doc-emacs.info, just below the two "Written by"
> lines. Should we add this when generating that file?
> INFO-DIR-SECTION Math
> * acl2: (acl2-doc-emacs.info). Applicative Common Lisp
> In acl2-sources/interface/emacs/acl2-interface.el, you changed
> (load "acl2-interface-functions.el") to
> (load "acl2-interface-functions"). By loading the .el file, aren't we less
> sensitive to emacs changes? Is there any advantage to loading the .elc
> (which I presume is why you made the change)?
> Everything else looks good; thank you for the improvements! By the way, I
> don't know if anyone uses acl2-sources/interface/infix/; I consider it a
> Thanks --
> -- Matt
> Gcl-devel mailing list
Many thanks again! I hope this is not too burdensome!
Camm Maguire address@hidden
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
|[Prev in Thread]
||[Next in Thread]|
- [Gcl-devel] Re: address@hidden,
Matt Kaufmann <=