[Gcl-devel] Re: gcl/acl2

[Matt Kaufmann]

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