[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: gcl/acl2

From: Matt Kaufmann
Subject: [Gcl-devel] Re: gcl/acl2
Date: Fri, 1 Nov 2002 14:08:15 -0600 (CST)

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.

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

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

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.

Finally, here are the instructions promised above.

========== Instructions for editing ACL2 Makefile and books/Makefile ==========

You can add the following to the end of Makefile, which will allows you to run
the mini-proveall by typing "make mini-proveall".  However, that's a very short

        @rm -rf mini-proveall.out
        @echo '(value :q) (lp) (mini-proveall)' | ${PREFIXsaved_acl2} > 
mini-proveall.out > /dev/null) || \
        (echo 'Mini-proveall failed!' ; exit 1)
        @echo 'Mini-proveall passed.'

The other new target takes about halfway inbetween 1/3 and 1/2 the time
required to do a "make" (to build ACL2), by running just some of the book

        cd books ; make short-test

The above two sections can be added at the end of Makefile.  Also,
books/Makefile needs editing.  Just above this line

.PHONY: $(DIRS1) $(DIRS2) $(DIRS3)

add the following line:

SHORTDIRS2 = data-structures bdd

Then at the end, add the following lines.

        @rm -f short-test.log
        @for dir in $(DIRS1) $(SHORTDIRS2) ; \
        do \
        (cd $$dir ; \
        $(MAKE) clean ; \
        cd ..) ; \

        @for dir in $(DIRS1) ; \
        do \
        (cd $$dir ; \
        $(MAKE) all ; \
        cd ..) ; \
        @$(MAKE) top-with-meta-cert
        @for dir in $(SHORTDIRS2) ; \
        do \
        (cd $$dir ; \
        $(MAKE) all ; \
        cd ..) ; \

        @rm -f short-test.log
        $(MAKE) short-clean
        $(MAKE) short-test-aux > short-test.log 2> short-test.log
        @if [ ! -f short-test.log ] || (fgrep '**' short-test.log > /dev/null) 
; then \
        (echo 'Short test failed!' ; exit 1) ; else \
        echo 'Short test passed.' ; fi


Thanks --
-- Matt

reply via email to

[Prev in Thread] Current Thread [Next in Thread]