gcl-devel
[Top][All Lists]
Advanced

[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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]