Profiling

Profiling the Idris compiler

First, you need to have Idris and all dependencies compiled with profiling support. To do this, enable the lines library-profiling: True and executable-profiling: True in ~/.cabal/config before installing everything. Alternatively, always pass Cabal the --enable-executable-profiling and --enable-library-profiling flags.

The next step is to run Idris with the flags +RTS -P.

Controlling the C RTS

Idris code that has been compiled with the default C backend has RTS options available to control the initial stack and heap size as well as to print information about the GC. Run a.out +RTS -? -RTS to get a list of RTS options. One of the most useful is +RTS -s -RTS, which prints a summary of allocator and GC activity.

Profiling generated C code

The first step in profiling the generated code is to compile it with instrumentation. This is done by passing GCC the option -pg. A way to have Idris do this for you is to set the environment variable IDRIS_CFLAGS to -pg. Example: IDRIS_CFLAGS="-pg" idris MyProgram.idr -o program When the program is run, it will create a file called gmon.out with the profile data. To view this in a human-readable form, use gprof program gmon.out | less.

Alternatively, compile the C code with gcc -g and then use Valgrind with the callgrind tool.

If you want a better idea of what the functions in the profile are doing, run Idris with two extra options: --dumpcases FILE and --dumpdefuns FILE, which causes intermediate language expressions to get dumped to files which can be examined.