[Gcl-devel] Re: gcl/acl2

[Camm Maguire]

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