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.

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_CC to gcc -pg. Example: IDRIS_CC="gcc -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.