[Agda] Some comments on agda performance

[Alan Jeffrey]

Hi everyone,

I've been cranking out proofs in agda for a paper I'm writing, and 
discovered some performance characteristics.

a) The machine I'm working on is a quad-core 1.6GHz Atom, and agda is 
single-threaded, so unsurprisingly it's sluggish.  (Yes, yes, I know, 
buy a faster machine... :-)  I'm guessing that adding multicore support 
to agda is non-trivial, and I shouldn't hold my breath waiting for it.

b) To reduce memory usage, I stopped using the standard library, and 
just copied the parts I needed (not very much, just propositional 
equality, existentials, products, lists and a few other bits and 
pieces).  Memory usage with the standard library was more than twice 
what it was without.  It would be nice if the standard library was a bit 
more modular, for example if I could use Data.List without dragging in 
the whole Algebra module.  Of course this would be difficult to achieve 
without breaking many existing programs.

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.

d) Most of the time when I'm working on a proof-in-progress, I don't 
care about cases being exhaustive, or about termination, when I reload 
it's because I've done something like introduce an optional parameter to 
a pattern.  It would be nice if I could use an emacs command to do a 
minimal reload that allows me to get on with proof refinement.

Thanks for the great work on agda, it's a brilliant system, and I'm 
enjoying using it very much!  My proofs thank you too :-)

Alan Jeffrey.