[Agda] Some comments on agda performance

[Nils Anders Danielsson]

On 2010-04-21 16:04, Alan Jeffrey wrote:
> c) My proofs were mostly constructed top-down breadth-first, so had
> quite a lot of proof holes (~25 in the current proof fragment) causing
> agda to spend a long time on constraint solving, getting on for 20s per
> proof refinement.  Replacing the proof holes by a (temporarily
> introduced!) term HOLE : {X : Set} -> X gave a speed up of about 5
> times.  I don't know if this is well-known agda folklore or not.

I think that, whenever a meta-variable is instantiated, Agda checks if
progress can be made on any of the other metas. If this is the case,
then it may be a good idea to keep track of dependencies between metas,
to avoid unnecessary work.

--
/NAD