gcl-devel
[Top][All Lists]
Advanced

[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: Mon, 26 Jul 2010 03:08:13 -0500

Hi, Camm --

Thank you for the cvs command; I've updated the ACL2 website
accordingly (in the section on obtaining GCL).

I executed that cvs command on my Intel Mac.  Then I ran ./configure,
which seemed to succeed.  But then I ran make, and got an error.  The
log concludes as follows (I'll send the full log in a separate email
that spares gcl-devel):

  gcc  -Wall -DVOL=volatile -fsigned-char -pipe -O3 -fomit-frame-pointer  
-I/Users/kaufmann/lisps/gcl/gcl-2.6.8pre/o -I../h -I../o -o rsym rsym.c
  In file included from rsym.c:18:
  rsym_macosx.c: In function 'rsym_doit2':
  rsym_macosx.c:87: error: 'union <anonymous>' has no member named 'n_name'
  rsym_macosx.c: In function 'rsym_doit1':
  rsym_macosx.c:138: warning: implicit declaration of function 'map_fd'
  rsym_macosx.c:179: error: 'union <anonymous>' has no member named 'n_name'
  rsym_macosx.c:182: error: 'union <anonymous>' has no member named 'n_name'
  rsym_macosx.c:184: error: 'union <anonymous>' has no member named 'n_name'
  rsym_macosx.c:188: error: 'union <anonymous>' has no member named 'n_name'
  make[1]: *** [rsym] Error 1
  make: *** [unixport/saved_pre_gcl] Error 2
  ~/lisps/gcl/gcl-2.6.8pre$ 

Thanks for naming the two books; nothing in particular comes to mind
about them, except that I remember that
misc/misc2/reverse-by-separation.cert takes unusually long to certfiy.

I think your saved_acl2.c target might be enough for me to reproduce
the problem.  I'll try to get to that in the next couple of weeks; I'm
still on extended vacation, but can speed this up if you need a
solution sooner.

Thanks --
-- Matt
   Cc: address@hidden
   From: Camm Maguire <address@hidden>
   Date: Sun, 25 Jul 2010 21:31:01 -0400
   X-MagicMail-UUID: 78300574-9855-11df-aca2-000c29c6406d
   X-SpamAssassin-Status: No, hits=-2.3 required=5.0
   X-UTCS-Spam-Status: No, hits=-275 required=165

   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




reply via email to

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