Re: [Gcl-devel] Re: ACL2 binaries

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> 
> Please see comments below.
> 
> > Cc: address@hidden, address@hidden, address@hidden,
> >         address@hidden, address@hidden,
> >         Aurelien Chanudet <address@hidden>
> > From: Camm Maguire <address@hidden>
> > Date: 25 Oct 2004 10:31:22 -0400
> > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > Content-Type: text/plain; charset=us-ascii
> > X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > X-UTCS-Spam-Status: No, hits=-332 required=180
> 
> > Greetings!
> 
> > Matt Kaufmann <address@hidden> writes:
> 
> > > Hi, Camm --
> > > 
> > > Thank you for dealing with compiler::link.  I didn't see any obvious 
> > > problems
> > > with your approach, not that I understood it all that well (I guess
> > > compiler::link somehow resets si;:*binary-modules* to nil, thus avoiding 
> > > the
> > > error on the second pass, but maybe I'm confused; probably it's not 
> > > important
> > > that I understand).  It's encouraging that you were able to certify all 
> > > books
> 
> > The second pass is run in a different image, outside of the lexical
> > scope of the let in the parent image, and therefore with the default
> > nil binding to si:*binary-modules*.
> 
> Sorry, I'm confused.  In the form you sent me, included (but edited) just
> below, I see (eval com) immediately followed by (compiler::link ...).  Are you
> saying that actually you create the same form twice, except with (eval com) in
> one and (compiler::link ...) in the other?
> 

Basically.  The first eval runs in the image in which the main form is
being evaluated.  compiler::link creates a second image with ld, and
adds the com form to the input file used to initialize this second
image.  The main image then runs the second image with its
initialization file as its input as a subprocess.

> (let ((si::*collect-binary-modules* t) ;; Collect a list of names of each 
> object file loaded 
>       si::*binary-modules*)
>   
>   (let (.....)
>     
>     (eval com)                                                       ;; first 
> evaluate the command in gcl
>     (compiler::link                                                  ;; link 
> in the .o files with ld
>      (remove-duplicates si::*binary-modules* :test (function equal)) ;; 
> collected here
>      "nsaved_acl2.gcl"                                               ;; new 
> image
>      (format nil "~S" com)                                           ;; run 
> the build sequence again in this image
>                                                                      ;; with 
> load redirected to initialize
>      ""        
>      nil)))
> 
> > > (workshop books too?).  I am not sure if Warren Hunt really had a problem 
> > > with
> 
> > Not yet.  Should I test this?
> 
> I think there's value in testing with all the workshop books.  I typically do
> this frequently when I make changes, and sometimes they uncover issues that 
> the
> distributed books don't.  But I don't know enough about your other priorities
> to say "should".

OK, this is now done (successfully) on both i386 using the standard
build sequence and ia64 using the one provided above.

I'm hoping that the make will bomb and exit with an error code if one
of the certification steps fails.

