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

The Agda Emacs mode has an interactive highlighting feature, which highlights the term that is currently being type checked. This can often reveal which pieces of a definition slow down type checking. To enable interactive highlighting, use M-x customize-group agda2-highlight and set Agda2 Highlight Level to Interactive.

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.

External tools

• agda-bench is a tool for benchmarking compile-time evaluation and type checking performance of Agda programs.