[Agda] memory eagerness

[Wolfram Kahl]

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). 
>

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

 agda +RTS -S -M6.5G -H6.5G -K200M -RTS ...

 With -S you see what is happening; with -H you force the whole
 space to be there for the heap from the beginning,
 avoiding gazillions of tiny allocations and garbage collections.

 Also run htop (http://htop.sourceforge.net) to see what else is going on.

 In extreme cases, don't start X; instead work in the console
 using possibly

     http://jfbterm.sourceforge.jp/
     The J Framebuffer Terminal/Multilingual Enhancement with UTF-8 support

 to be able to give perhaps 7.4G to Agda...
)

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.

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...


> [...]
>
> Concerning the style, I see the following points.
> 
> 
> 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.


> 
> 2. open, open - public
> ----------------------
> 
> There are many levels in this record hierarchy (may be, 15-20).
> I apply  `open' and `open - public'  in order to have a shorter
> path from the top level to an operation on a lower level.
> For example, the path to reach  _+_  from  Field  is
>   EuclideanRing   --> IntegralRing --> RingWithOne -->
>   CommutativeRing --> Ring         --> Ringoid     -->  _+_
>   
> I do not know, may be something large is copied due to this 
> nested `open' declarations
> -- ?

For re-exporting interfaces from local modules, it seems that

  open X public

is mostly harmless, but

  open X public using (a ; b ; c)

is definitely not harmless, and

  open X public hiding (a ; b ; c)

is almost certainly not harmless, either.

I found it useful to keep that in mind when constructing
my interfaces --- if ``X'' is large,
name the pieces you will want to re-export separately,
and compose X from these pieces.


Hope this helps!



Wolfram