[Agda] Type-checker evaluator performance

[Andrea Vezzosi]

Did you introduce parametrized modules during the cleaning-up?

If so you might have introduced problems similar to this issue:

https://github.com/agda/agda/issues/1625

Also, if you turn on interactive highlighting you'll get to see
approximately on which expression time is being spent during
typechecking.

Best,
Andrea



On Mon, Feb 1, 2016 at 9:46 AM, Liam O'Connor <liamoc at cse.unsw.edu.au> wrote:
> Hi all,
>
> I’m currently using the development version of Agda, and I’ve been working on using the evaluation in type checking to embed proof search procedures inside Agda.
>
> https://github.com/liamoc/me-em
>
> Now, one of the applications of this technique is a model checker for a fragment of CTL on the guarded command language (*).
>
> Here is an example, where I use the model checker to verify peterson’s synchronisation algorithm.
>
> https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L91
>
> Before I cleaned this code up and put it on GitHub, it was all in one file. I can affirm that I was able to type check the code then. Today, after splitting it into multiple files, and cleaning it up a little bit, 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.
>
> Going back to the original, single-file version, it now also fails to finish checking and gets OOM-killed, so perhaps the multiple-files thing isn’t causing the issue.
>
> (Perhaps I just used a bit of disk space and now it’s running out of swap).
>
> Anyway, I’ll try this on a machine with more memory (RAM and swap) later, but is there any plan to improve performance (both in time and space) of the type-checker evaluator? I appreciate that what I’m trying to do is not something which it was designed to handle, but it _was working_ at some point.
>
> BTW, it seems to make no difference whether I use sharing or not, but when I got it to successfully check yesterday it was using sharing.
>
> (*) If you’ve seen the paper I wrote on this, note that the model checker is substantially different now.
>
> (*) Also note that originally the definition for petersons-search read:
>
> petersons-search
>    = search $
>        and′ mutex? (and′ sf? termination?)
>        (model petersons initialState)
>
> but I gave it a fixed depth of 25 just to stop it doing any unnecessary searching.
>
> Liam
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda