<div dir="ltr">I would certainly appreciate the effort if this is properly merged into the next stable release!<div><br></div><div>I plan to use some of my proofs in a paper and it would be very disappointing if people needed to use a modified compiler to be able to verify them.</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-30 15:27 GMT+01:00 Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, Jun 30, 2017 at 3:14 PM, Jan Bracker <<a href="mailto:jan.bracker@googlemail.com">jan.bracker@googlemail.com</a>> wrote:<br>
> @Wolfram: That patch is amazing!<br>
> I patched it into the 2.5.2 stable release and it compiled the postulates<br>
> within a matter of seconds. Before the patch it wasn't done after 90+<br>
> minutes.<br>
> Is this going to be included in the release of 2.5.3? I hope it will be.<br>
> I do feel a bit of a twinge modifying the compiler to make my proofs type<br>
> check. I hope this does not introduce any inconsistencies or problems?<br>
> I rechecked all of my code and as far as I can tell none of my work takes<br>
> longer to compile. If anything it all appears to compile quicker now, though<br>
> I do not have actual numbers to back this up.<br>
<br>
</span>That patch is not planned to be merged, because it's more of an<br>
experiment. However if it helps so much it's tempting to try and do a<br>
proper job of comparing definitions without reducing them as much.<br>
<br>
It shouldn't introduce inconsistencies, it might however reject some<br>
programs that would otherwise be accepted, because it makes the<br>
typechecker heuristically assume things like:<br>
if (_A + _B) = (e1 + e2) then _A = e1 and _B = e2.<br>
<br>
while the program might need different solutions for _A and _B to typecheck.<br>
<br>
Best,<br>
Andrea<br>
<span class=""><br>
<br>
> I hope I don't hit another performance wall any time soon.<br>
><br>
> Best,<br>
> Jan<br>
><br>
> 2017-06-28 10:41 GMT+01:00 Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>>:<br>
>><br>
>> On 2017-06-27 17:09, Jan Bracker wrote:<br>
>>><br>
>>> I tried to add the last postulate I need, but even though I now have<br>
>>> marked all of the proofs as abstract the compilation time is again at<br>
>>> 30+ minutes with no end in sight:<br>
>><br>
>><br>
>> Some other things to try:<br>
>><br>
>> * Use copatterns to define records.<br>
>><br>
>> * Turn off η-equality for record types.<br>
>><br>
>> (I don't know if either of these things will help.)<br>
>><br>
>> --<br>
>> /NAD<br>
><br>
><br>
><br>
</span>> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>