Re: P.S. to address@hidden: Re: [Gcl-devel] Re: ACL2 Version 2.7 release]

[Matt Kaufmann]

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.

Comments on acl2_2.7.orig.tar.gz downloaded from
http://packages.debian.org/unstable/math/acl2.html:

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