[Agda] Possibly infinite/exponential compilation time by just calling a certain function

[Jan Bracker]

Hi,

and again thank you for the quick help!

@Nils: I tried turning off eta equality but that did not change a thing. I
did not try using copatterns, because it would have taken me a long time to
rewrite everything without being sure if it actually helps or which bit are
important to rewrite.

@Wolfram: That patch is amazing!
I patched it into the 2.5.2 stable release and it compiled the postulates
within a matter of seconds. Before the patch it wasn't done after 90+
minutes.
Is this going to be included in the release of 2.5.3? I hope it will be.
I do feel a bit of a twinge modifying the compiler to make my proofs type
check. I hope this does not introduce any inconsistencies or problems?
I rechecked all of my code and as far as I can tell none of my work takes
longer to compile. If anything it all appears to compile quicker now,
though I do not have actual numbers to back this up.

I hope I don't hit another performance wall any time soon.

Best,
Jan

2017-06-28 10:41 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se>:

> On 2017-06-27 17:09, Jan Bracker wrote:
>
>> I tried to add the last postulate I need, but even though I now have
>> marked all of the proofs as abstract the compilation time is again at
>> 30+ minutes with no end in sight:
>>
>
> Some other things to try:
>
> * Use copatterns to define records.
>
> * Turn off η-equality for record types.
>
> (I don't know if either of these things will help.)
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170630/86d399fc/attachment.html>