[Agda] Type-checker evaluator performance

[Jacques Carette]

Where can one read more about "no-eta-equality" ?  I believe that some 
of my work could benefit from this as well.

Similarly, I sought to learn from the changes you did
https://github.com/UlfNorell/me-em/commit/5930ad6b155244a1ba85abc36a0e79c1333ca7f4
but while I can "read the code", I can't quite understand how this 
matches your high-level description.  Could you comment a bit about 
this?  I believe that this would be well worth it, and may indeed help 
achieve a reduction in Agda-blame, as outlined in the first paragraph.

Jacques

On 2016-02-03 04:31 , Ulf Norell wrote:
> I think it's unfortunate, if perhaps not completely undeserved, that 
> Agda gets blamed every time a program is slow or uses a lot of memory. 
> When people are writing slow Haskell programs their first thoughts are 
> "maybe I should try to optimise my program", not "maybe someone should 
> optimise GHC" and I wish we could have a little more of that for Agda 
> programs. There are certainly performance problems in Agda's compile 
> time evaluator (call-by-name, interpretation overhead, etc) but that 
> doesn't mean that you can't write programs that perform reasonably well.
>
> I had a look at your code and the main performance problem seems to be 
> that you are too strict in the proof objects produced by the model 
> checker. In your example the correctness proof of Peterson's algorithm 
> consists of four (I think) complete state graphs (with ~14k states) 
> decorated with proofs that you build up eagerly before deciding that 
> you have a valid proof. If you instead separate the decision procedure 
> from the construction of the proof object you only need to run the 
> former to be sure that you have a proof, and can evaluate the latter 
> lazily as you need it. I forked [1] your repo and tried this out. The 
> Examples module checks in 26s and uses 900M memory on my machine. 
> Another thing I tried is to use a pair type without eta equality for 
> the models (in my experience eta equality and call-by-name is a major 
> source of inefficiency). This saves you another 30% time and space.
>
> / Ulf
>
> [1] https://github.com/UlfNorell/me-em
>
>
> On Mon, Feb 1, 2016 at 9:46 AM, Liam O'Connor <liamoc at cse.unsw.edu.au 
> <mailto: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 <mailto: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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160203/0659c48d/attachment.html