[Gcl-devel] Re: /p/bin/xa and /p/bin/xg

[Camm Maguire]

Greetings!

OK, just checked in what appears to be a fix for both static weak
symbol relocation bugs you've reported.  Please let me know if
problems persist.

Take care,

Robert Boyer <address@hidden> writes:

> OK, I suspect that the static/remprop patch that Camm very
> recently recommended is now accurately install in a large
> static UTCS GCL 2.7.0 image, viz., /p/bin/xg, and in an ACL2
> 2.9.4 image built on it, viz., /p/bin/xg.  This was done by
> me with following dubious (to me) act.  During the GCL
> build:
> 
>   cat /u/boyer/init_boyer.lisp >> unixport/init_ansi_gcl.lsp
> 
> That was simply the first way I could find to achieve a
> patch.  Gross.
> 
> /u/boyer/init_boyer.lisp contains:
> 
>    (print "Loading init_boyer.lisp" t)
>    ; Camm patch for static problem 2006516
>    (si::remprop 'read-byte 'compiler::co1)
>    (print "Done loading init_boyer.lisp" t)
> 
> Below is Jared's 'read-all' example, apparently now working.
> 
> Bob
> 
> % /p/bin/xa
> GCL (GNU Common Lisp)  2.7.0 ANSI    Apr 14 2006 16:04:17
> Source License: LGPL(gcl,gmp,pargcl), 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.
> Temporary directory for compiler files set to /tmp/
> 
>  ACL2 Version 2.9.4 built April 16, 2006  09:40:40.
>  Copyright (C) 2006  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-2-9-4 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 2.9.4.  Level 1.  Cbd "/v/filer2/boyer/acl2/acl2-sources/".
> Type :help for help.
> Type (good-bye) to quit completely out of ACL2.
> 
> ACL2 !>    (defun read-all (channel state acc)
>        (declare (xargs :mode :program
>                      :stobjs state))
>        (mv-let (byte state)
>              (read-byte$ channel state)
>              (if (eq byte nil)
>                  (mv (reverse acc) state)
>                (read-all channel state (cons byte acc)))))
> 
> Summary
> Form:  ( DEFUN READ-ALL ...)
> Rules: NIL
> Warnings:  None
> Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
>  READ-ALL
> ACL2 !>    (comp t)
> 
> ;; Compiling /v/filer2/boyer/acl2/acl2-sources/address@hidden@.lisp.
> ;; End of Pass 1.  
> ;; End of Pass 2.  
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3, 
> (Debug quality ignored)
> ;; Finished compiling /v/filer2/boyer/acl2/acl2-sources/address@hidden@.o.
> Loading /v/filer2/boyer/acl2/acl2-sources/address@hidden@.o
> start address -T 0xab7ea68 Finished loading 
> /v/filer2/boyer/acl2/acl2-sources/address@hidden@.o
> ;; Compiling /v/filer2/boyer/acl2/acl2-sources/address@hidden@1.lisp.
> ;; End of Pass 1.  
> [SGC for 73 CONS pages..(4158 writable)..(T=1).GC finished]
> ;; End of Pass 2.  
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3, 
> (Debug quality ignored)
> ;; Finished compiling /v/filer2/boyer/acl2/acl2-sources/address@hidden@1.o.
> Loading /v/filer2/boyer/acl2/acl2-sources/address@hidden@1.o
> start address -T 0xaae42a0 Finished loading 
> /v/filer2/boyer/acl2/acl2-sources/address@hidden@1.o
>  T
> ACL2 !>    (mv-let
>       (channel state)
>       (open-input-channel "/projects/hvg/ACL2/v2-9-4-hons/axioms.lisp" :byte 
> state)
>       (mv-let (data state)
>             (read-all channel state nil)
>             (declare (ignore data))
>             state))
> [SGC for 99 STRUCTURE pages..(4160 writable)..(T=1).GC finished]
> [SGC for 99 STRUCTURE pages..(4160 writable)..(T=1).GC finished]
> [SGC for 73 CONS pages..(4197 writable)..(T=1).GC finished]
> [SGC for 760 STRUCTURE pages..(5007 writable)..(T=2).GC finished]
> [SGC for 1156 STRUCTURE pages..(5688 writable)..(T=4).GC finished]
> [SGC for 2370 STRUCTURE pages..(7490 writable)..(T=6).GC finished]
> [SGC for 0 RELOCATABLE-BLOCKS pages..(7939 writable)..(T=7).GC finished]
> [SGC for 3027 CONS pages..(23037 writable)..(T=11).GC finished]
> <state>
> ACL2 !>
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah