[Top][All Lists]
[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
- [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/25
- [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/25
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries,
Matt Kaufmann <=
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28