[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: ACL2 binaries
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Re: ACL2 binaries |
|
Date: |
28 Oct 2004 13:06:44 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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
- [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, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries,
Camm Maguire <=
- 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