[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
test.
mini-proveall:
@rm -rf mini-proveall.out
@echo '(value :q) (lp) (mini-proveall)' | ${PREFIXsaved_acl2} >
mini-proveall.out
@(grep '^ ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR-TEST'
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
certifications:
certify-books-short:
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.
short-clean:
@rm -f short-test.log
@for dir in $(DIRS1) $(SHORTDIRS2) ; \
do \
(cd $$dir ; \
$(MAKE) clean ; \
cd ..) ; \
done
short-test-aux:
@for dir in $(DIRS1) ; \
do \
(cd $$dir ; \
$(MAKE) all ; \
cd ..) ; \
done
@$(MAKE) top-with-meta-cert
@for dir in $(SHORTDIRS2) ; \
do \
(cd $$dir ; \
$(MAKE) all ; \
cd ..) ; \
done
short-test:
@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
- [Gcl-devel] gcl/acl2, Camm Maguire, 2002/11/01
- Re: [Gcl-devel] gcl/acl2, C Y, 2002/11/01
- [Gcl-devel] Re: gcl/acl2,
Matt Kaufmann <=
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/02
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/02
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/03
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/10
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/13
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12