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

[Philip Wadler]

Thanks! If I write this up, I will use those numbers. Take this as an
indication that revising the system to exploit sharing would be valuable.
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 16 May 2018 at 10:30, Ulf Norell <ulf.norell at gmail.com> wrote:

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