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
verbosity:
-
-vprofile.definitions:10
¶
Break down by time spent checking each top-level definition.
-
-vprofile.modules:10
¶
Break down by time spent checking each top-level module.
-
-vprofile:7
¶
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.