[Gcl-devel] Re: ACL2 Version 4.0

[Camm Maguire]

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