[Top][All Lists]
[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
- [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/25
- [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/25
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries,
Matt Kaufmann <=
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28