[Agda] Type-checker evaluator performance

[Liam O'Connor]

For those that are interested, I took Ulf’s performance suggestions into account, and designed a new version of the whole library. Properties are now defined as a boolean test plus a proof to recover its provenance as Ulf suggested. Because these properties are also a monad[plus]/applicative/functor, most of my code can be unchanged. I also switched to pairs without eta throughout the library.

The performance improvement is drastic. Every example is faster. The slow petersons example now just takes less than two minutes and doesn’t even hit my swap :) 

Thanks Ulf! 

--  
Liam 

On 4 February 2016 at 8:55:54 PM, Nils Anders Danielsson (nad at cse.gu.se) wrote:
> On 2016-02-03 20:10, Sergei Meshveliani wrote:
> > Can you tell, please: how to turn on interactive highlighting?
>  
> Open an Agda file. Type "M-x cutomize-group RET agda2-highlight RET". Go
> to the "Value Menu" for "Agda2 Highlight Level". Select "Interactive".
> Go to "State". Select "Set for Current Session" or "Save for Future
> Sessions".
>  
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>