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

[Matt Kaufmann]

Hi --

I just downloaded the following to my Redhat Linux 7.3 home machine; some
comments are below.

http://incoming.debian.org/acl2_2.6-14_i386.deb
http://incoming.debian.org/acl2-doc_2.6-14_all.deb

I unpacked acl2_2.6-14_i386.deb using "ar x acl2_2.6-14_i386.deb" followed by
"tar zxf data.tar.gz", into a directory /home/kaufmann/apps/acl2/v2-6/.  I also
created a doc/ subdirectory, /home/kaufmann/apps/acl2/v2-6/doc/, and similarly
unpacked acl2-doc_2.6-14_all.deb there.  I'll refer below to
/home/kaufmann/apps/acl2/v2-6 as "....".

1. The books reside in ..../usr/share/acl2-2.6/books/, but
/home/kaufmann/apps/acl2/v2-6/usr/lib/acl2-2.6/books/ has just a portion of the
book directories, perhaps because you haven't yet included a full make in the
process.  (Or maybe that make was intended to be done as part of Debian package
installation?? -- which I'm avoiding since I have a Redhat machine.)

2. The .cert files are invalid, as they need correct absolute pathnames, which
were incorrect for my machine, e.g.  (from
..../usr/share/acl2-2.6/books/arithmetic/abs.cert):

/fix/t1/camm/tmp/acl2-2.6/books/arithmetic/abs.lisp

I think that the book certification will have to be done at installation time
rather than on your machine.  That probably means that there's no reason for
you to distribute the .o files for the books, since they will be re-created at
certification time.

It may be possible in some future ACL2 release to modify the nature of .cert
files so that they can refer to a system directory that avoids the need to
place those absolute pathnames in the .cert file.  With such a change, I think
you would be able to distribute .cert files.  Let me know if you think that is
important, in which case I'll put that on our "to do" list.

3. There is no need to distribute ..../usr/share/acl2-2.6/TMP1.lisp.

4. I'm not so sure about moving some of the stuff into doc.  For example,
..../doc/usr/share/doc/acl2-doc/books/arithmetic/README
talks about "contents of this directory", yet there are no such
contents -- the contents are in ..../usr/share/acl2-2.6/books/*/.

5. I didn't immediately find ..../doc/usr/share/info/.  But maybe Debian users
would know to look there.

-- Matt
   Cc: address@hidden, address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 17 Nov 2002 12:52:11 -0500

   Greetings!

   Matt Kaufmann <address@hidden> writes:

   > Hi --
   > 
   > I hadn't realized that an ACL2 Debian package is on the Web.  After getting
   > your email I did a google search and found
   > http://packages.debian.org/unstable/math/acl2.html; is that the right 
place to
   > look?  (It seems to point to version -11 rather than -12.)
   > 

   Yes this is the right place for the 'unstable' distribution.  In
   general, packages flow through Debian as follows:

   On upload, in http://incoming.debian.org
   After a day or so, at http://packages.debian.org/unstable/math/acl2.html
   After 10 days, if no critical bugs filed, at 
http://packages.debian.org/testing/math/acl2.html
   After ~ 6mos to 1 year, when a new stable is released, at 
http://packages.debian.org/stable/math/acl2.html

   Take care,

   > Thanks --
   > -- Matt
   >    Cc: address@hidden, address@hidden, address@hidden
   >    From: Camm Maguire <address@hidden>
   >    Date: 17 Nov 2002 00:11:50 -0500
   > 
   >    Greetings!  Just a note that I'm uploading version -12 of the package
   >    now.  It should be in the archives in a day or so.  I've tried to
   >    address all the points you raise below.  I'd greatly appreciate a
   >    knowledgeable person's feedback.
   > 
   >    Barring the unforeseen, I hope to release -13 in a few days with the
   >    sole change that the package will certify all the books.  By then 2.7
   >    should be ready and hopefully the package structure will be finalized.
   > 
   >    Take care,
   > 
   >    Matt Kaufmann <address@hidden> writes:
   > 
   >    > Hi, and thank YOU again for all your great GCL work --
   >    > 
   >    > As you requested, I have taken a look at the Debian ACL2 package that 
you
   >    > constructed.  Thanks for your work!  Here are some comments.
   >    > 
   >    > I downloaded 
http://ftp.debian.org/debian/pool/main/a/acl2/acl2_2.6-6_i386.deb
   >    > to my RedHat 7.3 laptop and then followed the instructions in
   >    > http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS.  (By the way, I had 
to become
   >    > root to do that; perhaps you could mention that in 
HOWTO-UNPACK-DEBS.)  I then
   >    > issued the command "acl2" at the shell and it seemed to work 
perfectly!  In
   >    > order to run ACL2 proof trees (meta-x proof-tree) in emacs, though, I 
needed to
   >    > execute the following forms in emacs (which I have added to my .emacs 
file).
   >    > 
   >    > (defvar *acl2-interface-dir* "/usr/share/emacs/site-lisp/acl2/")
   >    > 
   >    > (autoload 'start-proof-tree
   >    >   (concat *acl2-interface-dir* "top-start-shell-acl2")
   >    >   "Enable proof tree logging in a prooftree buffer."
   >    >   t)
   >    > 
   >    > But then they worked great; thanks.
   >    > 
   >    > Also, a file was missing in /usr/share/emacs/site-lisp/acl2/:
   >    > load-shell-acl2.el.  (That directory comes from the ACL2 
interface/emacs/
   >    > directory.)  I went ahead and copied it over manually (as root).  File
   >    > load-inferior-acl2.el was also missing, as were README, README.doc, 
README.mss,
   >    > and README.ps.
   >    > 
   >    > More importantly, several ACL2 directories (and their subdirectories) 
were
   >    > missing from the extraction.  In order of importance (most to least), 
they are
   >    > as follows, where acl2-sources is the top-level ACL2 source directory:
   >    > 
   >    > acl2-sources/        [users need to be able to browse the sources]
   >    > acl2-sources/books/  [these are like "libraries" -- pre-proved 
theorems etc.]
   >    > acl2-sources/doc/    [HTML, Emacs info, and Postscript documentation]
   >    > acl2-sources/emacs/  [Some emacs utilities]
   >    > acl2-sources/interface/infix/
   >    > 
   >    > I don't know enough about traditional file organization to suggest 
where these
   >    > should go in a Debian package.  Our method has been to allow ACL2 
users to
   >    > download ACL2 and put the acl2-sources directory anywhere they want,
   >    > maintaining the structure that we provide under acl2-sources/.  Under 
that
   >    > method, one of the first things to do is to run the "make 
certify-books"
   >    > command from acl2-sources/, in order to "certify" the many .lisp 
files under
   >    > acl2-sources/books/ (i.e., run them through ACL2).  This process 
compiles files
   >    > and, more importantly, writes out .cert files that have absolute 
pathnames.  I
   >    > don't know how that would fit into a Debian installation process.
   >    > 
   >    > >> > By the way, I'm hoping that we will release the next version 
(2.7) of ACL2
   >    > >> > later this month.  (It's been a year since we released ACL2 2.6.)
   >    > >> > 
   >    > >> 
   >    > >> Great!  Any surprises?
   >    > 
   >    > I don't think so.  The set of files has changed slightly, and of 
course the
   >    > contents of files have changed somewhat, but the basic structure is 
the same.
   >    > 
   >    > Thanks --
   >    > -- Matt
   >    >    Cc: address@hidden, address@hidden
   >    >    From: Camm Maguire <address@hidden>
   >    >    Date: 01 Nov 2002 19:41:24 -0500
   >    > 
   >    >    Greetings, and thanks for your reply!
   >    > 
   >    >    Matt Kaufmann <address@hidden> writes:
   >    > 
   >    >    > Hi, Camm --
   >    >    > 
   >    >    > That's really great that GCL is in such good shape!
   >    >    > 
   >    >    > I've added two targets to the top-level ACL2 Makefile for you, 
so that you can
   >    >    > easily run short tests.  In both cases, the exit status should 
be 0 if the test
   >    >    > succeeded and non-zero otherwise.  Two files need to be edited: 
Makefile and
   >    >    > books/Makefile.  At the end below are editing instructions, but 
if you'd rather
   >    >    > I just email you the entire files, let me know.
   >    >    > 
   >    > 
   >    >    Many thanks!  I've added these.  BTW, Debian's autobuilders expect
   >    >    *some* output from the build at least every 15 minutes.  For
   >    >    potentially long running tests with redirected standard output, I
   >    >    usually use this trick:
   >    > 
   >    >          $(MAKE) short-test-aux > short-test.log 2> short-test.log & 
j=$$! ; \
   >    >          tail -f --pid=$$j --retry short-test.log & wait $$j
   >    > 
   >    > 
   >    >    > >> Lastly, I'd be most appreciate if you or some other 
knowledgeable acl2
   >    >    > >> user could look at the package and comment as to whether 
everything is
   >    >    > >> available and in the right place.
   >    >    > 
   >    >    > Sure.  Please point me to where it is.  I don't know anything 
about Debian
   >    >    > packages but I'll try to find someone who does.  Or would it 
suffice to follow
   >    >    > the instructions at 
http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS and build
   >    >    > it on my Redhat 7.3 laptop?
   >    >    > 
   >    > 
   >    >    http://ftp.debian.org/debian/pool/main/a/acl2/
   >    > 
   >    >    > By the way, I'm hoping that we will release the next version 
(2.7) of ACL2
   >    >    > later this month.  (It's been a year since we released ACL2 2.6.)
   >    >    > 
   >    > 
   >    >    Great!  Any surprises?
   >    > 
   >    >    > Finally, regarding your emacs point:
   >    >    > 
   >    >    > >> Also, a Debian user has already brought up a minor issue in 
the emacs
   >    >    > >> lisp interface regarding differences between xemacs and GNU 
emacs.  He
   >    >    > >> is suggesting the following:
   >    >    > >> 
   >    >    > >> 
=============================================================================
   >    >    > >> (defun acl2-shared-lisp-mode-map ()
   >    >    > >>   "Return the shared lisp-mode-map, independent of Emacs 
version."
   >    >    > >>   (if (boundp 'shared-lisp-mode-map)
   >    >    > >>       shared-lisp-mode-map
   >    >    > >>     lisp-mode-shared-map))
   >    >    > >> 
   >    >    > >> and replacing references to shared-lisp-mode-map with
   >    >    > >> (acl2-shared-lisp-mode-map) ought to work.  (I actually even 
tested
   >    >    > >> the approach with GNU Emacs 20, GNU Emacs 21, and XEmacs 21 
this
   >    >    > >> time; I get byte-compiler warnings, but that's all. ;-))
   >    >    > >> 
=============================================================================
   >    >    > >> 
   >    >    > >> Do you have any thoughts here?
   >    >    > 
   >    >    > Thanks very much.  I guess you're referring to directory 
interface/emacs/ in
   >    >    > the ACL2 distribution; is that right?  Your solution looks 
reasonable to me.
   >    >    > 
   >    > 
   >    >    OK, its in.
   >    > 
   >    > 
   >    >    Thanks again!
   >    > 
   >    > 
   >    >    -- 
   >    >    Camm Maguire                                               
address@hidden
   >    >    
==========================================================================
   >    >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   >    > 
   >    > 
   >    > _______________________________________________
   >    > Gcl-devel mailing list
   >    > address@hidden
   >    > http://mail.gnu.org/mailman/listinfo/gcl-devel
   >    > 
   >    > 
   > 
   >    -- 
   >    Camm Maguire                                            address@hidden
   >    
==========================================================================
   >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   > 
   > 

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