[Agda] Type-checker evaluator performance

[Liam O'Connor]

*doesn’t* stop my project in its tracks, pardon me.

--  
Liam 

On 2 February 2016 at 7:20:07 AM, Liam O'Connor (liamoc at cse.unsw.edu.au) wrote:
> Alright,
>  
> I was able to type check the file in about 10 minutes on a newish Macbook Pro with 16GB of  
> RAM — but it required basically all 16GB (about 15.5GB actually). Even a heap size of 14GB  
> was too small.
>  
> At least I know it works!
>  
> Now I’m still interested in improving these numbers, but at least this stop my project  
> in its tracks :)
>  
> --
> Liam
>  
> On 2 February 2016 at 5:48:20 AM, Liam O'Connor (liamoc at cse.unsw.edu.au) wrote:
> > Thanks for the detailed advice, Wolfram. Copied it into my org notes. If I limit the heap  
> > size it should stop it getting OOM killed anyway.
> >
> > 6GB doesn’t seem to be enough. I got heap exhausted after about 6 minutes. I’ll try a bigger  
> > heap size on a beefier machine tomorrow.
> >
> > I still think I’ve triggered a performance bug in Agda though. Before, this would run  
> > for 5-10 minutes and check without hitting OOM, and now it’s taking at least 10 minutes,  
> > usually longer, and running out of memory. Unfortunately I didn’t put the code in git  
> > when I had a working version, so I don’t have access to the working, pre-cleanup code  
> :/
> >
> > I’m beginning to suspect that I may not have ever tried to check this theorem after I introduced  
> > the parameterised modules for the CTL logic and the GCL language. It’s possible that  
> > doing this parameterisation has triggered the bug Andrea mentioned. I’ll try the patch  
> > provided and see if that helps.
> >
> > Worst case, I can remove those modules, but that would be an enormous pain, adding parameters  
> > to every definition.
> >
> > --
> > Liam
> >
> >
> > On 2 February 2016 at 5:28:42 AM, Wolfram Kahl (kahl at cas.mcmaster.ca) wrote:
> > > Hi Liam,
> > >
> > > I am not addressing your real concern, but this may still
> > > give you better chances of having your stuff type-checked in general:
> > >
> > > > I found that Agda would just get OOM killed before
> > > > finishing, and it would take at least 10 minutes before getting
> > > > OOM-killed, using all 8GB of my RAM and 4GB of my swap.
> > >
> > > I recommend to NEVER run Agda without specifying the heap,
> > > e.g.:
> > >
> > > agda +RTS -M6G -H6G -A128M -S -RTS -i . -i $(agdalib) MyModule.lagda
> > >
> > > (Also run htop in another terminal to see what is going on.
> > > http://hisham.hm/htop/
> > > )
> > >
> > > -M6G Maximal heap.
> > > With certain workloads, Agda will use any size of heap,
> > > even though it might also succeed with smaller size.
> > > And it does not know about your RAM and swap sizes...
> > > So even though your run used all of your 12G of RAM+swap,
> > > it may still succeed with -M6G. (But it also may not...)
> > >
> > > If you kill your firefox first, you may be able to go to 6.5G
> > > or even 7G. If you work without desktop environment, and preferably also without X11,  
> > > perhaps even 7.2G to 7.5G.
> > > A stopped firefox can be pushed out into swap, but a live firefox will fight back.
> > > (A swapped-out firefox takes ages to swap back in, so better kill it,
> > > and restore session later.)
> > > If you give Agda -M7.2G in your normal environment,
> > > it will push out everything else (that does not fight back sufficiently) into swap,  
> > > and if it succeeds, then run mostly happily.
> > > But don't move your mouse nor expect reactions from your terminals and window managers.  
> > > If you don't limit Agda's heap: Once Agda starts swapping its own pages,
> > > you can forget it: Kill it.
> > >
> > > -H6G Start heap: If your Agda process is going to be big anyway, give it that start heap.  
> > > You will see that it does not ask for all of it from the OS immediately,
> > > but only when it finds a use for it.
> > > For some small tasks (I believe including the standard library),
> > > Agda never uses a large heap.
> > > But if it does need a large heap, and you specified a smaller start heap
> > > (e.g. by not passing -H), the GHC RTS will waste quite some time growing it
> > > in small increments.
> > >
> > > -A128M Allocation area: Perhaps surprisingly, this makes my Agda runs much faster,  
> > > by taking out the nervousness from the garbage collector.
> > > On my 16G machines, I normally run +RTS -M10G -H10G -A1G -S -RTS.
> > >
> > > -S (only when running from the command line):
> > > See how much heap is live after each garbage collection.
> > > If you see it doing major (i.e., generation 1) garbage collections all the time,
> > > just below the max heap size, it is spending fmost of its time garbage collecting,
> > > and not getting any work done; then it is normally only going to be a question of time  
> > > (minutes to hours) until it runs out of heap, so you might just as well kill it,
> > > and restart it with more heap if possible.
> > > Another pattern I am seeing occasionally: It grows the live heap extremely slowly,  
> > > doing only minor collections for hours. This tends to be deadly;
> > > I have had it run for a week until it ran out of 50GB heap.
> > >
> > > I have recently only used Agda as 64-bit executable; I have modules that need 5G,
> > > 6G, 8G, 9G, 10G, 11G, 13.5G. I have occasionally run Agda in heaps as large a 256G,
> > > but so far have never seen anything typecheck that didn't also check with just 14G.  
> > >
> > >
> > > Hope this helps!
> > >
> > >
> > > Wolfram
> > >
> >
> >
>  
>