[Agda] Type-checker evaluator performance

[Peter Selinger]

Also, Agda uses a normal order evaluator that is not lazy. For
example, any function that returns a pair will be evaluated twice. If
you use such a function recursively, the evaluation time will be
exponential. Also, if you write something like "let x = f y in (x , x)",
f will be evaluated twice. It's often very tricky to rewrite your
programs to avoid this effect, and even more tricky to prove
properties about them afterwards. In my experience, turning on
--sharing does not change this behavior. But maybe efforts are under
way to fix this?

-- Peter

Andrea Vezzosi wrote:
> 
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>