[Agda] type check performance

[Wolfram Kahl]

On Thu, Aug 13, 2015 at 01:09:29AM +0400, Sergei Meshveliani wrote:
> I am writing in Agda a library for algebra. And the project is (mainly)
> stuck due to that  Agda 2.4.2.3  takes too much space and time to
> type-check the current module.
> 
> [...]
>  
> There are many modules in the project, and the (currently) last module
> Foo.agda  has only about 130 nonempty lines. 
> All the previous modules are type-checked in 1-2 hours.
> After this, to type check  Foo.agda  takes 
>                     40 minutes  under the options of  -M14G -H14G.
>  
> And under  -M9G -H9G,  it does not finish in 4 hours (and I have
> interrupted it). 

I just filed

  https://github.com/agda/agda/issues/1625

with references to some of my code, available on-line, where a single line
takes hours to check.

If less than 129 of the non-empty lines of your module are import statement,
I would recommend experimenting with splitting the module --- this can lead
to dramatic improvments. (My developments are full of small modules
split only for that reason.)

 >                     40 minutes  under the options of  -M14G -H14G.

Do supply also -S so you see how much heap is full and how much time
is spent on garbage collection, and also try e.g., -A1G, which on my developments
has the effect of drastically reducing the hectic of the garbage collector
and increasing the ``productivity'' of my Agda runs as reported by the GHC
run-time system.



> Is the main type check inefficiency due to call by name in the
> normalizer?

--sharing with the development version appears to help on my developments ---
Agda-2.4.2.3 is even slower.
( --no-eta seems to be not worth the hassle on that development. )


Best regards,

Wolfram