> 
> > > the standard build on Itanium (and I think, Bob Boyer isn't sure either), 
> > > but
> > > if you think that's the case then that's good enough for me.
> > > 
> 
> > My understanding is that the 2.8 Itanium build is working for them.
> > You have pointed out an issue in an earlier email where some debugging
> > function is not being loaded with this method.  I'll try to look into
> > this, but I'm hoping that this new approach might avoid that
> > discrepancy for 2.9.
> 
> OK, thanks.  I'd forgotten about that issue (and still have forgotten!).
> 

I'll see if I can dig it out of my pile of old email.

> > > I confess that it makes me a little nervous that you have to delete the
> > > "ACL2-PC" package, and more generally that you combine the compile and
> > > load/save passes into a single gcl invocation, unlike the two gcl 
> > > invocations
> > > we otherwise make.  I haven't thought through whether there are any 
> > > "gotchas"
> 
> > Me too.
> 
> > > in doing so (for example, re-evaluation of defconstant forms comes to 
> > > mind,
> > > though that's probably not an issue).  I realize that you take advantage 
> > > of the
> 
> > Confused here.
> 
> Quite possibly, all of my comments are off-base because of confusion on my 
> part
> (see my "Sorry, I'm confused" above).
> 
> > > collection of .o files into si::*binary-modules* during the compile pass, 
> > > but
> > > we could arrange to write out a little file at the end of the compile 
> > > pass with
> > > the value of si::*binary-modules*, which would then be used in the second 
> > > gcl
> > > invocations (load/save) -- thus perhaps keeping the two gcl invocations
> > > separate.  (But I realize that I could be completely off-base; perhaps 
> > > previous
> 
> > This could very well be done, as it was in 2.8.  The primary issue is
> > that at some point one might want all those >3500  compiled closures
> > in the list, making this approach unwieldy.  I should emphasize here
> > that in this first attempt, these closures run *interpreted* on the
> > systems where compiler::link is required (ia64, alpha, mips, hppa).
> > This does not seem to bog the regression time down much from my very
> > rudimentary observation.  As stated in the comments, this can likely
> > be improved.  I just don't know how important it is.  If it is not
> > important, then of course a two-gcl-invocation approach is
> > straightforward. 
> 
> Aha; I might be gaining a glimmer of understanding finally.  I think those
> closures you refer to are from so-called *1* functions (also known as
> "executable counterparts" -- functions like that gazonk520.o function for the
> possible Windows bug we were looking at.  I believe that I got stack overflows
> on occasion during the build process, from the way ACL2 uses these functions 
> in
> its own handling of macroexpansion.  But if you can do the build without
> macroexpansion, then probably this isn't a problem as long as you load TMP1.o
> at some point, which holds the compiled *1* functions that we care most about
> for the user.
> 

OK, I don't seem to be getting a stack overflow, and we definitely
link in TMP1.o.  I'm assuming the above means that there should also
be no significant performance impact, though I have not tested this.
If not, then we really need not revisit this secondary build sequence
again until I get native loading working on the other machines.

> > > emails from you have explained why two passes are needed.)
> > > 
> > > But the bottom line is that I'm happy not to understand compiler::link, 
> > > and I'm
> 
> > As I would be too!
> 
> > > happy if you are and if all books certify.  If there's anything you want 
> > > us to
> > > add to the ACL2 sources to support this, let me know.
> > > 
> 
> > Not necessary I hope.  Looking at this has made me feel anew the
> > importance of extending native object relocation to these systems.
> > I think we can use dldbfd.c from the lush sources as a guide.
> > Aurelien, do you have any comments here?
> 
> > Take care,
> 
> Thanks --
> -- Matt

Take care,

> 
> > > Thanks again --
> > > -- Matt
> > >    Cc: address@hidden, address@hidden, address@hidden
> > >    From: Camm Maguire <address@hidden>
> > >    Date: 21 Oct 2004 16:32:43 -0400
> > >    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > >    Content-Type: text/plain; charset=us-ascii
> > >    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > >    X-UTCS-Spam-Status: No, hits=-222 required=180
> > > 
> > >    Greetings!  Just thought I'd let you know about the steps thus far at
> > >    building with compiler::link for ia64,mips,alpha, and hppa.  It is
> > >    really quite ugly, and is leading me to try to get native relocations
> > >    on these machines soon.  Alas, the latter is even uglier, though just
> > >    for gcl implementors, not users!
> > > 
> > >    This produces an image which will certify all books.
> > > 
> > >    Comments most appreciated, esp. re: possible oversights on my part.
> > > 
> > >    
> > > =============================================================================
> > >    (let ((si::*collect-binary-modules* t) ;; Collect a list of names of 
> > > each object file loaded 
> > >     si::*binary-modules*)
> > > 
> > >      (let ((com (quote    ;; This is a command to build acl2 which will 
> > > be run twice --
> > >                      ;; once in stock gcl, compiling files, loading and 
> > > recording same
> > >                      ;; once in an image which is linked via ld from the 
> > > results of the above
> > >                      ;;   redirecting each load to an initialization of 
> > > the .o file already
> > >                      ;;   linked into the image by ld
> > >             (progn
> > >               (load "init.lsp.ori")
> > >               (let* ((compiler::*default-system-p* t)       ;; .o files 
> > > to be linked in via ld
> > >                                                             ;; must be 
> > > compiled with :system-p t
> > >                      (la (find-symbol "LOAD-ACL2" "ACL2"))  ;; 
> > > acl2::load-acl2 doesn't exist at read-time
> > >                      (olf (symbol-function la))
> > >                      (si::*collect-binary-modules* t))      ;; make sure 
> > > the second pass watches for
> > >                                                             ;; .o loads, 
> > > for the purpose of triggering an error
> > >                 (unless (probe-file "axioms.o")             ;; no sense 
> > > to compile twice
> > >                   (funcall (symbol-function (find-symbol "COMPILE-ACL2" 
> > > "ACL2")))
> > >                   (delete-package "ACL2-PC"))               ;; prevent 
> > > package error when loading after compiling 
> > >                 (funcall olf)                               ;; must 
> > > load-acl2 to establish the symbols below 
> > >                 (let ((sa (find-symbol "SAVE-ACL2" "ACL2"))
> > >                       (ia (find-symbol "INITIALIZE-ACL2" "ACL2"))
> > >                       (ib (find-symbol "INCLUDE-BOOK" "ACL2"))
> > >                       (ap2f (find-symbol "*ACL2-PASS-2-FILES*" "ACL2"))
> > >                       (ocf (symbol-function 'compiler::compile))
> > >                       (osf (symbol-function 'si::save-system)))
> > >                   (setf (symbol-function 'compiler::compile)     ;; For 
> > > now, run closures interpreted
> > >                         (lambda (x) (symbol-function x)))        ;; At 
> > > some point, could compile saved
> > >                                                                  ;; 
> > > gazonk files without loading (i.e.
> > >                                                                  ;; 
> > > returning interpreted code) on first pass
> > >                                                                  ;; then 
> > > don't compile by load -> initialize
> > >                                                                  ;; on 
> > > second pass.  Cannot load via dlopen
> > >                                                                  ;; more 
> > > than 1024 files at once, and this is
> > >                                                                  ;; the 
> > > only relocation mechanism currently
> > >                                                                  ;; 
> > > available on ia64,alpha,mips,hppa
> > >                                                                  ;; On 
> > > first attempt, failure on initizlization of
> > >                                                                  ;; 
> > > acl2_gazonk3558.o
> > >                   (setf (symbol-function la) (lambda () nil))    ;; 
> > > save-acl2 calls load-acl2, but we can't load
> > >                                                                  ;; twice 
> > > when initializing in reality.
> > >                   (setf (symbol-function 'si::save-system)       ;; 
> > > Restore all moved functions on save-system
> > >                         (lambda (x)
> > >                           (setf (symbol-function 'compiler::compile) ocf)
> > >                           (setf (symbol-function la) olf)
> > >                           (setf (symbol-function 'si::save-system) osf)
> > >                           (when si::*binary-modules*             ;; 
> > > Saving when a .o has been loaded is a no-no
> > >                             (error "Loading binary modules prior to image 
> > > save in dlopen image: ~S~%"
> > >                                    si::*binary-modules*))
> > >                           (funcall osf x)))
> > >                   (let* ((no-save si::*binary-modules*))         ;; Don't 
> > > call save-system on first pass
> > >                     (funcall (symbol-function sa)
> > >                              (list ia (list 'quote ib) ap2f 
> > > "/usr/share/acl2-2.9/") ;; save-acl2
> > >                              nil
> > >                              no-save))))))))
> > > 
> > >        (eval com)                                                       
> > > ;; first evaluate the command in gcl
> > >        (compiler::link                                                  
> > > ;; link in the .o files with ld
> > >    (remove-duplicates si::*binary-modules* :test (function equal)) ;; 
> > > collected here
> > >    "nsaved_acl2.gcl"                                               ;; new 
> > > image
> > >    (format nil "~S" com)                                           ;; run 
> > > the build sequence again in this image
> > >                                                                    ;; 
> > > with load redirected to initialize
> > >    ""        
> > >    nil)))
> > >    
> > > =============================================================================
> > >    Take care,
> > >    -- 
> > >    Camm Maguire                                            address@hidden
> > >    
> > > ==========================================================================
> > >    "The earth is but one country, and mankind its citizens."  --  
> > > Baha'u'llah
> > > 
> > > 
> > > 
> 
> > -- 
> > Camm Maguire                                         address@hidden
> > ==========================================================================
> > "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
> 
> 
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://lists.gnu.org/mailman/listinfo/gcl-devel
> 
> 
> 

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