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

[Camm Maguire]

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