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

[Ulf Norell]

I believe the problem you've run into is that we don't have explicit
sharing in the
internal terms. The normal form of `normalise 100 ⊢four` is small, but the
weak-head
normal form is huge, and the type checker compares terms for equality by
successive
weak-head reduction steps. The lack of explicit sharing means that
evaluation won't be
shared across reduction steps.

Here are some numbers:

n   size of whnf of `normalise n ⊢four` (#nodes in syntax tree)
1   916
2   122,597
3   53,848,821
4   ??
100 ????

/ Ulf


On Wed, May 16, 2018 at 12:07 AM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> Ulf, Thanks again for your help. It is a great relief to be able to
> execute my proven-correct code!
>
> But there seems to be a further issue. Executing `normalise 100 ⊢four`
> terminates quickly. However, if I paste the result into the file and ask
> Agda to check that `normalise 100 ⊢four` is equal to the result of its own
> execution then type checking still takes forever to terminate (where
> "forever" means "longer than five minutes"). I expect this corresponds to
> some spot where call-by-name is still used instead of call-by-need.
> Fortunately, it is not on my critical path, but I thought I should alert
> you to the issue.
>
> I've attached the code, or you can find it at https://github.com/
> wenkokke/sf/src/.
>
> Cheers, -- 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 10 May 2018 at 18:35, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>
>> 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
>>>
>>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/eaf7a736/attachment.html>