[Agda] type check performance

[Wolfram Kahl]

On Sat, Aug 15, 2015 at 12:01:21AM +0400, Sergei Meshveliani wrote:
> On Wed, 2015-08-12 at 23:55 -0400, Wolfram Kahl wrote:
> > On Thu, Aug 13, 2015 at 01:09:29AM +0400, Sergei Meshveliani wrote:
> > > 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). 
> 
> > 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.)
> 
> 
> Among its 130 lines about 50 are of `import' or of `open'.
> 
> Can you point at the reason of why splitting to small modules often
> reduces the type check cost?

As far as I understand how Agda works, writing out the A.agdai file
performs a sharing (``hash-consing'') step, so that equal terms
turn into identical ``pointers'' in modules (e.g., B) that load that
A.agdai file, which makes typechecking the material in B faster than
it would be if the content of B was instead appended to A.


> Can it happen so that splitting some other .agda file into two reduces 
> the type check cost for the last .agda file?

If the last file depends on all parts of the split module,
I know no possible reason for this, and from my experience,
I have no indication that this might happen.

However, if the last file depends only on some parts of a large module,
and some of the other parts pull in dependencies that are not needed
for the last file, then it is worth splitting those other parts off,
so that they don't occupy valuable heap space while Agda
is typechecking the last file.
(With +RTS -S, you can watch how much heap is occupied after
 ``Skipping ...'' ...)


Besides that, just split the file that takes too long.
Sometimes the gains are quite incredible!



Best regards,

Wolfram