[Top][All Lists]

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

[Gcl-devel] Re: ACL2 binaries

From: Camm Maguire
Subject: [Gcl-devel] Re: ACL2 binaries
Date: 25 Oct 2004 10:31:22 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2


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

> (workshop books too?).  I am not sure if Warren Hunt really had a problem with

Not yet.  Should I test this?

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

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

> 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

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

reply via email to

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