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 13:09:42 -0500

Thanks.  Well, at this point I have no theory for why the proof failed.  We
tested this in quite a few Lisps (GCL, Allegro, CLISP, CMUCL, Lispworks,
OpenMCL) on Linux, Sun/Solaris, MacOS X, and Windows (though the workshops
books were only tested with one Lisp per platform other than Linux).  So I'd
first like to rule out the possibility of an "administrative" problem.

So the first step would be to tar up books/workshops/1999/simulator/ and send
it to me, so that I can make sure it agrees with what we distributed with ACL2
2.9.  Would you mind doing that?

Might it help if I try to get an account on Warren Hunt's ia64 machine at UT?
Specifically, is the ACL2 built there equivalent somehow to the one you're
using?

Thanks --
-- Matt
   Cc: address@hidden, address@hidden, address@hidden,
           address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 28 Oct 2004 13:06:44 -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, and thanks as always!

   Matt Kaufmann <address@hidden> writes:

   > 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

                    ^^^^^^^^^^^

   This works.

   > 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)))))
   > 

   Here is the output on ia64:
   =============================================================================
   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 !>(rebuild "tiny.lisp" 'plus<32>-works)

   ACL2 loading "tiny.lisp".
    "ACL2"
   [SGC for 243 CONS pages..(5727 writable)..(T=93).GC finished]
   [SGC for 243 CONS pages..(5729 writable)..(T=90).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..(6712 writable)..(T=266).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
    "/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..(6754 writable)..(T=285).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
    "/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..(6945 writable)..(T=317).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
    "/home/camm/acl2-2.9/books/meta/meta.lisp"
   [SGC for 26 FIXNUM pages..(6946 writable)..(T=328).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..(6947 writable)..(T=337).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..(8135 writable)..(T=576).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
    "/home/camm/acl2-2.9/books/ihs/logops-lemmas.lisp"
    NIL
    2663
    2
    ST
    PROGCLOC
    MEMLOC
    DTOSLOC
    CTOSLOC

   ACL2 Warning [Non-rec] in ( DEFTHM THE-ERROR-NOOP ...):  The :REWRITE
   rule generated from THE-ERROR-NOOP will be triggered only by terms
   containing the non-recursive function symbol THE-ERROR.  Unless this
   function is disabled, THE-ERROR-NOOP is unlikely ever to be used.


   ACL2 Warning [Subsume] in ( DEFTHM THE-ERROR-NOOP ...):  The newly
   proposed :REWRITE rule THE-ERROR-NOOP probably subsumes the previously
   added :REWRITE rule THE-ERROR, in the sense that THE-ERROR-NOOP will
   now probably be applied whenever the old rule would have been.


   ACL2 Warning [Subsume] in ( DEFTHM THE-ERROR-NOOP ...):  The previously
   added rule THE-ERROR subsumes the newly proposed :REWRITE rule THE-
   ERROR-NOOP, in the sense that the old rule rewrites a more general
   target.  Because the new rule will be tried first, it may nonetheless
   find application.

    THE-ERROR-NOOP

   ACL2 Warning [Subsume] in ( DEFTHM NTH-UPDATE-NTH-CONST ...):  The
   previously added rule NTH-UPDATE-NTH subsumes the newly proposed :REWRITE
   rule NTH-UPDATE-NTH-CONST, in the sense that the old rule rewrites
   a more general target.  Because the new rule will be tried first, it
   may nonetheless find application.

    NTH-UPDATE-NTH-CONST
    2708
    INT32
    NAT10
    MAX_INT<32>
    MIN_INT<32>
    MIN_INT<32>+1
    MAX_NAT<10>
    MAX_NAT-1<10>
    FIX10
    MAX<32>
    |+<32>|
    PLUS<32>
    |+BV32|

   ACL2 Warning [Non-rec] in ( DEFTHM PLUS<32>-WORKS ...):  The :REWRITE
   rule generated from PLUS<32>-WORKS will be triggered only by terms
   containing the non-recursive function symbol PLUS<32>.  Unless this
   function is disabled, PLUS<32>-WORKS is unlikely ever to be used.

    PLUS<32>-WORKS

   Finished loading "tiny.lisp".
    T
   ACL2 !>:u

    V       26:x(DEFUN |+BV32| (X Y) ...)
   ACL2 !>(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)))))

   ACL2 Warning [Non-rec] in ( DEFTHM PLUS<32>-WORKS ...):  The :REWRITE
   rule generated from PLUS<32>-WORKS will be triggered only by terms
   containing the non-recursive function symbol PLUS<32>.  Unless this
   function is disabled, PLUS<32>-WORKS is unlikely ever to be used.


   [Note:  A hint was supplied for our processing of the goal above. 
   Thanks!]

   We now augment the goal above by adding the hypotheses indicated by
   the :USE hint.  These hypotheses can be derived from LOGEXT-+-LOGEXT
   via instantiation.  The augmented goal is shown below.

   Goal'
   (IMPLIES
        (AND (IMPLIES (AND (INTEGERP (+ A B))
                           (INTEGERP (- (EXPT 2 32))))
                      (EQUAL (LOGEXT 32
                                     (+ (+ A B) (LOGEXT 32 (- (EXPT 2 32)))))
                             (LOGEXT 32 (+ (+ A B) (- (EXPT 2 32))))))
             (IMPLIES (AND (INTEGERP (+ A B))
                           (INTEGERP (EXPT 2 32)))
                      (EQUAL (LOGEXT 32 (+ (+ A B) (LOGEXT 32 (EXPT 2 32))))
                             (LOGEXT 32 (+ (+ A B) (EXPT 2 32))))))
        (IMPLIES (AND (SIGNED-BYTE-P 32 A)
                      (SIGNED-BYTE-P 32 B))
                 (EQUAL (PLUS<32> A B) (|+BV32| A B)))).

   By the simple :definitions |+BV32|, INTEGER-RANGE-P and SIGNED-BYTE-
   P, the :executable-counterparts of EXPT, INTEGERP, LOGEXT and UNARY-
   - and the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the conjecture
   to

   Goal''
   (IMPLIES (AND (IMPLIES (INTEGERP (+ A B))
                          (EQUAL (LOGEXT 32 (+ A B 0))
                                 (LOGEXT 32 (+ A B -4294967296))))
                 (IMPLIES (INTEGERP (+ A B))
                          (EQUAL (LOGEXT 32 (+ A B 0))
                                 (LOGEXT 32 (+ A B 4294967296))))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648))
            (EQUAL (PLUS<32> A B)
                   (LOGEXT 32 (+ A B)))).

   This simplifies, using the :definitions FIX, INTEGER-RANGE-P, PLUS<32>,
   SIGNED-BYTE-P and SYNP, the :executable-counterparts of <, BINARY-+,
   EXPT, INTEGERP and UNARY--, linear arithmetic, primitive type reasoning
   and the :rewrite rules <-+-NEGATIVE-0-1, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-
   OF-+, FOLD-CONSTS-IN-+, LOGEXT-IDENTITY and UNICITY-OF-0, to the following
   six conjectures.

   Subgoal 6
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (< (+ A B) 2147483648))
            (EQUAL (+ A B) (LOGEXT 32 (+ A B)))).

   But simplification reduces this to T, using the :definitions INTEGER-
   RANGE-P and SIGNED-BYTE-P, the :executable-counterparts of <, BINARY-
   +, EQUAL, EXPT, FIX, INTEGERP and UNARY--, linear arithmetic, primitive
   type reasoning, the :linear rule LOGEXT-BOUNDS, the :meta rule CANCEL_-
   PLUS-EQUAL-CORRECT and the :rewrite rule LOGEXT-IDENTITY.

   Subgoal 5
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B)
                 (<= 2147483648 (+ A B)))
            (EQUAL (+ -18446744073709551616 A B)
                   (LOGEXT 32 (+ A B)))).

   We now use the first hypothesis by substituting (+ -4294967296 A B)
   for (LOGEXT 32 (+ A B)) and hiding the hypothesis.  This produces

   Subgoal 5'
   (IMPLIES (AND (HIDE (EQUAL (LOGEXT 32 (+ A B))
                              (+ -4294967296 A B)))
                 (EQUAL (+ -4294967296 A B)
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B)
                 (<= 2147483648 (+ A B)))
            (EQUAL (+ -18446744073709551616 A B)
                   (+ -4294967296 A B))).

   By the :executable-counterparts of EQUAL and FIX and the simple :rewrite
   rule RIGHT-CANCELLATION-FOR-+ we reduce the conjecture to

   Subgoal 5''
   (IMPLIES (AND (HIDE (EQUAL (LOGEXT 32 (+ A B))
                              (+ -4294967296 A B)))
                 (EQUAL (+ -4294967296 A B)
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   We remove HIDE from the first hypothesis, which was used heuristically
   to transform Subgoal 5 by substituting into the rest of that goal.
   This produces

   Subgoal 5'''
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 A B))
                 (EQUAL (+ -4294967296 A B)
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   This simplifies, using primitive type reasoning, to

   Subgoal 5'4'
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   We now use the second hypothesis by substituting 
   (LOGEXT 32 (+ 4294967296 A B)) for (LOGEXT 32 (+ A B)) and hiding the
   hypothesis.  This produces

   Subgoal 5'5'
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ 4294967296 A B))
                        (+ -4294967296 A B))
                 (HIDE (EQUAL (LOGEXT 32 (+ A B))
                              (LOGEXT 32 (+ 4294967296 A B))))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   We remove HIDE from the second hypothesis, which was used heuristically
   to transform Subgoal 5'4' by substituting into the rest of that goal.
   This produces

   Subgoal 5'6'
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ 4294967296 A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   This simplifies, using linear arithmetic, primitive type reasoning
   and the :type-prescription rule LOGEXT-TYPE, to

   Subgoal 5'7'
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 B A))
                 (EQUAL (LOGEXT 32 (+ 4294967296 A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   This simplifies, using primitive type reasoning and the :rewrite rule
   COMMUTATIVITY-OF-+, to

   Subgoal 5'8'
   (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
                        (+ -4294967296 A B))
                 (EQUAL (LOGEXT 32 (+ A B))
                        (LOGEXT 32 (+ 4294967296 A B)))
                 (INTEGERP A)
                 (<= -2147483648 A)
                 (< A 2147483648)
                 (INTEGERP B)
                 (<= -2147483648 B)
                 (< B 2147483648)
                 (<= 0 A)
                 (<= 0 B))
            (< (+ A B) 2147483648)).

   Normally we would attempt to prove this formula by induction.  However,
   we prefer in this instance to focus on the original input conjecture
   rather than this simplified special case.  We therefore abandon our
   previous work on this conjecture and reassign the name *1 to the original
   conjecture.  (See :DOC otf-flg.)  [Note:  Thanks again for the hint.]

   No induction schemes are suggested by *1.  Consequently, the proof
   attempt has failed.

   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:  Non-rec
   Time:  3.99 seconds (prove: 3.19, print: 0.45, other: 0.35)

   ******** FAILED ********  See :DOC failure  ******** FAILED ********
   ACL2 !>
   =============================================================================

   > 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
   > 
   > 
   > 

   -- 
   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]