[Gcl-devel] Re: ACL2 binaries

[Matt Kaufmann]

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?

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

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

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

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