[Agda] How does one debug a programme that one has proved correct?

[Ulf Norell]

On Wed, May 9, 2018 at 3:32 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> Ulf,
>
> Any further progress with this?
>
> Wen downloaded HEAD, but cannot execute even four steps of reduction on
> his 2010 MacBook Pro.
>
> 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.
>
> I'm wondering if perhaps the issue is not version of Agda but available
> memory? How much is on your machine?
>
> Any other progress at tracking down what the issue might be?
>

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.
I've tracked down the mysterious issue that made some cases check fast and
others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.

It's not a memory issue. Type checking the file that executes all the way
to normal form requires less than 400M.
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
result of running

agda --version
agda Test.agda +RTS -s

on this Test.agda:

module Test where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh

isNormal : ∀ {M A} {⊢M : ε ⊢ M ⦂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true

proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl

For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180509/48b424ba/attachment.html>