[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: ACL2 Version 4.0
|
From: |
Camm Maguire |
|
Subject: |
[Gcl-devel] Re: ACL2 Version 4.0 |
|
Date: |
Sun, 25 Jul 2010 21:31:01 -0400 |
|
User-agent: |
Gnus/5.11 (Gnus v5.11) Emacs/22.2 (gnu/linux) |
Greetings!
Matt Kaufmann <address@hidden> writes:
> Hi, Camm --
>
> Thanks for the good news about intel and ppc macs! Which were the two
> books that failed due to insufficient memory? (If you don't have the
> answer handy, please don't bother answering.)
>
misc/misc2/reverse-by-separation.cert and coi/gacc/wrap.cert.
> Would you remind me of the latest, best way to fetch the latest GCL so
> that I can build using it? I followed the instructions on the ACL2
> web site (which are based on something you sent a long time ago, I
> think), but they didn't work:
>
> ~/lisps/gcl$ export CVS_RSH=ssh
> ~/lisps/gcl$ cvs -d:ext:address@hidden:/cvsroot/gcl co gcl
> The authenticity of host 'subversions.gnu.org (140.186.70.70)' can't be
> established.
> RSA key fingerprint is b5:a7:31:c7:75:69:a6:67:82:8c:ae:0c:a6:d2:b5:ac.
> Are you sure you want to continue connecting (yes/no)? yes
>
cvs -z9 -q -d:pserver:address@hidden:/sources/gcl \
co -d gcl-2.6.8pre -r Version_2_6_8pre gcl
> Warning: Permanently added 'subversions.gnu.org,140.186.70.70' (RSA) to the
> list of known hosts.
> Permission denied (publickey).
> cvs [checkout aborted]: end of file from server (consult above messages if
> any)
> ~/lisps/gcl$
>
> Regarding that include-book problem, perhaps the most efficient way
> for both of us to solve this would be for you to send me a tarball,
> together with commands I can issue that re-do the creation of the
> .cert files. I'll probably use ubuntu linux, if that's OK. If the
> include-book then fails for me too, then I should be able to get to
> the bottom of the problem.
>
We came up with this patch to saved_acl2 before the book
certification:
saved_acl2.c: saved_acl2
echo "(f-put-global 'old-certification-dir \"$$(pwd)/books\" state)" \
"(f-put-global 'new-certification-dir \"/usr/share/$(PD)/books\"
state)" \
":q #+(or sparc sparc64)(progn (si::sgc-on nil) (fmakunbound
'si::sgc-on))" \
"(save-exec \"address@hidden" \"Modified to produce final
certification files\")" | ./$<
I can send you the source package which will build fine on Ubuntu.
But to test, you have to install the packages and thereby the cert
files in their new locations. For the latter, you just need the
existing packages. Which would you like?
> Were you able to do that include-book test successfully with a recent
> Debian build, say for ACL2 3.6.1?
>
Yes.
Take care,
> -- Matt
> cc: address@hidden
> From: Camm Maguire <address@hidden>
> Date: Sun, 25 Jul 2010 11:38:26 -0400
> X-MagicMail-UUID: c25e9556-981f-11df-bee4-000c293e29ca
> X-SpamAssassin-Status: No, hits=1.9 required=5.0
> X-UTCS-Spam-Status: No, hits=-220 required=165
>
> Greetings, and thanks for pointing this out!
>
> It seems we need an adjustment here:
>
>
> =============================================================================
> GCL (GNU Common Lisp) 2.6.7 CLtL1 Apr 29 2010 18:42:31
> Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl)
> Binary License: GPL due to GPL'ed components: (XGCL READLINE BFD UNEXEC)
> Modifications of this banner must retain notice of a compatible license
> Dedicated to the memory of W. Schelter
>
> Use (help) to get some basic information on how to use GCL.
> Temporary directory for compiler files set to /tmp/
>
> ACL2 Version 4.0 built July 9, 2010 13:05:18.
> Copyright (C) 2010 University of Texas at Austin
> ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
> are welcome to redistribute it under certain conditions. For details,
> see the GNU General Public License.
>
> Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
> See the documentation topic note-4-0 for recent changes.
> Note: We have modified the prompt in some underlying Lisps to further
> distinguish it from the ACL2 prompt.
>
> ACL2 Version 4.0. Level 1. Cbd "/home/camm/debian/axiom/axiom-20100701/".
> Distributed books directory "/usr/share/acl2-4.0/books/".
> Type :help for help.
> Type (good-bye) to quit completely out of ACL2.
>
> ACL2 !>(include-book "arithmetic/top-with-meta" :dir :system)
>
> Loading /usr/share/acl2-4.0/books/arithmetic/top-with-meta.o
> Loading /usr/share/acl2-4.0/books/arithmetic/top.o
> Loading /usr/share/acl2-4.0/books/arithmetic/equalities.o
> Loading /usr/share/acl2-4.0/books/cowles/acl2-crg.o
> Loading /usr/share/acl2-4.0/books/cowles/acl2-agp.o
> Loading /usr/share/acl2-4.0/books/cowles/acl2-asg.o
> start address -T 0x9ed7000 Finished loading
> /usr/share/acl2-4.0/books/cowles/acl2-asg.o
> start address -T 0xa4c4000 Finished loading
> /usr/share/acl2-4.0/books/cowles/acl2-agp.o
> start address -T 0x92f0000 Finished loading
> /usr/share/acl2-4.0/books/cowles/acl2-crg.o
> start address -T 0x8fbd950 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/equalities.o
> Loading /usr/share/acl2-4.0/books/arithmetic/rational-listp.o
> start address -T 0x93a2f90 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/rational-listp.o
> Loading /usr/share/acl2-4.0/books/arithmetic/inequalities.o
> start address -T 0x9ed7f90 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/inequalities.o
> Loading /usr/share/acl2-4.0/books/arithmetic/natp-posp.o
> start address -T 0x8fbd570 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/natp-posp.o
> Loading /usr/share/acl2-4.0/books/arithmetic/rationals.o
> start address -T 0xae15f80 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/rationals.o
> start address -T 0x8fbdbf0 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/top.o
> Loading /usr/share/acl2-4.0/books/meta/meta.o
> Loading /usr/share/acl2-4.0/books/meta/meta-plus-equal.o
> Loading /usr/share/acl2-4.0/books/meta/term-defuns.o
> start address -T 0xae89000 Finished loading
> /usr/share/acl2-4.0/books/meta/term-defuns.o
> start address -T 0x9c38000 Finished loading
> /usr/share/acl2-4.0/books/meta/meta-plus-equal.o
> Loading /usr/share/acl2-4.0/books/meta/meta-plus-lessp.o
> start address -T 0xaf5d000 Finished loading
> /usr/share/acl2-4.0/books/meta/meta-plus-lessp.o
> Loading /usr/share/acl2-4.0/books/meta/meta-times-equal.o
> start address -T 0xb006000 Finished loading
> /usr/share/acl2-4.0/books/meta/meta-times-equal.o
> start address -T 0x8fbd8c0 Finished loading
> /usr/share/acl2-4.0/books/meta/meta.o
> start address -T 0x8fbd010 Finished loading
> /usr/share/acl2-4.0/books/arithmetic/top-with-meta.o
> [SGC for 45 STRING pages..(11246 writable)..(T=3).GC finished]
> [SGC for 7 CFUN pages..(11271 writable)..(T=1).GC finished]
> [SGC for 7 CFUN pages..(11280 writable)..(T=1).GC finished]
>
> ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "meta-times-equal" ...):
> The certificate on file for
> "/usr/share/acl2-4.0/books/meta/meta-times-equal.lisp" lists the check
> sum of the certified book as 877036282. But the check sum of the events
> now in the file is 2059408155. This generally indicates that the file
> has been modified since it was last certified.
>
>
> ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "meta/meta" ...): After
> including the book "/usr/share/acl2-4.0/books/meta/meta.lisp":
>
> -- its certificate requires the book "meta-times-equal" with certificate
> annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS))
> and check sum 877036282, but we have included an uncertified version
> of "meta-times-equal" with certificate annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)), so book recertification
> is probably required.
>
>
> ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "arithmetic/top-with-meta"
> ...): After including the book
> "/usr/share/acl2-4.0/books/arithmetic/top-with-meta.lisp":
>
> -- its certificate requires the book "meta" with certificate annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS))
> and check sum 1784568738, but we have included an uncertified version
> of "meta" with certificate annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)), so book recertification
> is probably required;
>
> -- its certificate requires the book "meta-times-equal" with certificate
> annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS))
> and check sum 877036282, but we have included an uncertified version
> of "meta-times-equal" with certificate annotations
> ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)), so book recertification
> is probably required.
>
>
> Summary
> Form: ( INCLUDE-BOOK "arithmetic/top-with-meta" ...)
> Rules: NIL
> Warnings: Uncertified
> Time: 0.15 seconds (prove: 0.00, print: 0.00, other: 0.15)
> "/usr/share/acl2-4.0/books/arithmetic/top-with-meta.lisp"
> ACL2 !>
>
> =============================================================================
>
> Advice most appreciated.
>
> Secondarily, acl2 builds on current gcl on intel and ppc mac verifying
> all books. There is a small issue that two books need more memory
> than the standard setup when sgc is not available and
> si::*optimize-maximum-pages* is on. Building for windows running
> cross compiled under wine is currently in testing.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > Hi, Camm --
> >
> > I've taken a look, and I didn't see anything amiss in the organization
> > (though I'm not particularly awk-literate and haven't thought about
> > Debian in awhile). We did make some changes in the book certification
> > mechanism, so it's worth testing to see your set-up still works (where
> > certificates are moved). A reasonable test is to do your usual Debian
> > build, and then start up ACL2 and try this:
> >
> > (include-book "arithmetic/top-with-meta" :dir :system)
> >
> > You should get a nice clean log, e.g. (though I did this on my Mac
> > with another underlying host Lisp):
> >
> > ACL2 !>(include-book "arithmetic/top-with-meta" :dir :system)
> >
> > Summary
> > Form: ( INCLUDE-BOOK "arithmetic/top-with-meta" ...)
> > Rules: NIL
> > Time: 0.09 seconds (prove: 0.00, print: 0.00, other: 0.09)
> > "/Users/kaufmann/acl2/devel/books/arithmetic/top-with-meta.lisp"
> > ACL2 !>
> >
> > Thanks --
> > -- Matt
> > From: Camm Maguire <address@hidden>
> > Date: Thu, 15 Jul 2010 17:28:44 -0400
> > X-SpamAssassin-Status: No, hits=-2.4 required=5.0
> > X-UTCS-Spam-Status: No, hits=-237 required=165
> >
> > Greetings! OK, here are the makefile snippets. Please let me know if
> > anything seems amiss. We had worked this out a long time ago -- just
> > looking for 4.x updates.
> >
> > Take care,
> >
> > INSTALLS:=$(addprefix debian/,$(addsuffix .install,acl2 acl2-source
> acl2-emacs acl2-doc acl2-books acl2-books-source acl2-books-certs acl2-infix
> acl2-infix-source))
> > LINKS:=$(addprefix debian/,$(addsuffix .links,acl2 acl2-books
> acl2-infix))
> > IFILES:=$(INSTALLS) $(shell ls -1 debian/*.examples debian/*.docs)
> >
> > debian/README.Debian: debian/README.Debian.in $(IFILES)
> > awk '/@PLIST@/ {exit 0} {print}' $< >$@
> > for i in $(filter %.install,$^); do\
> > awk '/^debian\// {next} {sub(".final$$","",$$1);$$2="/" $$2;print
> $$0 " " p}' \
> > p=$$(basename $${i%.install}) $$i >>$@ ; done
> > for i in $(filter %.info,$^); do\
> > awk '/^debian\// {next} {print $$0 " /usr/share/info " p}'
> p=$$(basename $${i%.info}) $$i >>$@ ; done
> > for i in $(filter %.examples,$^); do\
> > awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p "/examples
> " p}' \
> > p=$$(basename $${i%.examples}) $$i >>$@ ; done
> > for i in $(filter %.docs,$^); do\
> > awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p " " p}'
> p=$$(basename $${i%.docs}) $$i >>$@ ; done
> > awk '/@PLIST@/ {i=1;next} {if (i) print}' $< >>$@
> >
> >
> > debian/acl2-infix.install::
> > find interface/infix -name "*.o" | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
> > find interface/infix -name "*.sty" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/texmf/tex/latex\n",$$1);}' >>$@
> >
> > debian/acl2-infix-source.install::
> > find interface/infix -name "*.lisp" | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
> >
> > debian/acl2-emacs.install::
> > find interface/emacs -name "*.el" | awk '{printf("%s
> usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
> > find emacs -name "*.el" | awk '{printf("%s
> usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
> >
> > debian/acl2.install::
> > echo debian/acl2.sh usr/bin >>$@
> > echo saved_acl2 usr/lib/$(PD) >>$@
> >
> > debian/acl2-books.install::
> > find books -name "*.o" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
> >
> > debian/acl2-source.install::
> > find * -name "*.lisp" -maxdepth 0 | grep -v TMP1.lisp | awk
> '{printf("%s usr/share/$(PD)\n",$$1);}' >$@
> > find * -name "TAGS" -maxdepth 0 | awk '{printf("%s
> usr/share/$(PD)\n",$$1);}' >>$@
> >
> > debian/acl2-books-certs.install::
> > find books -name "*.cert" | grep -v fix-cert/moved | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s.final usr/share/$(PD)/%s\n",$$1,a);}'
> >>$@
> >
> > debian/acl2-books-source.install::
> > find books -name "*.lisp" | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
> > find books -name "*.acl2" | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
> > find books/bdd -name "bit-vector-reader.lsp" | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
> >
> > debian/acl2-doc.install::
> > echo doc/HTML usr/share/doc/acl2-doc >$@
> > find books -name "README*" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find books/textbook -name "*.txt" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find books/textbook -name "*.html" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find books/bdd/be/ -type f | awk
> '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find books/misc -name "simplify-defuns.txt" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find interface/infix -name "README*" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find interface/infix -name "*.ps" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find interface/infix -name "*.dvi" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find interface/emacs -name "README*" | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> > find books/arithmetic-2/pass1/arithmetic-axioms.txt | \
> > awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s
> usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
> >
> > debian/acl2.links::
> > echo usr/lib/$(PD)/saved_acl2 usr/share/$(PD)/saved_acl2 >$@
> >
> > debian/acl2-books.links::
> > find books -name "*.o" | awk '{printf("usr/lib/$(PD)/%s
> usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@
> >
> > debian/acl2-infix.links::
> > find interface/infix -name "*.o" | awk '{printf("usr/lib/$(PD)/%s
> usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@
> >
> >
> >
> > Matt Kaufmann <address@hidden> writes:
> >
> > > Hi, Camm --
> > >
> > > Sure, you might as well send it to me. I'm still packing and then
> > > leaving for a conference followed by 2 months in the UK -- I'll try
> to
> > > find time in the next couple of weeks or so -- if it's kind of
> urgent
> > > though, let me know. I would like to help get ACL2 4.0 Debianized
> > > (just want to maintain my sanity and sleep in the process...).
> > >
> > > Thanks --
> > > -- Matt
> > > From: Camm Maguire <address@hidden>
> > > Date: Thu, 08 Jul 2010 23:32:42 -0400
> > > X-MagicMail-UUID: aade0492-8b0a-11df-b736-000c29c6406d
> > > X-SpamAssassin-Status: No, hits=0.3 required=5.0
> > > X-UTCS-Spam-Status: No, hits=-210 required=165
> > >
> > > Greetings!
> > >
> > > Matt Kaufmann <address@hidden> writes:
> > >
> > > > Hi, Camm --
> > > >
> > > > Thanks. I may be missing something. Is there a program of
> some sort
> > > > that generates the lines starting with this one?
> > > >
> > > > saved_acl2 /usr/lib/acl2-4.0 acl2
> > > >
> > > > Or is all that updated manually with each release?
> > > >
> > >
> > > This is updated by program. There are several 'find' calls in
> the
> > > package building process which generates this list. I can show
> you
> > > that script if you'd like.
> > >
> > > Take care,
> > >
> > > > Thanks --
> > > > -- Matt
> > > > From: Camm Maguire <address@hidden>
> > > > Date: Thu, 08 Jul 2010 17:02:45 -0400
> > > > X-MagicMail-UUID: 315ad432-8ad4-11df-9c63-000c29c6406d
> > > > X-SpamAssassin-Status: No, hits=0.4 required=5.0
> > > > X-UTCS-Spam-Status: No, hits=-210 required=165
> > > >
> > > > --=-=-=
> > > >
> > > > Greetings!
> > > >
> > > > Matt Kaufmann <address@hidden> writes:
> > > >
> > > > > Hi, Camm -- I'm about to leave the country for over 2
> months -- am
> > > > >busy packing and then will be at a conference, then
> traveling. So it
> > > > >may take me at least a couple of weeks. Do you have any
> tools for
> > > > >mapping files from the ACL2 distribution to the Debian
> distribution?
> > > > >It seems to me that inspecting on a file-by-file basis is
> excessively
> > > > >time-consuming; probably there's a way to map just a few
> directories
> > > > >that is sufficient to guide the process, and maybe you
> already have
> > > > >such a system. Even some sort of guiding principle in
> English might
> > > > >be useful for me to help validate the Debian organization
> of ACL2
> > > > >files.
> > > >
> > > > Yes, we put one together, automatically generated in the
> > > > README.Debian.gz file, included below for your perusal when
> time
> > > > permits. Please let me know if this is not what you are
> looking for.
> > > >
> > > > Take care,
> > > >
> > > > > I've attached a list of all files in the ACL2
> distribution, as
> > > > > though using "ls -1R", in case that helps. > Thanks for
> your work
> > > > > for Macs! > -- Matt cc: address@hidden From: Camm Maguire
> > > > > <address@hidden> Date: Thu, 08 Jul 2010 15:16:32 -0400
> > > > > X-MagicMail-UUID: 1d3ed182-8ac6-11df-8377-000c29c6406d
> > > > > X-SpamAssassin-Status: No, hits=0.3 required=5.0
> X-UTCS-Spam-Status:
> > > > > No, hits=-220 required=165 > Greetings! > 1) I've
> uploaded acl2-4.0
> > > > > into Debian. I know there are perhaps some non-trivial
> changes, so
> > > > > I was wondering if you would find it useful to reexamine
> the acl2
> > > > > package structure for needed changes. If so, you can
> find .deb
> > > > > files at >
> > > > >
> ftp://ftp.debian.org/debian/pool/main/a/acl2/*4.0*i386*deb > and can
> > > > > see a listing with > dpkg -c foo.deb > or > ar x foo.deb;
> tar tvf
> > > > > data.tgz > 2) I have the ppc and intel macs working
> together now on
> > > > > the same codebase. Have not yet uploaded into the gcl
> cvs source
> > > > > tree. Your machine has been invaluable -- thanks! --
> 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
> > > >
> > > >
> > > > --=-=-=
> > > > Content-Type: text/plain; charset=us-ascii
> > > > X-Former-Content-Type: application/octet-stream
> > > > X-Former-Content-Disposition: attachment;
> filename=README.Debian.gz
> > > > Content-Transfer-Encoding: 7bit
> > > > X-Former-Content-Transfer-Encoding: base64
> > > > Content-Description: README.Debian.gz
> > > >
> > > > [file:/u/kaufmann/detached/README.Debian.gz]
> > > > --=-=-=--
> > > >
> > > >
> > > >
> > > >
> > >
> > > --
> > > 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
> >
> >
> >
> >
>
> --
> 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
- [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/08
- [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/08
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- Message not available
- [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/25
- [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/25
- [Gcl-devel] Re: ACL2 Version 4.0,
Camm Maguire <=
- [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/26
- Message not available
- Message not available
- Message not available
- [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/26
- [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/26
- Re: [Gcl-devel] Re: ACL2 Version 4.0, George W. Dinolt, 2010/07/26
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/27
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/27
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/27
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/27
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/27
- Re: [Gcl-devel] Re: ACL2 Version 4.0, Matt Kaufmann, 2010/07/27