Profiling
This document explains the use of standard profiling tools for the
development of lambdapi
.
Using Linux perf
The quickest way to obtain a per-symbol execution time is perf
. It
is simple to use, provided that you have the right privileges on your
machine. No change is required in the build procedure, but lambdapi
must be invoked as follows.
dune exec -- perf record lambdapi [LAMBDAPI_OPTIONS]
The program behaves as usual, but a trace is recorded in file
perf.data
. The data can then be displayed with the following
command.
perf report
Profiling using Gprof
The gprof
tool can be used to obtain a more precise (and thorough)
execution trace. However, it requires modifying the src/dune
file by
replacing
(executable
(name lambdapi)
with the following.
(executable
(name lambdapi)
(ocamlopt_flags (:standard -p))
This effectively adds the -p
flag to every invocation of
ocamlopt
.
After doing that, lambdapi
can be launched on the desired example,
to record an execution trace. This has the (side-)effect of producing a
gmon.out
file. To retrieve the data, the following command can then
be used.
gprof _build/install/default/lambdapi gmon.out > profile.txt
It takes two arguments: the path to the lambdapi
binary used to
generate the profiling data, and the profiling data itself.