Greetings! <[EMAIL PROTECTED]> writes:
> Camm, > I am making slow but steady progress toward my goal of being able to > profile the execution of my ACL2 books. Previously, I had been able > to build a profiling gcl. Thanks to help from you and Matt > Kaufmann, I can now generate .o's with the right sort of init > functions, and can build an ACL2 image whose primitives (e.g., those > files in axioms.lisp, etc.) can be profiled. However, the profiling > results still don't include my application ACL2 code. Note that I > *can* profile my code if it is "plain old" GCL: I just > (COMPILER::LINK (list "myfun1.o" "myfun2.o" ...) "MyNewExecutable"), > start MyNewExecutable, then do the SI::GPROF-START/SI::GPROF-QUIT > thing. But, no such luck for my ACL2 code. First, we should understand that a limitation of the ld workaround means that the heap has to be recreated *from scratch* in each compiler::link. One can alas not use this mechanism to incrementally modify a heap with a load/dump/reexecute sequence. This is one of the primary reasons I'd like to get pg support, dyn lib support, and ia64/mips/alpha/hppa support into the standard load/unexec incremental process seemingly so true to the spirit of lisp. What this essentially means is that you need to append your "foo.o" to the list of si::*binary-modules* supplied to compiler::link in dlopen.lsp, and run it again in profgcl. It doesn't appear that you have tried this yet -- if you have and it failed, please let me know. You should also know that I use this script primarily to build acl2 on ia64/alpha/mips/hppa, on which we can only load .o files using dlopen. There is a limit of 1024 such files, hence I've prevented the compilation of closures. You likely need not do this. I'd still suggest trying dlopen (with the append) as is first. > I have been trying to > use the dlopen.in that you sent me, but perhaps I don't know how to > use it yet. Here's the scenario: I have built a profiling GCL > 2.6.5 executable, which I'll call profgcl here. I have an ACL2 2.9 > distribution; my current working directory is its acl2-sources. I > start up profgcl, then paste in the dlopen.in that you sent, having > changed "/usr/share/[EMAIL PROTECTED]@/" to the appropriate directory > path. It runs, and I get an nsaved_acl2.gcl, which I can then use > to certify the distributed books, etc. So far so good. Now, I want > to add my own object file, myACL2fun1.o, which was compiled via an > ACL2 CERTIFY-BOOK, using an earlier ACL2 built on top of the > profiling GCL, with COMPILER::*DEFAULT-SYSTEM-P* set to T. I want > to add myACL2fun1.o to the set of files that get ld'ed, so I can > profile it -- how do I do that? Please be specific -- I have tried > a number of things, including setting SI::*BINARY-MODULES* to (list > "myACL2fun1.o") by hand, and none of them has worked. OK, try this: ============================================================================= (let ((si::*collect-binary-modules* t) ;; Collect a list of names of each object file loaded si::*binary-modules* (my-modules (list "myACL2fun1.o" "myACL2fun2.o")) ;; Put your custom modules here (compiler::*default-system-p* t));; .o files to be linked in via ld ;; must be compiled with :system-p t (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* ((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/[EMAIL PROTECTED]@/") ;; save-acl2 nil no-save)))))))) (eval com) ;; first evaluate the command in gcl (compiler::link ;; link in the .o files with ld (append (remove-duplicates si::*binary-modules* :test (function equal));; collected here my-modules) ;; your modules here "saved_acl2" ;; new image (format nil "~S" com) ;; run the build sequence again in this image ;; with load redirected to initialize "" nil))) ============================================================================= > Also, the > comments in dlopen.in indicate that it should be run twice -- does > that happen automatically, or do I have to paste it in twice. If it It happens automatically, once in the (eval com), and then once in the image produced by compiler::link as supplied in the third argument as an init string to run. > is the latter, how exactly do I perform the second run? Many thanks > in advance -- solving this problem in as soon as possible is quite > important to my project. David Hardin If you get stuck and want to send me your .lisp, I might have time to help. Take care, -- Camm Maguire [EMAIL PROTECTED] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel