[Agda] type check performance

[Wolfram Kahl]

On Mon, Mar 30, 2015 at 06:43:11PM +0400, Sergei Meshveliani wrote:
> I have a certain middle-size project, call it "FooLib library".
> I am going to publish it soon, but first it would have sense to try to 
> reduce its space eagerness.
> And I wonder how to reduce.
> 
> Its type check in  Agda 2.4.2.2  takes
>      
>     9G byte memory and  10 minutes  (on a 2 GHz machine),

What exactly do you mean by this?
I can imagine three meanings:

 (1) When running agda without RTS options,
     maximum memory usage reaches 9G

 (2) When running agda with +RTS -s -RTS (or -S),
      it reports maximum residency of 9G

 (3) When started with +RTS -M8.9G -RTS ,
     it runs out of heap or never finishes,
     but with 9G, it succeeds.

Since your type checking takes only 10 minutes,
I would guess that you mean (1),
and strongly recommend:

  +RTS -S -H10G -M10G -RTS

(only if you ave more than 11G physical RAM)
and watch how much heap it actually occupies during the run.
In particular observe the ``maximum residency'' reported at the end,
and if that is, e.g., 5.6G, then you should try your run with

  +RTS -S -H6G -M6G -RTS

, which is still marginally feasible on an 8G laptop running
a web browser at the same time.

(If you observe ``nervous garbage collection behaviour''
 with way below full heap, passing also something like
  -A32M
 may help, but I don't understand why,
 and so far needed it only for UHC.
)



> I know about the possibilities of 
> 1) with --> case,
> 2) using `private' for some proof pieces.

I think you mean ``abstract'', which I used for that purpose many
years ago. But then it got into my way, and by that time the gains
were almost negligible, so I abandoned that.


(At some point, ``open public hiding (...)'' was expensive,
 so I avoided it, but I made no experiments recently.)


Wolfram