[Agda] type check performance

[Sergei Meshveliani]

On Mon, 2015-03-30 at 11:37 -0400, Wolfram Kahl wrote:
> 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?
> [..]
> 
> 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.
> )
> 

1) I must have written 	`abstract'  instead of `private'.

2) Now I recall that splitting modules may help. I split the most
type-check-consuming module into two smaller ones. This only helps to
reduce the minimum from 9Gb to 8 Gb.

I apply
  agda -c $agdaLibOpt +RTS -S -K200m -M10G -RTS TestAll.agda >& log

on a Linux machine with  16 Gb memory.

Type check is about 10 minutes, compilation is about 50 minutes.
It reports 

 616,041,012,096 bytes allocated in the heap
 210,019,698,464 bytes copied during GC
   8,991,174,320 bytes maximum residency (77 sample(s))
     398,360,008 bytes maximum slop
           10450 MB total memory in use (0 MB lost due to fragmentation)
 [..]

Also the `top' command shows that  ghc  sometimes takes  98%  of the
16Gb memory despite this  -M10G.  The system hungs sometimes during this
process, swapping to disk.

The problem is: how to make this  TestAll.agda  install on a  8 Gb
machine in a reasonable way: at about the same expense as -M10G does.

Because "-M8G" works badly.

Thanks,

------
Sergei



  




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