[Top][All Lists]

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

[Gcl-devel] Re: gcl profiler?

From: Camm Maguire
Subject: [Gcl-devel] Re: gcl profiler?
Date: 12 Jul 2004 17:05:19 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!  Yes there are two profiling capabilities in GCL, based on
profil and gprof respectively, the latter giving the more extensive
output.  Gprof support needs to be selected at compile time with
--enable-gprof.  It is not enabled by default due to the extra memory
consumption.  Then just bracket your stuff between (si::gprof-start)
and (si::gprof-quit).  Presumably you want information not just on
time spent in GCL core functions, but also in your compiled lisp
code.  These functions need to be compiled into the .text section of
the executable in order to be reported, which one achieves via

(compiler::link (list "my_obj1.o" "my_obj2.o") "new_image")

Fire up new_image, and bracket the calls between gprof-start and
gprof-quit as described above.  Compiled lisp functions are given
arbitrary names, e.g. L1(), etc.  Each function has a comment in the C
source giving its lisp name.  So when compiling your objects, keep the
generated C by (setq compiler::*default-c-file* t) or use :c-file t as
a compile-file argument.  One of the todo items for the next release
is to include the lisp function name in the C function name for this
reason, as well as to hopefully enable gprof by default if the memory
usage can be worked out, and to see if profiling can be done when
modules are loaded into the .data section of the executable via (load

Take care,

"Matt Kaufmann" <address@hidden> writes:

> Eric --
> I think I've profiled with GCL and I might be able to find notes on that, but
> this may have changed anyhow now that you're using 2.6.2 (I think).  Camm is 
> on
> acl2-help and he may know this stuff cold, so perhaps he'll answer.  If you
> don't get an answer from him by the time you need it, ping me and I'll see 
> what
> I can do.
> Camm, if you send notes then I may put them on the ACL2 installation page for
> the next release, if you don't mind.
> -- Matt
>    Date: Mon, 12 Jul 2004 08:46:46 -0700 (PDT)
>    From: "Eric W. Smith" <address@hidden>
>    Reply-to: address@hidden
>    Sender: address@hidden
>    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
>    X-WSS-ID: 6CEC6D26880668-01-01
>    Content-Type: text/plain;
>     charset=us-ascii
>    X-Spam-Status: No, hits=0 required=5 tests=
>    X-Spam-Level:  
>    X-Scanned-By: MIMEDefang 2.39
>    Does gcl have a profiler?  I'd like to know where the time for my proofs is
>    going?.  (For example, how fast are my metafunctions?)  Has anyone profiled
>    ACL2 using gcl (maybe using gprof?)?
>    Thanks!
>    -Eric

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]