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

[Camm Maguire]

Greetings, and thanks as always for your feedback!

Matt Kaufmann <address@hidden> writes:

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

This is correct.  The package build pushes whatever .o files it finds
under books to /usr/lib/acl2-2.6, making whatever directories
necessary in the process, and linking back to /usr/share.  When the
full build is run, presumably all directories will appear in /usr/lib.

> 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 received your subsequent note indicating that include-books still
works.  Nevertheless, I've just added a bit to debian/rules to insert
the correct final path into these files.  In general, no references to
the build directory should exist in the package.  I haven't double
checked everything on this score yet.

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

OK, removed!

> 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/*/.
> 

I wasn't too sure about this either -- however, this is *definitely*
the standard place for Debian documentation, and all users will look
there.  No one by default will ever think of looking for anything
under /usr/share, unless they are a sysadmin or something.  Which is
again interesting given that the .lisp files are here.  But I don't
think there is any better place for these.

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

All info reading tools, (e.g. emacs, info) look here.  On a Debian
box, you can just fire up emacs and do a C-h i to see the info pages.

Take care,

> -- 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
> 
> 
> 
> _______________________________________________
> 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