gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] Re: ACL2 binaries


From: Matt Kaufmann
Subject: Re: [Gcl-devel] Re: ACL2 binaries
Date: Thu, 28 Oct 2004 08:53:52 -0500

Thanks, Camm.  Please see comments below.

> Cc: address@hidden, address@hidden, address@hidden,
>         address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 28 Oct 2004 09:41:50 -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 --
> > 
> > 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.

I think I understand; thanks.  So, you're doing the compile and the
(funcall (symbol-function sa) ...) in the same image, which is why you need to
evaluate (delete-package "ACL2-PC").

> > (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.

Great!

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

Hmmm, that's a good point and I don't think we do that.  Rather, we print ** to
the log file.  I've made a note to improve this before the next release (time
permitting) to return a non-zero error code.

> > 
> > > > 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.

If you care to (or, you can ask me to, or we can let it drop).

> > > > 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.

OK.  I think all is well then.  I seem to recall a very minor performance gain
when we do those compiles, but I suspect it's under a percent and you needn't
bother further.

> > > > 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 --
-- Matt

> > 
> > > > 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




reply via email to

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