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

[Andrea Vezzosi]

On Fri, Jun 30, 2017 at 3:14 PM, Jan Bracker <jan.bracker at googlemail.com> wrote:
> @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.

That patch is not planned to be merged, because it's more of an
experiment. However if it helps so much it's tempting to try and do a
proper job of comparing definitions without reducing them as much.

It shouldn't introduce inconsistencies, it might however reject some
programs that would otherwise be accepted, because it makes the
typechecker heuristically assume things like:
if (_A + _B) = (e1 + e2) then _A = e1 and _B = e2.

while the program might need different solutions for _A and _B to typecheck.

Best,
Andrea


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