coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Debugging an apparently diverging Coq program

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
Date: Sat, 21 Sep 2019 10:11:50 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay11.mail.gandi.net
Ironport-phdr: 9a23:GHZXjh+yzdkBq/9uRHKM819IXTAuvvDOBiVQ1KB31e4cTK2v8tzYMVDF4r011RmVBN6dsakP0rCH++C4ACpcuMzH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjfu8UMn4dvJKk9xgbXrnZMZu9awX9kKU+Jkxvz+8u84oRv/zhMt/4k6sVNTbj0c6MkQLJCET8oKXo15MrltRnCSQuA+H4RWXgInxRLHgbI8gj0Uo/+vSXmuOV93jKaPdDtQrAvRTui9aZrRwT2hyoBKjU07XvYis10jKJcvRKhuxlyyJPabY2JKPZzeL7WcNUHTmRDQ8lRTTRMDJ6iYYsBD+QPPuhWoIfyqFQMsRSwChKhBP/sxzJSmnP6waM33uYnHArb3AIgBdUOsHHModv0LqgVTfy1w7POzTrbbv1W2DP955PWfRA7vfGHQLV9ccXLxkYxCwPKlFOQpZbqPzOU0uQCqHaU7/B8Ve+0kG4nqAFwoiOsxsctj4nJg5waykre+SV/3ok1OcS1RUhmatCqF5tQsjuVN4pwQs46TGFouTo6yr0buZGgZiQF1JMnxxvZZveacIaI+gruWPiMLTp6nn5oeq6ziwyv/UWiyeDwTNe43VhXoiZdj9XAqnQA2wbN5sSbVPdx5Fqt1SqN2gzJ6uxJJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lLWWeVsg+uey6+Xrf6jqqoWZN4BuiwH+Nr4imsOlDuQ+LwcOXnKX+eKi273/5UH5QbNKgeMqkqTBrpzWOMYWqrS7DgNJyIov9hSyAjS83NgGk3QLMUpJeBedgIjoP1HOLur4DfC6g1m0nzdk3e7JPqH7DZXLNHTDn7bhfbJm5EFC0goz0ctS54lXCrABO/LzWU7xtNndDhAnKQy42eDnB8th1o8GQ2KAHreZML/OsV+P/u8gP+6MZJYMtDnhL/gl+uXhgGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7nhj0THWjpObV6zWbg973c1EtGIF4DGE6+kA6CI2hCUH5lca3paQgSDGHr0foPCVPYIYi+IPud6kS0fVrmkToI7kxejqFmpmPJcMuPI93hA5trY399v6riLzEBgxXlPF82Yllq1YSRxl2IMSSUx2fkh81d+20yA0K19juYeE9FPtaoQDlUKcKXExuk/MOjcHxrbd47XGk2lU86lADQ0Q8h3xdISMR4kRoeSyyvb1i/vOIc70ryGAJturvDG0nz4Np8kjXPP1a1ngFAgTsoJM2C61PZy

Because atomeq_dec is a parameter normalizing means you normalize and keep both branches when it's involved. Since it's involved in termination (when you Subst on graft) it also gets into the Program-generated parts. This may quickly become huge.

Gaëtan Gilbert

On 21/09/2019 02:13, William J. Bowman wrote:

All,

At the following URL is a model of a language with capture-avoiding
substitution
that a student wrote:

https://gist.github.com/wilbowma/acf125222c64ff715a33b26a0ce8b4ab

The program looks (to me) like it ought to terminate quickly, and it's proven
terminating using Program, yet when we run the substitution function on a
small
example... coqtop eats about 20 GB of memory and doesn't terminate within 5
minutes.
I'm using Coq 8.9.1 on MacOS 10.14.2; the same behavior is also observed on
Windows 10.

I'd appreciate any help debugging this.

--
William J. Bowman

Re: [Coq-Club] Debugging an apparently diverging Coq program, (continued)
- Re: [Coq-Club] Debugging an apparently diverging Coq program, Gaëtan Gilbert, 09/21/2019