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.

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.

External tools

• 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.