[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: ACL2 Version 4.0
|
From: |
Matt Kaufmann |
|
Subject: |
[Gcl-devel] Re: ACL2 Version 4.0 |
|
Date: |
Sun, 25 Jul 2010 14:23:45 -0500 |
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.)
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
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.
Were you able to do that include-book test successfully with a recent
Debian build, say for ACL2 3.6.1?
-- 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
- [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 <=
- [Gcl-devel] Re: ACL2 Version 4.0, Camm Maguire, 2010/07/25
- [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