[Agda] memory eagerness

[Sergei Meshveliani]

Wolfram,
thank you for your notes. 

To my letter of  2013-05-06 
> On Mon, May 06, 2013 at 10:33:16PM +0400, Sergei Meshveliani wrote:
> > [...]
> > The longest one has about  250 lines  of a proper source code.
> > 
> > And it needs more than  6 Gb  memory to type check: 
> > 
> >   agda -c -i . -i $agdaStLib +RTS -K200m -M8000m -RTS Main.agda
> > 
> > (-M6000m  is not enough). 
> >

you respond:


> (How much memory does your machine have?
>  If it has only 8G, don't do -M8000m!
>  ``kill -STOP'' your firefox, and run

It has 16 Gb now! And I have given half of it.
But happiness is not in Gb-s! 
As this example takes more than 6 Gb to type-check,  further practical
examples will need much more than the machine has.

Various further  option tricks  with controlling memory will not help,
for the same reason
(-H looks good, in a certain sense).
On the other hand,  1 Gb  is quite a lot of memory for any reasonable
compilation.

Your experience with type-checking in  12 Gb  confirms my impression
that something essential needs to be improved in the type checker
implementation. 
Because you have already applied various precautions against the space
eating, and still have 12 Gb -- an awful size. 

> Agda typechecking performs a lot of evaluation/reduction,
> and the current reduction engine that is used for this
> does not implement the degree of sharing you might expect.

This is mentioned again. A naive user's wish to the  developers:  
please, do more sharing in the type checker!

> Sharing happens when interface files are written,
> but not while a single module is checked.
> For that reason, sometimes it makes sense to split a
> two-definition module into two one-definition modules...

I had modules of 600 proper lines; then I have split them voluntarily
(not by their sense!) to 300 lines each; this somewhat helped. 
Now, I need to divide them once more ... A suspicious activity.

> > 1. Record  vs  ordinary module
> > ------------------------------
> > 
> > For example, the record  Group
> > has a parameter :  UpMonoid c l
> > and a single       field  totalInversion : ...
> > 
> > There are also several related auxiliary functions 
> > (defined via the parameter and  field  totalInversion)
> > and their proved lemmata:
> >   division,  proof for  inv (x * y) == (inv y) * (inv x),
> >   for  inv (inv x) == x,   and such.
> > 
> > And I put all them into this very record, so that it exports them
> > (because a record is also a module).
> > 
> > Their code size is about 20 times larger than the proper Group 
> > record part. And it can grow further several times, because 
> > there are many useful lemmata about groups.
> > 
> > I think, so far, that this is a natural style. Is it?
> 
> I consider this natural, too, and followed this style for a long time.
> 
> But recently I had to remove large chunks of such code into separate modules
> to get my developments typechecked (in 12G...).
> 
> > Another design may be:
> > to create
> >    module Group-related (G : Group ...) 
> >    where
> >    ...
> > 
> > and move there the above Group related items, so that the proper 
> > Group  record will become a small code.
> > Will this approach save much space in the type-check?
> 
> It did in my case.
> 
> I also have what in your case is ``Group-related'' in a separate file,
> and actually have multiple such modules for different topics.
> 

My case is a bit more complicated:

  module GroupPack (upM : UpMonoid c l) 
    where
    <prelude using  upM>  

    record Group : Set _    
      where                    -- it uses  <prelude>
      <prelude-2>

           field  totalInversion : ...

      <lemmata for Group>      -- uses  <prelude>, <prelude-2>,
                               --       totalInversion. 

-- a parametrized module with a large  record Group  inside.
Now, I need to move a large part of  <lemmata>  to a separate file ...
Well, may be this is not difficult.

But look: you did all these tricks -- and still have 12 Gb in the type
check!  12 Gb is a very un-natural size for this. 
 
I shall see further. Thanks again,

------
Sergei