PerformanceTips

This page is intended to collect advice about how to manage improve/limit the space and time taken to type check your Agda development.

Don't use a 64-bit version of agda unless you have a lot of memory (> 8Gb)

Using a 64-bit version of agda compiled with a 64-bit version of ghc will use double the amount of memory as a 32-bit agda. Eg. building the standard library on my machine using the current development version of agda (9/9/2011) has a peak memory usage of 576Mb with a 32-bit version and 1167Mb with a 64-bit version. The 64-bit version is also marginally slower as it does some more garbage collection (7m30s as opposed to 6m38s).

A 32-bit version of agda can only allocate 4Gb of memory, presumably a 64-bit version would allocate 8Gb to do the same task. This implies that you would only gain an advantage from using the 64-bit version if you have more than 8Gb of memory.

Tweak the ghc runtime behaviour

Nisse uses the following configuration on his 4Gb machine. The flags between +RTS and -RTS supply arguments to the ghc runtime systems which controls memory usage of the heap and the stack. normal agda arguments come afterwards:

agda +RTS -K40M -M1.5G -RTS blah.agda

-K40M sets the size of the stack to 40Mb. The default is 8M. Sometimes Agda requires a bigger stack and this prevents Agda producing a stack overflow error. This one is a bit of a no-brainer, if you need a bigger stack than 8Mb to check your development then you need to change this setting, otherwise you don't.

-M1.5G sets the maximum heap size to 1.5Gb. This is intended to stop your computer from using so much memory it will start swapping. The downside is that you might need more heap space. But, if your computer is swapping you're not really in a usable state anyway so perhaps it's better to give up early. The rule of thumb here is that if it is swapping you're already dead.

Another useful RTS flag is -s. This gives a summary of memory usage and runtime. Eg.

Ulf on the other hand does not use settings like these.

These options can also be set in the emacs mode for using Agda interactively.

One option:

• M-x customize-group RET haskell-ghci RET
• Add three new arguments to "Haskell Ghci Program Args": +RTS -MxxG -RTS

You could also use the GHCRTS environment variable.

Write a prototype with type-in-type

You can play things less safe by using type-in-type instead of universe polymorphism. Universe polymorphism has about a factor of three penalty in 2.2.10 and a factor of two penalty in the development version (although the absolute penalty has decreased). Your mileage may vary.

Try the development version!

The current development version 2.2.11 has significantly better performance than the current release version 2.2.10

Checking version 0.5 of the standard library with agda 2.2.10 takes 9m45s and 876Mb peak memory usage. Checking the current development version of the standard library with the current development version of agda (9/9/2011) takes 6m38s and 576Mb. For other developments the difference can be more dramatic like taking minutes instead of hours or checking in several Gb instead of being unfeasible.

For a formalization of relative monads I did some rough benchmarks:

It is interesting to see that universe-polymorphism in the development version is faster than type-in-type in 2.2.10

Split up your file

If you have a big file then you should split it up and import the pieces. Agda generates and serializes files to disk when it type checks a file storing the result in a .agdai file. Apart from the fact there when you make a change later earlier definitions imported from another file won't need to be rechecked the serialization process also recovers some sharing. There is not much performance difference between splitting up the file a lot and importing lots of pieces or just using one import. This is a sensible design strategy.

Use abstract

A useful technique is to mark some proofs as abstract ((Nisse says he always this does equality proofs)) this means they don't get unfolded. In Coq ending your proof with "Qed." (instead of "Defined") has roughly the same effect. Before abstract you could do roughly the same thing by first proving your lemma, then commenting it out and postulating it, but this is cheating:

{-
prf : A
prf = …(real)…
-}
postulate prf : A

Abstract is rather more honest:

abstract
  prf : A
  prf = ...(real)...

Use Irrelevance

You can try to experimental support for proof irrelevance to prevent agda from keeping computationally irrelevant things (such as equality proofs) in memory. This can have a dramatic effect but is experimental and also limited. For example you cannot substitute by a irrelevant equation in a relevant type.