gcl-devel
[Top][All Lists]
Advanced

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

[Gcl-devel] Re: address@hidden


From: Matt Kaufmann
Subject: [Gcl-devel] Re: address@hidden
Date: 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?

  INFO-DIR-SECTION Math
  START-INFO-DIR-ENTRY
  * acl2: (acl2-doc-emacs.info). Applicative Common Lisp
  END-INFO-DIR-ENTRY

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

==============================

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.

 LICENSE
 Makefile
 TAGS
 all-files.txt
 doc/
 emacs/ [moved to usr/share/emacs/site-lisp/acl2/]
 init.lsp
 installation.html
 new.html
 saved/
 workshops.html

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

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/atl2_2.7-8_i386.deb or
http://people.debian.org/~camm/acl2-doc_2.7-8_all.deb, which seems problematic
to me.

==============================

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
following:

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

All README files
bdd/be/
bdd/bit-vector-reader.lsp
cli-misc/ [This is minor, but why not leave it?]
misc/simplify-defuns.txt
ordinals/copyright
textbook/chap3/solutions.txt
textbook/chap6/solutions.txt
textbook/chap7/
textbook/index.html

==============================

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/]
CLI.sty
README [moved to documentation??]
acl2-formatting.lisp
doinfix
infix.lisp
latex-init.lisp
latex-theory.lisp
makefile
scribe-init.lisp
scribe-theory.lisp
sloop.lisp

==============================

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

==============================

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.

==============================

Thanks --
-- Matt
   Cc: address@hidden
   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
   http://people.debian.org/~camm/atl2_2.7-8_i386.deb. 

   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,
   i.e. _i386.deb. 

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

   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 
obtained
   > ACL2 following Jun Sawada's instructions (sorry for the misguided email 
last
   > night):
   > 
   >   8. Download ACL2 source and patch file from the Debian site. Go to
   > 
   >      http://packages.debian.org/unstable/math/acl2.html
   > 
   >      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, 
which
   > 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 
just
   > let me know how I should think of the organization of acl2_2.7.8_i386.deb, 
and
   > 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
   > http://packages.debian.org/unstable/math/acl2.html:
   > 

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

   > Delete acl2-sources/books/textbook/chap3/programs.cert1
   > 
   > I view acl2-sources/debian/ as yours, not part of ACL2, so I didn't really 
look
   > at it, though I noticed that acl2-sources/debian/acl2 points to ACL2 2.6, 
not
   > 2.7.
   > 
   > 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?
   > 
   > INFO-DIR-SECTION Math
   > START-INFO-DIR-ENTRY
   > * acl2: (acl2-doc-emacs.info). Applicative Common Lisp
   > END-INFO-DIR-ENTRY
   > 
   > 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)?
   > 
   > 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 
low
   > priority.
   > 
   > Thanks --
   > -- Matt
   > 
   > 
   > _______________________________________________
   > Gcl-devel mailing list
   > address@hidden
   > http://mail.gnu.org/mailman/listinfo/gcl-devel
   > 
   > 
   > 

   Many thanks again!  I hope this is not too burdensome!

   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]