[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: GCL 2.6.7 problem
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: GCL 2.6.7 problem |
Date: |
03 Jul 2007 11:12:36 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings, and thanks so much for the report!
I can't seem to reproduce on elgin. Here is my transcript. Please
advise.
Take care,
=============================================================================
elgin.cs.utexas.edu$ cp /projects/acl2/gcl-issue.tgz .
elgin.cs.utexas.edu$ tar zxf gcl-issue.tgz
elgin.cs.utexas.edu$ ls -lrt |tail
drwxr-xr-x 4 camm hons 4096 Sep 12 2006 etc
drwxr-sr-x 7 camm hons 4096 Oct 20 2006 test
-rw-r--r-- 1 camm hons 144048 Dec 20 2006 gcl.cvs.diff
-rw-r--r-- 1 camm hons 4397093 Jan 23 13:31 camm.tgz
drwxr-sr-x 4 camm hons 4096 Jan 23 16:46 camm
drwxr-sr-x 3 camm hons 4096 May 10 10:08 l
-rw------- 1 camm hons 1020389 May 31 20:05 mailbox
drwxr-xr-x 2 camm hons 4096 Jun 13 18:25 bin
drwxr-sr-x 4 camm hons 4096 Jun 30 08:25 gcl-issue
-rw-r--r-- 1 camm hons 2544747 Jul 2 16:25 gcl-issue.tgz
elgin.cs.utexas.edu$ cd gcl-issue
elgin.cs.utexas.edu$ ls
GNUmakefile defpkgs.lisp openmcl-acl2-trace.lisp
LICENSE defthm.lisp other-events.lisp
Makefile defuns.lisp other-processes.lisp
acl2-check.lisp email.txt proof-checker-a.lisp
acl2-fns.lisp history-management.lisp proof-checker-b.lisp
acl2-init.lisp hons-raw.lisp proof-checker-pkg.lisp
acl2.lisp hons.lisp prove.lisp
akcl-acl2-trace.lisp induct.lisp rewrite.lisp
all-files-nonstd.txt init.lisp save-gprof.lsp
all-files-workshops.txt interface-raw.lisp saved
all-files.txt ld.lisp simplify.lisp
allegro-acl2-trace.lisp linear-a.lisp sum-list-example.lisp
axioms.lisp linear-b.lisp translate.lisp
basis.lisp mcl-acl2-startup.lisp tutorial.lisp
bdd.lisp my-fast-gcl type-set-a.lisp
books non-linear.lisp type-set-b.lisp
build-allegro-exe.cl notes.txt
elgin.cs.utexas.edu$ cat notex.txt
cat: notex.txt: No such file or directory
elgin.cs.utexas.edu$ cat notes.txt
I've placed the email on this problem in file email.txt.
Here is how to re-create a problem I have with GCL 2.6.7 smashing a property
list.
First, build ACL2 in this directory. You'll need to edit ./my-fast-gcl if you
are not on the UT Linux filesystem.
==============================
(time nice make LISP=./my-fast-gcl) >& make.log&
make clean-books ### not necessary the first time
make regression
==============================
That should fail, like this:
ls: b-ops-aux-def.cert: No such file or directory
**CERTIFICATION FAILED** for
/projects/acl2/gcl-issue/books/workshops/1999/pipeline/b-ops-aux-def.lisp
Then do the following.
==============================
cd books/workshops/1999/pipeline/
../../../../saved_acl2
; Optional:
:q
(si::use-fast-links nil)
(lp)
; Required:
(SET-DEBUGGER-ENABLE T) ; allow debug
(include-book "../../../data-structures/array1")
(include-book "../../../arithmetic/rationals")
==============================
; From here, there are probably many ways to cause and then see the corruption
; of (symbol-plist 'binary-logand).
; One way is this, which may give a fatal error:
(include-book "ihs") ; fatal error
; But instead, you could just do the following, which is just part of what the
; above include-book form does, and you may find that (symbol-plist
; 'binary-logand) is already corrupted.
(include-book "../../../ihs/ihs-definitions")
elgin.cs.utexas.edu$ ls saved_acl2
ls: saved_acl2: No such file or directory
elgin.cs.utexas.edu$ cat my-fast-gcl
#!/bin/sh
/p/bin/gcl-2.6.7 -eval "(defparameter user::*fast-acl2-gcl-build* t)" $*
elgin.cs.utexas.edu$ (time nice make LISP=./my-fast-gcl) > make.log 2>&1 &
[1] 10037
elgin.cs.utexas.edu$ while tail -n 5 mail.log ; do sleep 30 ; done
tail: cannot open `mail.log' for reading: No such file or directory
elgin.cs.utexas.edu$ while tail -n 5 make.log ; do sleep 30 ; done
Finished loading translate.lisp
Compiling translate.lisp.
[GC for 398 ARRAY pages..(T=2).GC finished]
End of Pass 1.
End of Pass 2.
Finished loading history-management.lisp
Compiling history-management.lisp.
[GC for 4494 CONS pages..(T=5).GC finished]
End of Pass 1.
End of Pass 2.
Finished loading defthm.lisp
[GC for 10485 RELOCATABLE-BLOCKS pages..(T=5).GC finished]
Compiling defthm.lisp.
End of Pass 1.
End of Pass 2.
Finished loading other-events.lisp
Compiling other-events.lisp.
[GC for 6301 CONS pages..(T=8).GC finished]
End of Pass 1.
End of Pass 2.
[GC for 1931 CONS pages..(T=4).GC finished]
[GC for 1941 CONS pages..(T=4).GC finished]
[GC for 1951 CONS pages..(T=5).GC finished]
[GC for 1961 CONS pages..(T=5).GC finished]
[GC for 1971 CONS pages..(T=4).GC finished]
[GC for 3021 CONS pages..(T=7).GC finished]
[GC for 3031 CONS pages..(T=7).GC finished]
[GC for 3041 CONS pages..(T=7).GC finished]
[GC for 3051 CONS pages..(T=6).GC finished]
[GC for 3061 CONS pages..(T=7).GC finished]
INFO-FOR-LINEAR-LEMMAS
INFO-FOR-ELIMINATE-DESTRUCTORS-RULE
INFO-FOR-CONGRUENCES
INFO-FOR-COARSENINGS
INFO-FOR-FORWARD-CHAINING-RULES
QUERY-ON-EXIT
REPLAY-QUERY
[GC for 5871 CONS pages..(T=13).GC finished]
[GC for 5881 CONS pages..(T=13).GC finished]
[GC for 5891 CONS pages..
ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)).
[GC for 7411 CONS pages..(T=16).GC finished]
[GC for 7421 CONS pages..(T=16).GC finished]
[GC for 7431 CONS pages..[GC for 2147 CONTIGUOUS-BLOCKS pages..(T=19).GC
finished]
[GC for 2147 CONTIGUOUS-BLOCKS pages..(T=18).GC finished]
[GC for 2147 CONTIGUOUS-BLOCKS pages..(T=18).GC finished]
[GC for 2147 CONTIGUOUS-BLOCKS pages..(T=18).GC finished]
[GC for 2147 CONTIGUOUS-BLOCKS pages..[1]+ Done ( time nice
make LISP=./my-fast-gcl ) > make.log 2>&1
make[1]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue'
real 4m54.504s
user 4m47.618s
sys 0m5.656s
make[1]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue'
real 4m54.504s
user 4m47.618s
sys 0m5.656s
elgin.cs.utexas.edu$ elgin.cs.utexas.edu$ make regression
uname -a
Linux elgin.cs.utexas.edu 2.6.19.1 #2 SMP Wed Jan 3 13:26:45 CST 2007 i686
GNU/Linux
cd books ; make -i all-plus
make[1]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books'
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/cowles'
Using ACL2=../../saved_acl2
make -s -f Makefile acl2-agp.cert acl2-asg.cert acl2-crg.cert
INHIBIT='(assign inhibit-output-lst (list (quote prove) (quote proof-tree)
(quote warning) (quote observation) (quote event) (quote expansion)))'
ACL2='../../saved_acl2'
make[3]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/cowles'
Making /u/camm/gcl-issue/books/cowles/acl2-asg.cert on Mon Jul 2 16:35:42 CDT
2007
-rw-r--r-- 1 camm hons 369 Jul 2 16:35 acl2-asg.cert
Making /u/camm/gcl-issue/books/cowles/acl2-agp.cert on Mon Jul 2 16:35:43 CDT
2007
-rw-r--r-- 1 camm hons 638 Jul 2 16:35 acl2-agp.cert
Making /u/camm/gcl-issue/books/cowles/acl2-crg.cert on Mon Jul 2 16:35:44 CDT
2007
-rw-r--r-- 1 camm hons 778 Jul 2 16:35 acl2-crg.cert
make[3]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/cowles'
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/cowles'
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
Using ACL2=../../saved_acl2
make -s -f Makefile abs.cert binomial.cert equalities.cert factorial.cert
idiv.cert inequalities.cert mod-gcd.cert natp-posp.cert rational-listp.cert
rationals.cert sumlist.cert top.cert INHIBIT='(assign inhibit-output-lst
(list (quote prove) (quote proof-tree) (quote warning) (quote observation)
(quote event) (quote expansion)))' ACL2='../../saved_acl2'
make[3]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
Making /u/camm/gcl-issue/books/arithmetic/equalities.cert on Mon Jul 2
16:35:44 CDT 2007
-rw-r--r-- 1 camm hons 1067 Jul 2 16:35 equalities.cert
Making /u/camm/gcl-issue/books/arithmetic/rational-listp.cert on Mon Jul 2
16:35:47 CDT 2007
-rw-r--r-- 1 camm hons 262 Jul 2 16:35 rational-listp.cert
Making /u/camm/gcl-issue/books/arithmetic/inequalities.cert on Mon Jul 2
16:35:47 CDT 2007
-rw-r--r-- 1 camm hons 836 Jul 2 16:35 inequalities.cert
Making /u/camm/gcl-issue/books/arithmetic/natp-posp.cert on Mon Jul 2 16:35:48
CDT 2007
-rw-r--r-- 1 camm hons 981 Jul 2 16:35 natp-posp.cert
Making /u/camm/gcl-issue/books/arithmetic/mod-gcd.cert on Mon Jul 2 16:35:49
CDT 2007
-rw-r--r-- 1 camm hons 1841 Jul 2 16:35 mod-gcd.cert
Making /u/camm/gcl-issue/books/arithmetic/rationals.cert on Mon Jul 2 16:35:51
CDT 2007
-rw-r--r-- 1 camm hons 1905 Jul 2 16:35 rationals.cert
Making /u/camm/gcl-issue/books/arithmetic/top.cert on Mon Jul 2 16:35:52 CDT
2007
-rw-r--r-- 1 camm hons 2341 Jul 2 16:35 top.cert
Making /u/camm/gcl-issue/books/arithmetic/abs.cert on Mon Jul 2 16:35:53 CDT
2007
-rw-r--r-- 1 camm hons 2470 Jul 2 16:35 abs.cert
Making /u/camm/gcl-issue/books/arithmetic/factorial.cert on Mon Jul 2 16:35:54
CDT 2007
-rw-r--r-- 1 camm hons 248 Jul 2 16:35 factorial.cert
Making /u/camm/gcl-issue/books/arithmetic/sumlist.cert on Mon Jul 2 16:35:54
CDT 2007
-rw-r--r-- 1 camm hons 240 Jul 2 16:35 sumlist.cert
Making /u/camm/gcl-issue/books/arithmetic/binomial.cert on Mon Jul 2 16:35:55
CDT 2007
-rw-r--r-- 1 camm hons 2772 Jul 2 16:35 binomial.cert
Making /u/camm/gcl-issue/books/arithmetic/idiv.cert on Mon Jul 2 16:35:57 CDT
2007
-rw-r--r-- 1 camm hons 2472 Jul 2 16:35 idiv.cert
make[3]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/meta'
Using ACL2=../../saved_acl2
make -s -f Makefile meta-plus-equal.cert meta-plus-lessp.cert
meta-times-equal.cert meta.cert pseudo-termp-lemmas.cert term-defuns.cert
term-lemmas.cert INHIBIT='(assign inhibit-output-lst (list (quote prove) (quote
proof-tree) (quote warning) (quote observation) (quote event) (quote
expansion)))' ACL2='../../saved_acl2'
make[3]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/meta'
Making /u/camm/gcl-issue/books/meta/term-defuns.cert on Mon Jul 2 16:35:58 CDT
2007
-rw-r--r-- 1 camm hons 247 Jul 2 16:35 term-defuns.cert
Making /u/camm/gcl-issue/books/meta/term-lemmas.cert on Mon Jul 2 16:35:59 CDT
2007
-rw-r--r-- 1 camm hons 393 Jul 2 16:36 term-lemmas.cert
Making /u/camm/gcl-issue/books/meta/meta-plus-equal.cert on Mon Jul 2 16:36:00
CDT 2007
-rw-r--r-- 1 camm hons 561 Jul 2 16:36 meta-plus-equal.cert
Making /u/camm/gcl-issue/books/meta/meta-plus-lessp.cert on Mon Jul 2 16:36:02
CDT 2007
-rw-r--r-- 1 camm hons 561 Jul 2 16:36 meta-plus-lessp.cert
Making /u/camm/gcl-issue/books/meta/meta-times-equal.cert on Mon Jul 2
16:36:03 CDT 2007
-rw-r--r-- 1 camm hons 1799 Jul 2 16:36 meta-times-equal.cert
Making /u/camm/gcl-issue/books/meta/meta.cert on Mon Jul 2 16:36:07 CDT 2007
-rw-r--r-- 1 camm hons 1632 Jul 2 16:36 meta.cert
Making /u/camm/gcl-issue/books/meta/pseudo-termp-lemmas.cert on Mon Jul 2
16:36:07 CDT 2007
-rw-r--r-- 1 camm hons 564 Jul 2 16:36 pseudo-termp-lemmas.cert
make[3]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/meta'
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/meta'
Using ACL2=
cd arithmetic ; make top-with-meta.cert
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
Making /u/camm/gcl-issue/books/arithmetic/top-with-meta.cert on Mon Jul 2
16:36:11 CDT 2007
-rw-r--r-- 1 camm hons 3586 Jul 2 16:36 top-with-meta.cert
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic'
make[2]: Entering directory
`/v/filer4b/v19q001/camm/gcl-issue/books/data-structures'
Using ACL2=../../saved_acl2
make -s -f Makefile array1.cert list-defuns.cert list-defthms.cert
utilities.cert deflist.cert list-theory.cert set-defuns.cert
set-defthms.cert set-theory.cert alist-defuns.cert alist-defthms.cert
defalist.cert alist-theory.cert structures.cert number-list-defuns.cert
number-list-defthms.cert number-list-theory.cert INHIBIT='(assign
inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning)
(quote observation) (quote event) (quote expansion)))' ACL2='../../saved_acl2'
make[3]: Entering directory
`/v/filer4b/v19q001/camm/gcl-issue/books/data-structures'
Making /u/camm/gcl-issue/books/data-structures/array1.cert on Mon Jul 2
16:36:12 CDT 2007
-rw-r--r-- 1 camm hons 244 Jul 2 16:36 array1.cert
Making /u/camm/gcl-issue/books/data-structures/list-defuns.cert on Mon Jul 2
16:36:14 CDT 2007
-rw-r--r-- 1 camm hons 258 Jul 2 16:36 list-defuns.cert
Making /u/camm/gcl-issue/books/data-structures/list-defthms.cert on Mon Jul 2
16:36:16 CDT 2007
-rw-r--r-- 1 camm hons 1654 Jul 2 16:36 list-defthms.cert
Making /u/camm/gcl-issue/books/data-structures/utilities.cert on Mon Jul 2
16:36:21 CDT 2007
-rw-r--r-- 1 camm hons 336 Jul 2 16:36 utilities.cert
Making /u/camm/gcl-issue/books/data-structures/deflist.cert on Mon Jul 2
16:36:24 CDT 2007
-rw-r--r-- 1 camm hons 2271 Jul 2 16:36 deflist.cert
Making /u/camm/gcl-issue/books/data-structures/list-theory.cert on Mon Jul 2
16:36:27 CDT 2007
-rw-r--r-- 1 camm hons 1664 Jul 2 16:36 list-theory.cert
Making /u/camm/gcl-issue/books/data-structures/set-defuns.cert on Mon Jul 2
16:36:29 CDT 2007
-rw-r--r-- 1 camm hons 255 Jul 2 16:36 set-defuns.cert
Making /u/camm/gcl-issue/books/data-structures/set-defthms.cert on Mon Jul 2
16:36:29 CDT 2007
-rw-r--r-- 1 camm hons 413 Jul 2 16:36 set-defthms.cert
Making /u/camm/gcl-issue/books/data-structures/set-theory.cert on Mon Jul 2
16:36:30 CDT 2007
-rw-r--r-- 1 camm hons 567 Jul 2 16:36 set-theory.cert
Making /u/camm/gcl-issue/books/data-structures/alist-defuns.cert on Mon Jul 2
16:36:31 CDT 2007
-rw-r--r-- 1 camm hons 261 Jul 2 16:36 alist-defuns.cert
Making /u/camm/gcl-issue/books/data-structures/alist-defthms.cert on Mon Jul 2
16:36:33 CDT 2007
-rw-r--r-- 1 camm hons 2140 Jul 2 16:36 alist-defthms.cert
Making /u/camm/gcl-issue/books/data-structures/defalist.cert on Mon Jul 2
16:36:36 CDT 2007
-rw-r--r-- 1 camm hons 801 Jul 2 16:36 defalist.cert
Making /u/camm/gcl-issue/books/data-structures/alist-theory.cert on Mon Jul 2
16:36:38 CDT 2007
-rw-r--r-- 1 camm hons 1988 Jul 2 16:36 alist-theory.cert
Making /u/camm/gcl-issue/books/data-structures/structures.cert on Mon Jul 2
16:36:40 CDT 2007
-rw-r--r-- 1 camm hons 1071 Jul 2 16:36 structures.cert
Making /u/camm/gcl-issue/books/data-structures/number-list-defuns.cert on Mon
Jul 2 16:36:47 CDT 2007
-rw-r--r-- 1 camm hons 437 Jul 2 16:36 number-list-defuns.cert
Making /u/camm/gcl-issue/books/data-structures/number-list-defthms.cert on Mon
Jul 2 16:36:48 CDT 2007
-rw-r--r-- 1 camm hons 1708 Jul 2 16:36 number-list-defthms.cert
Making /u/camm/gcl-issue/books/data-structures/number-list-theory.cert on Mon
Jul 2 16:36:49 CDT 2007
-rw-r--r-- 1 camm hons 1886 Jul 2 16:36 number-list-theory.cert
make[3]: Leaving directory
`/v/filer4b/v19q001/camm/gcl-issue/books/data-structures'
make[2]: Leaving directory
`/v/filer4b/v19q001/camm/gcl-issue/books/data-structures'
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/ihs'
Using ACL2=../../saved_acl2
make -s -f Makefile @logops.cert ihs-definitions.cert ihs-init.cert
ihs-lemmas.cert ihs-theories.cert logops-definitions.cert logops-lemmas.cert
math-lemmas.cert quotient-remainder-lemmas.cert INHIBIT='(assign
inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning)
(quote observation) (quote event) (quote expansion)))' ACL2='../../saved_acl2'
make[3]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/ihs'
Making /u/camm/gcl-issue/books/ihs/ihs-init.cert on Mon Jul 2 16:36:51 CDT 2007
-rw-r--r-- 1 camm hons 492 Jul 2 16:36 ihs-init.cert
Making /u/camm/gcl-issue/books/ihs/ihs-theories.cert on Mon Jul 2 16:36:52 CDT
2007
-rw-r--r-- 1 camm hons 555 Jul 2 16:36 ihs-theories.cert
Making /u/camm/gcl-issue/books/ihs/math-lemmas.cert on Mon Jul 2 16:36:53 CDT
2007
-rw-r--r-- 1 camm hons 2806 Jul 2 16:36 math-lemmas.cert
Making /u/camm/gcl-issue/books/ihs/quotient-remainder-lemmas.cert on Mon Jul 2
16:36:54 CDT 2007
-rw-r--r-- 1 camm hons 4208 Jul 2 16:37 quotient-remainder-lemmas.cert
Making /u/camm/gcl-issue/books/ihs/logops-definitions.cert on Mon Jul 2
16:37:03 CDT 2007
-rw-r--r-- 1 camm hons 5164 Jul 2 16:37 logops-definitions.cert
Making /u/camm/gcl-issue/books/ihs/ihs-definitions.cert on Mon Jul 2 16:37:08
CDT 2007
-rw-r--r-- 1 camm hons 4335 Jul 2 16:37 ihs-definitions.cert
Making /u/camm/gcl-issue/books/ihs/logops-lemmas.cert on Mon Jul 2 16:37:10
CDT 2007
-rw-r--r-- 1 camm hons 4524 Jul 2 16:37 logops-lemmas.cert
Making /u/camm/gcl-issue/books/ihs/ihs-lemmas.cert on Mon Jul 2 16:37:19 CDT
2007
ls: ihs-lemmas.cert: No such file or directory
**CERTIFICATION FAILED** for /u/camm/gcl-issue/books/ihs/ihs-lemmas.lisp
Making /u/camm/gcl-issue/books/ihs/@logops.cert on Mon Jul 2 16:37:21 CDT 2007
ls: @logops.cert: No such file or directory
**CERTIFICATION FAILED** for /u/camm/gcl-issue/books/ihs/@logops.lisp
make[3]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/ihs'
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/ihs'
make[2]: Entering directory `/v/filer4b/v19q001/camm/gcl-issue/books/workshops'
if [ -f 1999/Makefile ]; then \
cd 1999 ; make ; cd .. ; fi
make[3]: Entering directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999'
if [ -f calculus/Makefile ]; then \
cd calculus ; make ; cd .. ; fi
if [ -f compiler/Makefile ]; then \
cd compiler ; make ; cd .. ; fi
if [ -f de-hdl/Makefile ]; then \
cd de-hdl ; make ; cd .. ; fi
if [ -f embedded/Makefile ]; then \
cd embedded ; make ; cd .. ; fi
if [ -f graph/Makefile ]; then \
cd graph ; make ; cd .. ; fi
if [ -f knuth-91/Makefile ]; then \
cd knuth-91 ; make ; cd .. ; fi
if [ -f mu-calculus/Makefile ]; then \
cd mu-calculus ; make ; cd .. ; fi
if [ -f multiplier/Makefile ]; then \
cd multiplier ; make ; cd .. ; fi
if [ -f pipeline/Makefile ]; then \
cd pipeline ; make ; cd .. ; fi
make[4]: Entering directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline'
Using ACL2=../../../../saved_acl2
make -s -f Makefile b-ops-aux-def.cert ihs.cert trivia.cert INHIBIT='(assign
inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning)
(quote observation) (quote event) (quote expansion)))'
ACL2='../../../../saved_acl2'
make[5]: Entering directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline'
Making /u/camm/gcl-issue/books/workshops/1999/pipeline/trivia.cert on Mon Jul
2 16:37:22 CDT 2007
-rw-r--r-- 1 camm hons 2679 Jul 2 16:37 trivia.cert
Making
/u/camm/gcl-issue/books/workshops/1999/pipeline/../../../ihs/ihs-lemmas.cert on
Mon Jul 2 16:37:23 CDT 2007
ls: ../../../ihs/ihs-lemmas.cert: No such file or directory
**CERTIFICATION FAILED** for
/u/camm/gcl-issue/books/workshops/1999/pipeline/../../../ihs/ihs-lemmas.lisp
Making /u/camm/gcl-issue/books/workshops/1999/pipeline/ihs.cert on Mon Jul 2
16:37:24 CDT 2007
ls: ihs.cert: No such file or directory
**CERTIFICATION FAILED** for
/u/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp
Making /u/camm/gcl-issue/books/workshops/1999/pipeline/b-ops-aux-def.cert on
Mon Jul 2 16:37:25 CDT 2007
ls: b-ops-aux-def.cert: No such file or directory
**CERTIFICATION FAILED** for
/u/camm/gcl-issue/books/workshops/1999/pipeline/b-ops-aux-def.lisp
make[5]: Leaving directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline'
make[4]: Leaving directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline'
if [ -f simulator/Makefile ]; then \
cd simulator ; make ; cd .. ; fi
if [ -f ste/Makefile ]; then \
cd ste ; make ; cd .. ; fi
if [ -f vhdl/Makefile ]; then \
cd vhdl ; make ; cd .. ; fi
if [ -f ivy/Makefile ]; then \
cd ivy ; make ; cd .. ; fi
make[3]: Leaving directory
`/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999'
if [ -f 2000/Makefile ]; then \
cd 2000 ; make ; cd .. ; fi
if [ -f 2002/Makefile ]; then \
cd 2002 ; make ; cd .. ; fi
if [ -f 2003/Makefile ]; then \
cd 2003 ; make ; cd .. ; fi
if [ -f 2004/Makefile ]; then \
cd 2004 ; make ; cd .. ; fi
if [ -f 2006/Makefile ]; then \
cd 2006 ; make ; cd .. ; fi
make[2]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books/workshops'
make[1]: Leaving directory `/v/filer4b/v19q001/camm/gcl-issue/books'
elgin.cs.utexas.edu$ cd books/workshops/1999/pipeline/
elgin.cs.utexas.edu$ ../../../../saved_acl2
GCL (GNU Common Lisp) 2.6.7 CLtL1 Sep 15 2005 12:36:56
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License: GPL due to GPL'ed components: (BFD 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 3.2.1 built July 2, 2007 16:31:43.
Copyright (C) 2007 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*).
See the documentation topic note-3-2-1 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
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 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2> (si::use-fast-links nil)
NIL
ACL2>(lp)
ACL2 Version 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(SET-DEBUGGER-ENABLE T)
<state>
ACL2 !>(include-book "../../../data-structures/array1")
[SGC for 25 FIXNUM pages..(12615 writable)..(T=2).GC finished]
[SGC for 25 FIXNUM pages..(12615 writable)..(T=1).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
start address -T 0x8494000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
Summary
Form: ( INCLUDE-BOOK "../../../data-structures/array1" ...)
Rules: NIL
Warnings: None
Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
"/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.lisp"
ACL2 !>(include-book "../../../arithmetic/rationals")
[SGC for 555 CONS pages..(12985 writable)..(T=2).GC finished]
[SGC for 555 CONS pages..(12986 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
start address -T 0x8995ec0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
[SGC for 7 SYMBOL pages..(13331 writable)..(T=1).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
start address -T 0x894afc0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
start address -T 0x8424770 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
Summary
Form: ( INCLUDE-BOOK "../../../arithmetic/rationals" ...)
Rules: NIL
Warnings: None
Time: 0.23 seconds (prove: 0.00, print: 0.00, other: 0.23)
"/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.lisp"
ACL2 !>(symbol-plist 'binary-logand)
ACL2 Error in TOP-LEVEL: The symbol SYMBOL-PLIST (in package "COMMON-LISP")
has neither a function nor macro definition in ACL2. Moreover, this
symbol is in the main Lisp package; hence, you cannot define it in
ACL2, which is not Common Lisp.
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'binary-logand)
(COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T T) #:*CURRENT-ACL2-WORLD-KEY*
((COARSENINGS NIL)
(RUNIC-MAPPING-PAIRS
((1296 :DEFINITION BINARY-LOGAND)
(1297 :EXECUTABLE-COUNTERPART BINARY-LOGAND)
(1298 :TYPE-PRESCRIPTION BINARY-LOGAND)
(1299 :INDUCTION BINARY-LOGAND)))
(DEF-BODIES
(((1296 NIL IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I)))))
(BINARY-LOGAND) (I J) (:DEFINITION BINARY-LOGAND)
(BINARY-LOGAND T NIL))))
(TYPE-PRESCRIPTIONS
((11 (1298 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION BINARY-LOGAND) INTEGERP
(BINARY-LOGAND I J)))
((11 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T)))
(CONGRUENCES NIL)
(SYMBOL-CLASS :COMMON-LISP-COMPLIANT :IDEAL :ACL2-PROPERTY-UNBOUND
:PROGRAM)
(LEMMAS ((REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T)))
(STOBJS-OUT (NIL) :ACL2-PROPERTY-UNBOUND (NIL))
(FORMALS (I J) :ACL2-PROPERTY-UNBOUND (I J)) (LEVEL-NO 2)
(UNNORMALIZED-BODY
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQL I '-1) J
(IF (EQL J '-1) I
((LAMBDA (X J I)
(BINARY-+ X
(IF (EVENP I) '0 (IF (EVENP J) '0 '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I))))))
(QUICK-BLOCK-INFO (SELF-REFLEXIVE SELF-REFLEXIVE))
(INDUCTION-MACHINE
((TESTS-AND-CALLS ((ZIP I)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (ZIP J)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (NOT (ZIP J)) (EQL I '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(EQL J '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(NOT (EQL J '-1)))
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))))
(JUSTIFICATION (JUSTIFICATION (I) O-P O< (ACL2-COUNT I)))
(RECURSIVEP (BINARY-LOGAND))
(REDEFINED
(:RECLASSIFYING-OVERWRITE BINARY-LOGAND (I J) (NIL NIL) (NIL)))
(ABSOLUTE-EVENT-NUMBER 5625 :ACL2-PROPERTY-UNBOUND 527)
(PREDEFINED T T)
(GUARD (IF (INTEGERP I) (INTEGERP J) 'NIL) :ACL2-PROPERTY-UNBOUND
(IF (INTEGERP I) (INTEGERP J) 'NIL))
(STOBJS-IN (NIL NIL) :ACL2-PROPERTY-UNBOUND (NIL NIL)))
*UNDO-STACK*
((PROGN
(MAYBE-UNTRACE BINARY-LOGAND)
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::BINARY-LOGAND)
'(LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::BINARY-LOGAND (I J)
(COND
((AND (NOT (MEMBER-EQ
(F-GET-GLOBAL 'GUARD-CHECKING-ON
*THE-LIVE-STATE*)
'(NIL :NONE)))
(NOT (AND (INTEGERP I) (INTEGERP J))))
(THROW-RAW-EV-FNCALL
(LIST 'EV-FNCALL-GUARD-ER 'BINARY-LOGAND
(LIST I J)
'(AND (INTEGERP I) (INTEGERP J))
'(NIL NIL))))
((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*)
(RETURN-FROM ACL2_*1*_ACL2::BINARY-LOGAND
(IF (ACL2_*1*_ACL2::ZIP I) '0
(IF (ACL2_*1*_ACL2::ZIP J) '0
(IF (ACL2_*1*_COMMON-LISP::EQL I '-1) J
(IF (ACL2_*1*_COMMON-LISP::EQL J '-1)
I
(LET
((X
(ACL2_*1*_ACL2::BINARY-* '2
(ACL2_*1*_ACL2::BINARY-LOGAND
(ACL2_*1*_COMMON-LISP::FLOOR
I '2)
(ACL2_*1*_COMMON-LISP::FLOOR
J '2)))))
(ACL2_*1*_ACL2::BINARY-+ X
(IF
(ACL2_*1*_COMMON-LISP::EVENP
I)
'0
(IF
(ACL2_*1*_COMMON-LISP::EVENP
J)
'0 '1)))))))))))
(BINARY-LOGAND I J)))))
#:**1*-SYMBOL-KEY* ACL2_*1*_ACL2::BINARY-LOGAND
#:*GLOBAL-SYMBOL-KEY* ACL2_GLOBAL_ACL2::BINARY-LOGAND *PREDEFINED*
T SYSTEM:PNAME "BINARY-LOGAND")
ACL2>(lp)
ACL2 Version 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(include-book "ihs")
ACL2 Warning [WARNING-SUMMARY] in ( INCLUDE-BOOK "ihs" ...): There
is no certificate on file for
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp".
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
start address -T 0x8c3b000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
start address -T 0x8c4a000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
[SGC for 20 STRING pages..(13720 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
start address -T 0x8496fd0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
[SGC for 20 STRING pages..(13896 writable)..(T=3).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
start address -T 0x8ad0000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
start address -T 0x894af60 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rational-listp.o
start address -T 0x8a17f90 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rational-listp.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/natp-posp.o
start address -T 0x8424f90 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/natp-posp.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/top.o
start address -T 0x8a57c60 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/top.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/math-lemmas.o
start address -T 0x8a57cb0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/math-lemmas.o
[SGC for 20 CFUN pages..(14645 writable)..(T=4).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/quotient-remainder-lemmas.o
start address -T 0x8939120 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/quotient-remainder-lemmas.o
[SGC for 2016 CONS pages..(14844 writable)..(T=4).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-lemmas.o
start address -T 0x8a16000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-lemmas.o
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "../../../ihs/ihs-lemmas"
...): The compiled file for
"/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-lemmas.lisp" was not
loaded because the compiled file
"/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-lemmas.o" was not
found. See :DOC include-book.
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "ihs" ...): The compiled
file for
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp"
was not loaded because the compiled file
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.o"
was not found. See :DOC include-book.
Summary
Form: ( INCLUDE-BOOK "ihs" ...)
Rules: NIL
Warnings: Compiled file and WARNING-SUMMARY
Time: 2.02 seconds (prove: 0.00, print: 0.00, other: 2.02)
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp"
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'binary-logand)
(#:*CURRENT-ACL2-WORLD-KEY*
((COARSENINGS NIL)
(RUNIC-MAPPING-PAIRS
((1296 :DEFINITION BINARY-LOGAND)
(1297 :EXECUTABLE-COUNTERPART BINARY-LOGAND)
(1298 :TYPE-PRESCRIPTION BINARY-LOGAND)
(1299 :INDUCTION BINARY-LOGAND)))
(DEF-BODIES
(((2714 (IF (FORCE (INTEGERP I)) (FORCE (INTEGERP J)) 'NIL)
LOGCONS (B-AND (LOGCAR I) (LOGCAR J))
(BINARY-LOGAND (LOGCDR I) (LOGCDR J)))
(BINARY-LOGAND) (I J) (:DEFINITION LOGAND*)
(BINARY-LOGAND T T))
((1296 NIL IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I)))))
(BINARY-LOGAND) (I J) (:DEFINITION BINARY-LOGAND)
(BINARY-LOGAND T NIL)))
(((1296 NIL IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I)))))
(BINARY-LOGAND) (I J) (:DEFINITION BINARY-LOGAND)
(BINARY-LOGAND T NIL))))
(TYPE-PRESCRIPTIONS
((11 (2218 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION LOGAND-TYPE) INTEGERP
(BINARY-LOGAND I J))
(11 (1298 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION BINARY-LOGAND) INTEGERP
(BINARY-LOGAND I J)))
((11 (1298 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION BINARY-LOGAND) INTEGERP
(BINARY-LOGAND I J)))
((11 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T)))
(CONGRUENCES NIL)
(SYMBOL-CLASS :COMMON-LISP-COMPLIANT :IDEAL :ACL2-PROPERTY-UNBOUND
:PROGRAM)
(LEMMAS ((REWRITE-RULE (:REWRITE LOGAND-WITH-MASK) 2740
((LOGMASKP MASK) (EQUAL SIZE (INTEGER-LENGTH MASK))
(FORCE (INTEGERP I)))
EQUAL (BINARY-LOGAND MASK I) (LOGHEAD SIZE I)
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:REWRITE LOGAND-LOGXOR) 2732
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))
(FORCE (INTEGERP K)))
EQUAL (BINARY-LOGAND I (BINARY-LOGXOR J K))
(BINARY-LOGXOR (BINARY-LOGAND I J)
(BINARY-LOGAND I K))
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:REWRITE LOGAND-LOGIOR) 2731
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))
(FORCE (INTEGERP K)))
EQUAL (BINARY-LOGAND I (BINARY-LOGIOR J K))
(BINARY-LOGIOR (BINARY-LOGAND I J)
(BINARY-LOGAND I K))
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:DEFINITION LOGAND*) 2714
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))) EQUAL
(BINARY-LOGAND I J)
(LOGCONS (B-AND (LOGCAR I) (LOGCAR J))
(BINARY-LOGAND (LOGCDR I) (LOGCDR J)))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T T)) NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '-1 I) (IFIX I) ABBREVIATION NIL NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:REWRITE LOGAND-LOGXOR) 2732
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))
(FORCE (INTEGERP K)))
EQUAL (BINARY-LOGAND I (BINARY-LOGXOR J K))
(BINARY-LOGXOR (BINARY-LOGAND I J)
(BINARY-LOGAND I K))
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:REWRITE LOGAND-LOGIOR) 2731
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))
(FORCE (INTEGERP K)))
EQUAL (BINARY-LOGAND I (BINARY-LOGIOR J K))
(BINARY-LOGIOR (BINARY-LOGAND I J)
(BINARY-LOGAND I K))
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:DEFINITION LOGAND*) 2714
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))) EQUAL
(BINARY-LOGAND I J)
(LOGCONS (B-AND (LOGCAR I) (LOGCAR J))
(BINARY-LOGAND (LOGCDR I) (LOGCDR J)))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T T)) NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '-1 I) (IFIX I) ABBREVIATION NIL NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:REWRITE LOGAND-LOGIOR) 2731
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))
(FORCE (INTEGERP K)))
EQUAL (BINARY-LOGAND I (BINARY-LOGIOR J K))
(BINARY-LOGIOR (BINARY-LOGAND I J)
(BINARY-LOGAND I K))
BACKCHAIN NIL NIL T)
(REWRITE-RULE (:DEFINITION LOGAND*) 2714
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))) EQUAL
(BINARY-LOGAND I J)
(LOGCONS (B-AND (LOGCAR I) (LOGCAR J))
(BINARY-LOGAND (LOGCDR I) (LOGCDR J)))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T T)) NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '-1 I) (IFIX I) ABBREVIATION NIL NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:DEFINITION LOGAND*) 2714
((FORCE (INTEGERP I)) (FORCE (INTEGERP J))) EQUAL
(BINARY-LOGAND I J)
(LOGCONS (B-AND (LOGCAR I) (LOGCAR J))
(BINARY-LOGAND (LOGCDR I) (LOGCDR J)))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T T)) NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '-1 I) (IFIX I) ABBREVIATION NIL NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '-1 I) (IFIX I) ABBREVIATION NIL NIL
T)
(REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:REWRITE SIMPLIFY-LOGAND) 2625 NIL EQUAL
(BINARY-LOGAND '0 I) '0 ABBREVIATION NIL NIL T)
(REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:REWRITE COMMUTATIVITY-OF-LOGAND) 2624 NIL
EQUAL (BINARY-LOGAND I J) (BINARY-LOGAND J I)
BACKCHAIN ((I J BINARY-LOGAND)) NIL T)
(REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T))
((REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T)))
(STOBJS-OUT (NIL) :ACL2-PROPERTY-UNBOUND (NIL))
(FORMALS (I J) :ACL2-PROPERTY-UNBOUND (I J))
(LINEAR-LEMMAS
((LINEAR-LEMMA (2730 (NOT (< I '0)) (INTEGERP J))
(BINARY-LOGAND J I) (NOT (< I (BINARY-LOGAND J I))) NIL
(:LINEAR LOGAND-UPPER-BOUND . 2))
(LINEAR-LEMMA (2729 (NOT (< I '0)) (INTEGERP J))
(BINARY-LOGAND I J) (NOT (< I (BINARY-LOGAND I J))) NIL
(:LINEAR LOGAND-UPPER-BOUND . 1)))
((LINEAR-LEMMA (2729 (NOT (< I '0)) (INTEGERP J))
(BINARY-LOGAND I J) (NOT (< I (BINARY-LOGAND I J))) NIL
(:LINEAR LOGAND-UPPER-BOUND . 1))))
(LEVEL-NO 2)
(UNNORMALIZED-BODY
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQL I '-1) J
(IF (EQL J '-1) I
((LAMBDA (X J I)
(BINARY-+ X
(IF (EVENP I) '0 (IF (EVENP J) '0 '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I))))))
(QUICK-BLOCK-INFO (SELF-REFLEXIVE SELF-REFLEXIVE))
(INDUCTION-MACHINE
((TESTS-AND-CALLS ((ZIP I)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (ZIP J)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (NOT (ZIP J)) (EQL I '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(EQL J '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(NOT (EQL J '-1)))
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))))
(JUSTIFICATION (JUSTIFICATION (I) O-P O< (ACL2-COUNT I)))
(RECURSIVEP (BINARY-LOGAND))
(REDEFINED
(:RECLASSIFYING-OVERWRITE BINARY-LOGAND (I J) (NIL NIL) (NIL)))
(ABSOLUTE-EVENT-NUMBER 5625 :ACL2-PROPERTY-UNBOUND 527)
(PREDEFINED T T)
(GUARD (IF (INTEGERP I) (INTEGERP J) 'NIL) :ACL2-PROPERTY-UNBOUND
(IF (INTEGERP I) (INTEGERP J) 'NIL))
(STOBJS-IN (NIL NIL) :ACL2-PROPERTY-UNBOUND (NIL NIL)))
COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T T) *UNDO-STACK*
((PROGN
(MAYBE-UNTRACE BINARY-LOGAND)
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::BINARY-LOGAND)
'(LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::BINARY-LOGAND (I J)
(COND
((AND (NOT (MEMBER-EQ
(F-GET-GLOBAL 'GUARD-CHECKING-ON
*THE-LIVE-STATE*)
'(NIL :NONE)))
(NOT (AND (INTEGERP I) (INTEGERP J))))
(THROW-RAW-EV-FNCALL
(LIST 'EV-FNCALL-GUARD-ER 'BINARY-LOGAND
(LIST I J)
'(AND (INTEGERP I) (INTEGERP J))
'(NIL NIL))))
((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*)
(RETURN-FROM ACL2_*1*_ACL2::BINARY-LOGAND
(IF (ACL2_*1*_ACL2::ZIP I) '0
(IF (ACL2_*1*_ACL2::ZIP J) '0
(IF (ACL2_*1*_COMMON-LISP::EQL I '-1) J
(IF (ACL2_*1*_COMMON-LISP::EQL J '-1)
I
(LET
((X
(ACL2_*1*_ACL2::BINARY-* '2
(ACL2_*1*_ACL2::BINARY-LOGAND
(ACL2_*1*_COMMON-LISP::FLOOR
I '2)
(ACL2_*1*_COMMON-LISP::FLOOR
J '2)))))
(ACL2_*1*_ACL2::BINARY-+ X
(IF
(ACL2_*1*_COMMON-LISP::EVENP
I)
'0
(IF
(ACL2_*1*_COMMON-LISP::EVENP
J)
'0 '1)))))))))))
(BINARY-LOGAND I J)))))
#:**1*-SYMBOL-KEY* ACL2_*1*_ACL2::BINARY-LOGAND
#:*GLOBAL-SYMBOL-KEY* ACL2_GLOBAL_ACL2::BINARY-LOGAND *PREDEFINED*
T SYSTEM:PNAME "BINARY-LOGAND")
ACL2>(lp)
ACL2 Version 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(include-book "../../../ihs/ihs-definitions")
The event ( INCLUDE-BOOK "../../../ihs/ihs-definitions" ...) is redundant.
See :DOC redundant-events.
Summary
Form: ( INCLUDE-BOOK "../../../ihs/ihs-definitions" ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT
ACL2 !>
Bye.
elgin.cs.utexas.edu$ elgin.cs.utexas.edu$ ../../../../saved_acl2
GCL (GNU Common Lisp) 2.6.7 CLtL1 Sep 15 2005 12:36:56
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License: GPL due to GPL'ed components: (BFD 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 3.2.1 built July 2, 2007 16:31:43.
Copyright (C) 2007 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*).
See the documentation topic note-3-2-1 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
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 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(si::use-fast-links nil)
NIL
ACL2>(lp)
ACL2 Version 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(SET-DEBUGGER-ENABLE T)
<state>
ACL2 !>(include-book "../../../data-structures/array1")
(include-book "../../../arithmetic/rationals")
[SGC for 25 FIXNUM pages..(12615 writable)..(T=1).GC finished]
[SGC for 25 FIXNUM pages..(12615 writable)..(T=1).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
start address -T 0x8494000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
Summary
Form: ( INCLUDE-BOOK "../../../data-structures/array1" ...)
Rules: NIL
Warnings: None
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
"/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.lisp"
ACL2 !>[SGC for 555 CONS pages..(12985 writable)..(T=1).GC finished]
[SGC for 555 CONS pages..(12986 writable)..(T=1).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
start address -T 0x8995ec0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
[SGC for 7 SYMBOL pages..(13331 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
start address -T 0x894afc0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
start address -T 0x8424770 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
Summary
Form: ( INCLUDE-BOOK "../../../arithmetic/rationals" ...)
Rules: NIL
Warnings: None
Time: 0.25 seconds (prove: 0.00, print: 0.00, other: 0.25)
"/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.lisp"
ACL2 !>(include-book "ihs")
ACL2 Warning [WARNING-SUMMARY] in ( INCLUDE-BOOK "ihs" ...): There
is no certificate on file for
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp".
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
start address -T 0x8c3b000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
start address -T 0x8c4a000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
[SGC for 20 STRING pages..(13718 writable)..(T=3).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
start address -T 0x8496fd0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
[SGC for 20 STRING pages..(13895 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
start address -T 0x8ad0000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
start address -T 0x894af60 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rational-listp.o
start address -T 0x8a17f90 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rational-listp.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/natp-posp.o
start address -T 0x8424f90 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/natp-posp.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/top.o
start address -T 0x8a57c60 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/top.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/math-lemmas.o
start address -T 0x8a57cb0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/math-lemmas.o
[SGC for 20 CFUN pages..(14660 writable)..(T=4).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/quotient-remainder-lemmas.o
start address -T 0x8939120 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/quotient-remainder-lemmas.o
[SGC for 2016 CONS pages..(14844 writable)..(T=4).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-lemmas.o
start address -T 0x8a16000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-lemmas.o
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "../../../ihs/ihs-lemmas"
...): The compiled file for
"/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-lemmas.lisp" was not
loaded because the compiled file
"/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-lemmas.o" was not
found. See :DOC include-book.
ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "ihs" ...): The compiled
file for
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp"
was not loaded because the compiled file
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.o"
was not found. See :DOC include-book.
Summary
Form: ( INCLUDE-BOOK "ihs" ...)
Rules: NIL
Warnings: Compiled file and WARNING-SUMMARY
Time: 1.92 seconds (prove: 0.00, print: 0.00, other: 1.92)
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/ihs.lisp"
ACL2 !>
Bye.
elgin.cs.utexas.edu$ elgin.cs.utexas.edu$ ../../../../saved_acl2
GCL (GNU Common Lisp) 2.6.7 CLtL1 Sep 15 2005 12:36:56
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License: GPL due to GPL'ed components: (BFD 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 3.2.1 built July 2, 2007 16:31:43.
Copyright (C) 2007 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*).
See the documentation topic note-3-2-1 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
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 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(si::use-fast-links nil)
NIL
ACL2>(lp)
ACL2 Version 3.2.1. Level 1. Cbd
"/v/filer4b/v19q001/camm/gcl-issue/books/workshops/1999/pipeline/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(SET-DEBUGGER-ENABLE T)
<state>
ACL2 !>(include-book "../../../data-structures/array1")
(include-book "../../../arithmetic/rationals")
[SGC for 25 FIXNUM pages..(12615 writable)..(T=0).GC finished]
[SGC for 25 FIXNUM pages..(12615 writable)..(T=1).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
start address -T 0x8494000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.o
Summary
Form: ( INCLUDE-BOOK "../../../data-structures/array1" ...)
Rules: NIL
Warnings: None
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
"/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/array1.lisp"
ACL2 !>[SGC for 555 CONS pages..(12985 writable)..(T=1).GC finished]
[SGC for 555 CONS pages..(12986 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
start address -T 0x8995ec0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/equalities.o
[SGC for 7 SYMBOL pages..(13331 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
start address -T 0x894afc0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/inequalities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
start address -T 0x8424770 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.o
Summary
Form: ( INCLUDE-BOOK "../../../arithmetic/rationals" ...)
Rules: NIL
Warnings: None
Time: 0.26 seconds (prove: 0.00, print: 0.00, other: 0.26)
"/v/filer4b/v19q001/camm/gcl-issue/books/arithmetic/rationals.lisp"
ACL2 !>(include-book "../../../ihs/ihs-definitions")
Loading /v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
start address -T 0x8c3b000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/data-structures/utilities.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
start address -T 0x8c4a000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-init.o
[SGC for 20 STRING pages..(13761 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
start address -T 0x8496fd0 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-theories.o
[SGC for 20 STRING pages..(13921 writable)..(T=2).GC finished]
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
start address -T 0x8ad0000 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/logops-definitions.o
Loading /v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
start address -T 0x894af60 Finished loading
/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.o
Summary
Form: ( INCLUDE-BOOK "../../../ihs/ihs-definitions" ...)
Rules: NIL
Warnings: None
Time: 0.89 seconds (prove: 0.00, print: 0.00, other: 0.89)
"/v/filer4b/v19q001/camm/gcl-issue/books/ihs/ihs-definitions.lisp"
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'binary-logand)
(#:*CURRENT-ACL2-WORLD-KEY*
((COARSENINGS NIL)
(RUNIC-MAPPING-PAIRS
((1296 :DEFINITION BINARY-LOGAND)
(1297 :EXECUTABLE-COUNTERPART BINARY-LOGAND)
(1298 :TYPE-PRESCRIPTION BINARY-LOGAND)
(1299 :INDUCTION BINARY-LOGAND)))
(DEF-BODIES
(((1296 NIL IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I)))))
(BINARY-LOGAND) (I J) (:DEFINITION BINARY-LOGAND)
(BINARY-LOGAND T NIL))))
(TYPE-PRESCRIPTIONS
((11 (2218 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION LOGAND-TYPE) INTEGERP
(BINARY-LOGAND I J))
(11 (1298 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION BINARY-LOGAND) INTEGERP
(BINARY-LOGAND I J)))
((11 (1298 BINARY-LOGAND I J) NIL
(NIL :TYPE-PRESCRIPTION BINARY-LOGAND) INTEGERP
(BINARY-LOGAND I J)))
((11 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL BINARY-LOGAND I J) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T)))
(CONGRUENCES NIL)
(SYMBOL-CLASS :COMMON-LISP-COMPLIANT :IDEAL :ACL2-PROPERTY-UNBOUND
:PROGRAM)
(LEMMAS ((REWRITE-RULE (:DEFINITION BINARY-LOGAND) 1296 NIL EQUAL
(BINARY-LOGAND I J)
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQUAL I '-1) J
(IF (EQUAL J '-1) I
((LAMBDA (X J I)
(IF (EVENP I) (BINARY-+ X '0)
(IF (EVENP J) (BINARY-+ X '0)
(BINARY-+ X '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2)
(FLOOR J '2)))
J I)))))
DEFINITION ((BINARY-LOGAND) (BINARY-LOGAND T NIL))
NIL T)))
(STOBJS-OUT (NIL) :ACL2-PROPERTY-UNBOUND (NIL))
(FORMALS (I J) :ACL2-PROPERTY-UNBOUND (I J)) (LEVEL-NO 2)
(UNNORMALIZED-BODY
(IF (ZIP I) '0
(IF (ZIP J) '0
(IF (EQL I '-1) J
(IF (EQL J '-1) I
((LAMBDA (X J I)
(BINARY-+ X
(IF (EVENP I) '0 (IF (EVENP J) '0 '1))))
(BINARY-* '2
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))
J I))))))
(QUICK-BLOCK-INFO (SELF-REFLEXIVE SELF-REFLEXIVE))
(INDUCTION-MACHINE
((TESTS-AND-CALLS ((ZIP I)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (ZIP J)))
(TESTS-AND-CALLS ((NOT (ZIP I)) (NOT (ZIP J)) (EQL I '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(EQL J '-1)))
(TESTS-AND-CALLS
((NOT (ZIP I)) (NOT (ZIP J)) (NOT (EQL I '-1))
(NOT (EQL J '-1)))
(BINARY-LOGAND (FLOOR I '2) (FLOOR J '2)))))
(JUSTIFICATION (JUSTIFICATION (I) O-P O< (ACL2-COUNT I)))
(RECURSIVEP (BINARY-LOGAND))
(REDEFINED
(:RECLASSIFYING-OVERWRITE BINARY-LOGAND (I J) (NIL NIL) (NIL)))
(ABSOLUTE-EVENT-NUMBER 5625 :ACL2-PROPERTY-UNBOUND 527)
(PREDEFINED T T)
(GUARD (IF (INTEGERP I) (INTEGERP J) 'NIL) :ACL2-PROPERTY-UNBOUND
(IF (INTEGERP I) (INTEGERP J) 'NIL))
(STOBJS-IN (NIL NIL) :ACL2-PROPERTY-UNBOUND (NIL NIL)))
COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T T) *UNDO-STACK*
((PROGN
(MAYBE-UNTRACE BINARY-LOGAND)
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::BINARY-LOGAND)
'(LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::BINARY-LOGAND (I J)
(COND
((AND (NOT (MEMBER-EQ
(F-GET-GLOBAL 'GUARD-CHECKING-ON
*THE-LIVE-STATE*)
'(NIL :NONE)))
(NOT (AND (INTEGERP I) (INTEGERP J))))
(THROW-RAW-EV-FNCALL
(LIST 'EV-FNCALL-GUARD-ER 'BINARY-LOGAND
(LIST I J)
'(AND (INTEGERP I) (INTEGERP J))
'(NIL NIL))))
((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*)
(RETURN-FROM ACL2_*1*_ACL2::BINARY-LOGAND
(IF (ACL2_*1*_ACL2::ZIP I) '0
(IF (ACL2_*1*_ACL2::ZIP J) '0
(IF (ACL2_*1*_COMMON-LISP::EQL I '-1) J
(IF (ACL2_*1*_COMMON-LISP::EQL J '-1)
I
(LET
((X
(ACL2_*1*_ACL2::BINARY-* '2
(ACL2_*1*_ACL2::BINARY-LOGAND
(ACL2_*1*_COMMON-LISP::FLOOR
I '2)
(ACL2_*1*_COMMON-LISP::FLOOR
J '2)))))
(ACL2_*1*_ACL2::BINARY-+ X
(IF
(ACL2_*1*_COMMON-LISP::EVENP
I)
'0
(IF
(ACL2_*1*_COMMON-LISP::EVENP
J)
'0 '1)))))))))))
(BINARY-LOGAND I J)))))
#:**1*-SYMBOL-KEY* ACL2_*1*_ACL2::BINARY-LOGAND
#:*GLOBAL-SYMBOL-KEY* ACL2_GLOBAL_ACL2::BINARY-LOGAND *PREDEFINED*
T SYSTEM:PNAME "BINARY-LOGAND")
ACL2>
=============================================================================
Matt Kaufmann <address@hidden> writes:
> Hi, Camm --
>
> I'm hitting a reproducible problem when building the current
> development version of ACL2 on top of GCL 2.6.7, on ubuntu at UT CS.
> I've tried to track it down, but to no avail. I'm not having this
> problem in any other Lisp I've tested (Allegro CL, OpenMCL, SBCL,
> CMUCL, CLISP, Lispworks). So I hope you'll be willing to take a look.
>
> Actually, the problem went away when I used /p/bin/gcl-2.6.8pre on our
> system (which you seem to have installed in September of last year).
> But since the problem is rare even with /p/bin/gcl (2.6.7) -- I
> haven't seen it in many months, if ever -- I can easily imagine that
> it's not fixed in 2.6.8pre, but rather, we simply don't happen to hit
> the bad thing with the 2.6.8pre image we're using. In fact, even the
> 2.6.7 image only hits the problem on occasion; you can see in
> /projects/acl2/devel/logs/make-regression-gcl-fast-build-june28.log
> that almost all of the ACL2 regression suite passes.
>
> I have saved a pared-down tarball on the UT CS filesystem, which
> extracts to a directory gcl-issue/, with a file notes.txt that
> explains how to re-create the problem:
>
> /projects/acl2/gcl-issue.tgz
>
> You're welcome to copy it somewhere else; I'd also be happy to email
> it to you (2.54G). You're also welcome to work in the directory
>
> /projects/acl2/gcl-issue/
>
> which has the results of my following the instructions in notes.txt.
> I've tried this on two different 32-bit UT CS linux machines and
> gotten the problem on both.
>
> By the way, I tried compiling with safety 3 (see the first declaim
> form in acl2.lisp), but that didn't work ("Error: Invocation history
> stack overflow.").
>
> Thanks --
> -- Matt
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Gcl-devel] Re: GCL 2.6.7 problem,
Camm Maguire <=