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

[Philip Wadler]

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

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 9 May 2018 at 12:14, Ulf Norell <ulf.norell at gmail.com> wrote:

>
> 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/20180510/6afa3f04/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180510/6afa3f04/attachment.ksh>