Performance debugging

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.

Note

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 --profile flag:

--profile=definitions

Break down by time spent checking each top-level definition.

--profile=modules

Break down by time spent checking each top-level module.

--profile=internal

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.

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.

agda-criterion has bindings for a small part of the criterion Haskell library for performance measurement.
agda-ghc-names can translate the names in generated Haskell code back to Agda names.