[Agda] Type-checker evaluator performance

[Dominique Devriese]

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