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

[Matt Kaufmann]

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

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