Re: [Gcl-devel] Re: ACL2 binaries

[Camm Maguire]

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