<div dir="ltr">Hi,<div><br></div><div>and again thank you for the quick help!</div><div><br></div><div>@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.</div><div><br></div><div>@Wolfram: That patch is amazing!</div><div>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.</div><div>Is this going to be included in the release of 2.5.3? I hope it will be. </div><div>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?<br></div><div>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.</div><div><br></div><div>I hope I don't hit another performance wall any time soon.</div><div><br></div><div>Best,</div><div>Jan</div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-28 10:41 GMT+01:00 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2017-06-27 17:09, Jan Bracker wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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>
</blockquote>
<br></span>
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.)<span class="m_4182491594484273337m_-5216188789975381510HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div></div>