gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] Re: ACL2 binaries


From: Matt Kaufmann
Subject: Re: [Gcl-devel] Re: ACL2 binaries
Date: Thu, 28 Oct 2004 11:16:50 -0500

Howdy --

The second error is a consequence of the first.  But the first is completely
surprising.  Are you using the copy of workshops/1999/simulator/ derived from
/stage/ftp/pub/moore/acl2/v2-9/acl2-sources/books/workshops.tar.gz?

If so, then I'm at a loss.  A first step would be for you to submit the
following to the shell and send me the log.  It might also be interesting for
you to execute (expt 2 32) after starting up ACL2, and also in GCL, and verify
the results.

cd /home/camm/acl2-2.9/books/workshops/1999/simulator/
acl2
(rebuild "tiny.lisp" 'plus<32>-works)
:u
(defthm plus<32>-works
  (implies
   (and
    (signed-byte-p 32 a)
    (signed-byte-p 32 b))
  (equal
   (plus<32> a b)
   (+bv32 a b)))
  :hints (("goal" :use ((:instance logext-+-logext (size 32) (i (+ a b)) (j (- 
(expt 2 32))))
                        (:instance logext-+-logext (size 32) (i (+ a b)) (j 
(expt 2 32))))
           :in-theory (set-difference-theories (enable signed-byte-p) 
'(logext-+-logext)))))

Thanks --
-- Matt
   Cc: address@hidden, address@hidden, address@hidden,
           address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 28 Oct 2004 10:27:09 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-232 required=180

   Greetings!

   Matt Kaufmann <address@hidden> writes:

   > > I'm hoping that the make will bomb and exit with an error code if one
   > > of the certification steps fails.
   > 
   > Hmmm, that's a good point and I don't think we do that.  Rather, we print 
** to
   > the log file.  I've made a note to improve this before the next release 
(time
   > permitting) to return a non-zero error code.
   > 

   OK, thank you for clarifying.  Then we have two issues on ia64, with
   which I hope to seek your help, as I cannot yet make sense of the
   output:

   =============================================================================
   workshops/1999/simulator/tiny.out
   =============================================================================
   GCL (GNU Common Lisp)  2.6.5 CLtL1    Sep  3 2004 20:49:20
   Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
   Binary License:  GPL due to GPL'ed components: (READLINE 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.

    ACL2 Version 2.9 built October 22, 2004  20:52:30.
    Copyright (C) 2004  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*
                         /usr/share/acl2-2.9/).
    See the documentation topic note-2-9 for recent changes.

    NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
    look under the ACL2 source directory in interface/emacs/README.doc; 
    and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
    command loop.   Look in the ACL2 documentation under PROOF-TREE.

   ACL2 Version 2.9.  Level 1.  Cbd 
   "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
   Type :help for help.
   Type (good-bye) to quit completely out of ACL2.

   ACL2 !>
   Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
   ACL2>
   #<"ACL2" package>

   ACL2>
   ACL2 Version 2.9.  Level 1.  Cbd 
   "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
   Type :help for help.
   Type (good-bye) to quit completely out of ACL2.

   ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
   ACL2 !>[SGC for 243 CONS pages..(5726 writable)..(T=90).GC finished]
   [SGC for 243 CONS pages..(5729 writable)..(T=95).GC finished]

   Loading /home/camm/acl2-2.9/books/arithmetic/equalities.o
    start address (dynamic) 0x20000000007d0e50 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/equalities.o
   Loading /home/camm/acl2-2.9/books/arithmetic/rational-listp.o
    start address (dynamic) 0x20000000007d0ea0 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/rational-listp.o
   [SGC for 191 SFUN pages..(6749 writable)..(T=275).GC finished]
   Loading /home/camm/acl2-2.9/books/arithmetic/inequalities.o
    start address (dynamic) 0x20000000007d0ef0 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/inequalities.o
   Loading /home/camm/acl2-2.9/books/arithmetic/natp-posp.o
    start address (dynamic) 0x20000000007d0f40 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/natp-posp.o
   Loading /home/camm/acl2-2.9/books/arithmetic/rationals.o
    start address (dynamic) 0x20000000007d0f90 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/rationals.o
   Loading /home/camm/acl2-2.9/books/arithmetic/top.o
    start address (dynamic) 0x20000000007d0fe0 Finished loading 
/home/camm/acl2-2.9/books/arithmetic/top.o

   Summary
   Form:  ( INCLUDE-BOOK "../../../arithmetic/top" ...)
   Rules: NIL
   Warnings:  None
   Time:  13.65 seconds (prove: 0.00, print: 0.00, other: 13.65)
   "/home/camm/acl2-2.9/books/arithmetic/top.lisp"
   Loading /home/camm/acl2-2.9/books/data-structures/list-defuns.o
    start address (dynamic) 0x20000000007d1250 Finished loading 
/home/camm/acl2-2.9/books/data-structures/list-defuns.o
   [SGC for 191 SFUN pages..(6791 writable)..(T=292).GC finished]
   Loading /home/camm/acl2-2.9/books/data-structures/list-defthms.o
    start address (dynamic) 0x20000000007d12a0 Finished loading 
/home/camm/acl2-2.9/books/data-structures/list-defthms.o

   Summary
   Form:  ( INCLUDE-BOOK "../../../data-structures/list-defthms" ...)
   Rules: NIL
   Warnings:  None
   Time:  8.06 seconds (prove: 0.00, print: 0.01, other: 8.05)
   "/home/camm/acl2-2.9/books/data-structures/list-defthms.lisp"
   Loading /home/camm/acl2-2.9/books/meta/term-defuns.o
    start address (dynamic) 0x20000000007d1430 Finished loading 
/home/camm/acl2-2.9/books/meta/term-defuns.o
   Loading /home/camm/acl2-2.9/books/meta/meta-plus-equal.o
    start address (dynamic) 0x20000000007d1540 Finished loading 
/home/camm/acl2-2.9/books/meta/meta-plus-equal.o
   [SGC for 1114 CONS pages..(6942 writable)..(T=321).GC finished]
   Loading /home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
    start address (dynamic) 0x20000000007d1650 Finished loading 
/home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
   Loading /home/camm/acl2-2.9/books/meta/meta-times-equal.o
    start address (dynamic) 0x20000000007d1790 Finished loading 
/home/camm/acl2-2.9/books/meta/meta-times-equal.o
   Loading /home/camm/acl2-2.9/books/meta/meta.o
    start address (dynamic) 0x20000000007d17e0 Finished loading 
/home/camm/acl2-2.9/books/meta/meta.o

   Summary
   Form:  ( INCLUDE-BOOK "../../../meta/meta" ...)
   Rules: NIL
   Warnings:  None
   Time:  5.40 seconds (prove: 0.00, print: 0.00, other: 5.40)
   "/home/camm/acl2-2.9/books/meta/meta.lisp"
   [SGC for 26 FIXNUM pages..(6943 writable)..(T=330).GC finished]
   Loading /home/camm/acl2-2.9/books/data-structures/utilities.o
    start address (dynamic) 0x20000000007d1ef0 Finished loading 
/home/camm/acl2-2.9/books/data-structures/utilities.o
   Loading /home/camm/acl2-2.9/books/ihs/ihs-init.o
    start address (dynamic) 0x20000000007d2160 Finished loading 
/home/camm/acl2-2.9/books/ihs/ihs-init.o
   Loading /home/camm/acl2-2.9/books/ihs/ihs-theories.o
    start address (dynamic) 0x20000000007d21b0 Finished loading 
/home/camm/acl2-2.9/books/ihs/ihs-theories.o
   [SGC for 26 FIXNUM pages..(6944 writable)..(T=336).GC finished]
   Loading /home/camm/acl2-2.9/books/ihs/logops-definitions.o
    start address (dynamic) 0x20000000007d2980 Finished loading 
/home/camm/acl2-2.9/books/ihs/logops-definitions.o
   [SGC for 2069 CONS pages..(8133 writable)..(T=582).GC finished]
   Loading /home/camm/acl2-2.9/books/ihs/logops-lemmas.o
    start address (dynamic) 0x20000000007d2a90 Finished loading 
/home/camm/acl2-2.9/books/ihs/logops-lemmas.o

   Summary
   Form:  ( INCLUDE-BOOK "../../../ihs/logops-lemmas" ...)
   Rules: NIL
   Warnings:  None
   Time:  45.35 seconds (prove: 0.00, print: 0.07, other: 45.28)
   "/home/camm/acl2-2.9/books/ihs/logops-lemmas.lisp"
   NIL

   Summary
   Form:  (IN-THEORY (SET-DIFFERENCE-THEORIES ...))
   Rules: NIL
   Warnings:  None
   Time:  0.27 seconds (prove: 0.00, print: 0.00, other: 0.27)
   2663
   2

   Summary
   Form:  ( DEFSTOBJ ST ...)
   Rules: NIL
   Warnings:  None
   Time:  1.63 seconds (prove: 0.00, print: 0.00, other: 1.63)
   ST

   Summary
   Form:  ( DEFMACRO PROGCLOC ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   PROGCLOC

   Summary
   Form:  ( DEFMACRO MEMLOC ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MEMLOC

   Summary
   Form:  ( DEFMACRO DTOSLOC ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   DTOSLOC

   Summary
   Form:  ( DEFMACRO CTOSLOC ...)
   Rules: NIL
   Warnings:  None
   Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
   CTOSLOC

   Summary
   Form:  ( DEFTHM THE-ERROR-NOOP ...)
   Rules: ((:DEFINITION THE-ERROR)
           (:REWRITE CDR-CONS))
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   THE-ERROR-NOOP

   Summary
   Form:  ( DEFTHM NTH-UPDATE-NTH-CONST ...)
   Rules: ((:DEFINITION NFIX)
           (:EXECUTABLE-COUNTERPART IF)
           (:EXECUTABLE-COUNTERPART SYNP)
           (:FAKE-RUNE-FOR-TYPE-SET NIL)
           (:REWRITE NTH-UPDATE-NTH))
   Warnings:  None
   Time:  0.21 seconds (prove: 0.15, print: 0.00, other: 0.06)
   NTH-UPDATE-NTH-CONST

   Summary
   Form:  (IN-THEORY (DISABLE ...))
   Rules: NIL
   Warnings:  None
   Time:  0.29 seconds (prove: 0.00, print: 0.00, other: 0.29)
   2708

   Summary
   Form:  ( DEFMACRO INT32 ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   INT32

   Summary
   Form:  ( DEFMACRO NAT10 ...)
   Rules: NIL
   Warnings:  None
   Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
   NAT10

   Summary
   Form:  ( DEFMACRO MAX_INT<32> ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MAX_INT<32>

   Summary
   Form:  ( DEFMACRO MIN_INT<32> ...)
   Rules: NIL
   Warnings:  None
   Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
   MIN_INT<32>

   Summary
   Form:  ( DEFMACRO MIN_INT<32>+1 ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MIN_INT<32>+1

   Summary
   Form:  ( DEFMACRO MAX_NAT<10> ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MAX_NAT<10>

   Summary
   Form:  ( DEFMACRO MAX_NAT-1<10> ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MAX_NAT-1<10>

   Summary
   Form:  ( DEFMACRO FIX10 ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   FIX10

   Summary
   Form:  ( DEFMACRO MAX<32> ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   MAX<32>

   Summary
   Form:  ( DEFMACRO |+<32>| ...)
   Rules: NIL
   Warnings:  None
   Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
   |+<32>|

   Summary
   Form:  ( DEFUN PLUS<32> ...)
   Rules: ((:DEFINITION FIX)
           (:DEFINITION INTEGER-RANGE-P)
           (:DEFINITION NOT)
           (:DEFINITION SIGNED-BYTE-P)
           (:DEFINITION SYNP)
           (:EXECUTABLE-COUNTERPART <)
           (:EXECUTABLE-COUNTERPART BINARY-+)
           (:EXECUTABLE-COUNTERPART EXPT)
           (:EXECUTABLE-COUNTERPART INTEGERP)
           (:EXECUTABLE-COUNTERPART UNARY--)
           (:FAKE-RUNE-FOR-LINEAR NIL)
           (:FAKE-RUNE-FOR-TYPE-SET NIL)
           (:FORWARD-CHAINING SIGNED-BYTE-P-FORWARD)
           (:META CANCEL_PLUS-LESSP-CORRECT)
           (:REWRITE <-+-NEGATIVE-0-1)
           (:REWRITE ASSOCIATIVITY-OF-+)
           (:REWRITE COMMUTATIVITY-2-OF-+)
           (:REWRITE COMMUTATIVITY-OF-+)
           (:REWRITE FOLD-CONSTS-IN-+)
           (:REWRITE UNICITY-OF-0)
           (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
   Warnings:  None
   Time:  4.00 seconds (prove: 3.12, print: 0.01, other: 0.87)
   PLUS<32>

   Summary
   Form:  ( DEFUN |+BV32| ...)
   Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
           (:FORWARD-CHAINING SIGNED-BYTE-P-FORWARD)
           (:TYPE-PRESCRIPTION LOGEXT-TYPE)
           (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
   Warnings:  None
   Time:  0.13 seconds (prove: 0.00, print: 0.00, other: 0.13)
   |+BV32|

   Summary
   Form:  ( DEFTHM PLUS<32>-WORKS ...)
   Rules: ((:DEFINITION |+BV32|)
           (:DEFINITION FIX)
           (:DEFINITION HIDE)
           (:DEFINITION INTEGER-RANGE-P)
           (:DEFINITION NOT)
           (:DEFINITION PLUS<32>)
           (:DEFINITION SIGNED-BYTE-P)
           (:DEFINITION SYNP)
           (:EXECUTABLE-COUNTERPART <)
           (:EXECUTABLE-COUNTERPART BINARY-+)
           (:EXECUTABLE-COUNTERPART EQUAL)
           (:EXECUTABLE-COUNTERPART EXPT)
           (:EXECUTABLE-COUNTERPART FIX)
           (:EXECUTABLE-COUNTERPART INTEGERP)
           (:EXECUTABLE-COUNTERPART LOGEXT)
           (:EXECUTABLE-COUNTERPART UNARY--)
           (:FAKE-RUNE-FOR-LINEAR NIL)
           (:FAKE-RUNE-FOR-TYPE-SET NIL)
           (:LINEAR LOGEXT-BOUNDS)
           (:META CANCEL_PLUS-EQUAL-CORRECT)
           (:REWRITE <-+-NEGATIVE-0-1)
           (:REWRITE ASSOCIATIVITY-OF-+)
           (:REWRITE COMMUTATIVITY-2-OF-+)
           (:REWRITE COMMUTATIVITY-OF-+)
           (:REWRITE FOLD-CONSTS-IN-+)
           (:REWRITE LOGEXT-IDENTITY)
           (:REWRITE RIGHT-CANCELLATION-FOR-+)
           (:REWRITE UNICITY-OF-0)
           (:TYPE-PRESCRIPTION LOGEXT-TYPE))
   Warnings:  None
   Time:  3.44 seconds (prove: 3.14, print: 0.00, other: 0.30)

   ******** FAILED ********  See :DOC failure  ******** FAILED ********

   Summary
   Form:  (CERTIFY-BOOK "tiny" ...)
   Rules: NIL
   Warnings:  None
   Time:  83.61 seconds (prove: 6.41, print: 0.09, other: 77.11)

   ******** FAILED ********  See :DOC failure  ******** FAILED ********
   ACL2 !>
   Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

   ACL2>
   =============================================================================
   workshops/1999/simulator/exercises.out
   =============================================================================
   GCL (GNU Common Lisp)  2.6.5 CLtL1    Sep  3 2004 20:49:20
   Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
   Binary License:  GPL due to GPL'ed components: (READLINE 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.

    ACL2 Version 2.9 built October 22, 2004  20:52:30.
    Copyright (C) 2004  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*
                         /usr/share/acl2-2.9/).
    See the documentation topic note-2-9 for recent changes.

    NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
    look under the ACL2 source directory in interface/emacs/README.doc; 
    and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
    command loop.   Look in the ACL2 documentation under PROOF-TREE.

   ACL2 Version 2.9.  Level 1.  Cbd 
   "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
   Type :help for help.
   Type (good-bye) to quit completely out of ACL2.

   ACL2 !>
   Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
   ACL2>
   #<"ACL2" package>

   ACL2>
   ACL2 Version 2.9.  Level 1.  Cbd 
   "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
   Type :help for help.
   Type (good-bye) to quit completely out of ACL2.

   ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
   ACL2 !>

   ACL2 Error in ( INCLUDE-BOOK "tiny" ...):  There is no certificate
   on file for "/home/camm/acl2-2.9/books/workshops/1999/simulator/tiny.lisp".


   Summary
   Form:  ( INCLUDE-BOOK "tiny" ...)
   Rules: NIL
   Warnings:  None
   Time:  0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)

   ******** FAILED ********  See :DOC failure  ******** FAILED ********

   Summary
   Form:  (CERTIFY-BOOK "exercises" ...)
   Rules: NIL
   Warnings:  None
   Time:  0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)

   ******** FAILED ********  See :DOC failure  ******** FAILED ********
   ACL2 !>
   Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

   ACL2>
   =============================================================================
   Take care,
   -- 
   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]