Profiling

Profiling the Idris compiler

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.

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.