[Agda] Type-checker evaluator performance

[Jon Sterling]

I hope this isn't off-topic, but what's the state of the art for this?
Krivine machines?

Best,
Jon


On Mon, Feb 1, 2016, at 11:28 PM, Dominique Devriese wrote:
> Note that at the last Agda Meeting, there was a group of us who played
> with introducing a more efficient form of compile-time evaluation in
> Agda, but we basically didn't get it to work due to hard-to-track bugs
> that kept popping up and as far as I know, the work has not progressed
> since then...  My impression is that this will require a dedicated
> person with a few months' time on his hands...
> 
> See you,
> Dominique
> 
> 2016-02-01 21:21 GMT+01:00 Liam O'Connor <liamoc at cse.unsw.edu.au>:
> > *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
> >> > >
> >> >
> >> >
> >>
> >>
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda