<div dir="ltr"><br><div class="gmail_extra"><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><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.<br><br></div><div class="gmail_quote">/ Ulf<br></div><div class="gmail_quote"><br></div></div></div>