<div dir="ltr">Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it works now! A big thank you to Ulf and Wen for their help. -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 9 May 2018 at 12:14, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><span class=""><div class="gmail_quote">On Wed, May 9, 2018 at 3:32 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Ulf,<div><br></div><div>Any further progress with this?</div><div><br></div><div>Wen downloaded HEAD, but cannot execute even four steps of reduction on his 2010 MacBook Pro. </div><div><br></div><div>I have not downloaded HEAD (I'm cautious about Agda updates because if I break Agda I'm on my own trying to fix it). With the version below, four steps of reduction takes five minutes, and full reduction does not complete overnight.</div><div><br></div><div>I'm wondering if perhaps the issue is not version of Agda but available memory? How much is on your machine?</div><div><br></div><div>Any other progress at tracking down what the issue might be?</div></div></blockquote><br></div></span><div class="gmail_quote">I'm all but certain that the issue that makes it slow on 2.5.3 is call-by-name. Development Agda has call-by-need.<br></div><div class="gmail_quote">I've tracked down the mysterious issue that made some cases check fast and others not. The problem was that<br></div><div class="gmail_quote">we accidentally reverted back to call-by-name evaluation in some situations. I have a patch that just needs some<br></div><div class="gmail_quote">testing before deployment.<br><br></div><div class="gmail_quote">It's not a memory issue. Type checking the file that executes all the way to normal form requires less than 400M.<br></div><div class="gmail_quote">My suspicion is that there's a path issue or similar making Wen still run an old Agda. It would be helpful to see the<br></div><div class="gmail_quote">result of running<br><br></div><div class="gmail_quote"><span style="font-family:monospace,monospace">agda --version<br></span></div><div class="gmail_quote"><span style="font-family:monospace,monospace">agda Test.agda +RTS -s<br></span><br></div><div class="gmail_quote">on this Test.agda:<br><br><div style="margin-left:40px"><span style="font-family:monospace,monospace">module Test where</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">open import Agda.Builtin.Equality</span><br><span style="font-family:monospace,monospace">open import Agda.Builtin.Bool</span><br><span style="font-family:monospace,monospace">open import TypedFresh</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">isNormal : ∀ {M A} {⊢M : ε ⊢ M ⦂ A} → Normalise ⊢M → Bool</span><br><span style="font-family:monospace,monospace">isNormal (out-of-gas _ _) = false</span><br><span style="font-family:monospace,monospace">isNormal (normal _ _ _) = true</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">proof : isNormal (normalise 15 ⊢four) ≡ true</span><br><span style="font-family:monospace,monospace">proof = refl</span><br></div><br></div><div class="gmail_quote">For reference, if I have up-to-date interface files for the imported modules, this takes 3s and <400M memory<br></div><div class="gmail_quote">on my machine with Agda version 2.6.0-20c3e9d.<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888"><div class="gmail_quote">/ Ulf<br></div><div class="gmail_quote"><br></div></font></span></div></div>
</blockquote></div><br></div>