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

[Philip Wadler]

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
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/9503756d/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TypedFresh.lagda
Type: application/octet-stream
Size: 37824 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/9503756d/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Collections.lagda
Type: application/octet-stream
Size: 6501 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/9503756d/attachment-0001.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/9503756d/attachment.ksh>