[isabelle-dev] profiling

[Brian Huffman]

Hello all,

I am trying to use profiling to measure the performance of the HOLCF
domain package. I recently discovered that I can enable profiling in
Isabelle with the following command:

ML {* Toplevel.profiling := 1; *}

Here's the output from a "new_domain" command that I tried:

... (lots of small numbers) ...
        10 Defs.reduction(4)reduct(3)
        11 Table().fold_table(1)fold(2)
        12 Defs.match_args(2)
        12 Sorts.mg_domain(3)
        13 Type.raw_match(3)
        15 List.map(2)
        16 GARBAGE COLLECTION (update phase)
        21 GARBAGE COLLECTION (mark phase)
        39 Table().lookup(2)look(1)
        39 GARBAGE COLLECTION (total)
        40 Table().modify(3)modfy(1)

Total: 293; Counted: 293; Uncounted: 0
### 1.420s elapsed time, 1.284s cpu time, 0.156s GC time

Apparently the domain package spends a lot of time doing lookups and
modifications of tables. But I have no idea which functions are
calling the table library, so this information is basically useless.

What other profiling tools are available for me to use? It would be
nice to have something similar to the profiler in GHC, which outputs a
tree-like table that shows the time spent in each function, as well as
the total inherited time from all other functions called by it.

- Brian