Sometimes your Agda program doesn’t type check or run as fast as you expected. This section describes some tools available to figure out why not.
This is a stub
Measuring typechecking performance¶
Agda can do some internal book-keeping of how time is spent, which can be turned on using the
Break down by time spent checking each top-level definition.
Break down by time spent checking each top-level module.
Break down by activity (such as parsing, type checking, termination checking, etc).
The Haskell runtime system can also tell you something about how Agda spends its time:
- +RTS -s -RTS¶
Show memory usage and time spent on garbage collection.
agda-bench is a tool for benchmarking compile-time evaluation and type checking performance of Agda programs.
Measuring run-time performance¶
Agda programs are compiled (by default) via Haskell (see Compilers), so the GHC profiling tools can be applied to Agda programs. For instance,
> agda -c Test.agda --ghc-flag=-prof --ghc-flag=-fprof-auto > ./Test +RTS -p
A complication is that the GHC backend generates names like
d76, so making sense of the
profiling output can require a little bit of work.