coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Debugging an apparently diverging Coq program

From: "William J. Bowman" <wjb AT williamjbowman.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Debugging an apparently diverging Coq program
Date: Fri, 20 Sep 2019 17:13:52 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=None smtp.mailfrom=wjb AT williamjbowman.com; spf=None smtp.helo=postmaster AT williamjbowman.com
Ironport-phdr: 9a23:LoofwxdAVpURYtPNq9BjBT5FlGMj4u6mDksu8pMizoh2WeGdxcSyZR7h7PlgxGXEQZ/co6odzbaP6Oa6Aidbud7B6ClELMUWEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/JKs90AXFr3VHd+lY2W9jOFafkwrh6suq85Nv7jpct+g9+8JcVKnxYrg1Q6FfADk6KW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndaU81PSyJOHJ+zb4oXD+oAI+lYqZX9p0ATphe6HAWgGf/jxiNNinLwwKY00fkuERve0QIuH9wArmnaotb6O6gOTO+6wrLFzSnfY/5MxTvx9JLFfg4nrPqRXbxwa83RyUw3Gg/LjlqQqIjlPzeU1usXtmiQ8u5uWfiygGM6rAFwrD2vyd0qioXHm4kYzV7F9Sdiz4suK9y4SUp7YdqlEJRKsiGaNZB5QsQsQmFtoik6zKcKtoK8fCgP0ZkqwQPUZfKAc4iN+B3jVeCRLC93hHJkZLK/hwuy/lO6xuLgUcm01VBHpTdGnNnUrn0Byhje5tadRvdg/kqs2SyD2gPQ5+1ePEw4iKvWJ4Y8zrM0lZcfq1nPEy7olEnsjKKbdl8o9+uo5unhf77ovIWTN5VuhQH7KqkumtKwAeA/MgUWUWmb+OC81Lni/ULjRbVKjOY5kq7XsZDfP8sboLS1DBNS0oYm8xq/DjGm38oEnXQfMV5IfAyLg5L0N1zOIP30F/Syjle2nDt22vzLP6XtApDXIXjClLfhc6x960lZyAcrw9Ff5YlbB6oPIfLyXk/xsN3YAQU8Mwy22OnnD9t81oYEVmKJGKOWLKTSsVqQ6uI1P+aMfJMVuCr6K/U9+/HuimY5lUYBcqmtwJsYc2u1Hu9mIkWceXrjmM0NEWYMvgokTezlkkeOUTBJZyX6Y6VpzTYiQKmiEI2LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDr0zaSaWI8Zk2h5CHZKmVIoo01vm4BD4wZJ4L+7Q+yQdt5jky9184avYkhRkpm88NNiUz2zYFzI8pWgPXTJjmfkn+RUhmGfG6rBxhrljLfIW/+lACF9oKp/Yy+1zDtL4XR3Ed9HPQ1GjEI3/UGMBC+kpytpLWH5TXtCrjxTNxS2vWedHiL2PAJ0996DW2Gf0LsA7wHHDhvF40gsWB/BXPGjjvZZRsgjeA4mTyxeGlqKudK0Z3iTK62KKyyyFu0QKCAM=

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

[Coq-Club] Debugging an apparently diverging Coq program, William J. Bowman, 09/21/2019
- Re: [Coq-Club] Debugging an apparently diverging Coq program, Abhishek Anand, 09/21/2019
  - Re: [Coq-Club] Debugging an apparently diverging Coq program, Nathaniel Yazdani, 09/21/2019
  - Re: [Coq-Club] Debugging an apparently diverging Coq program, William J. Bowman, 09/21/2019
    - Re: [Coq-Club] Debugging an apparently diverging Coq program, Jason -Zhong Sheng- Hu, 09/23/2019
      - Re: [Coq-Club] Debugging an apparently diverging Coq program, Sylvain Boulmé, 09/23/2019
        
        Re: [Coq-Club] Debugging an apparently diverging Coq program, Sylvain Boulmé, 09/23/2019
      - Re: [Coq-Club] Debugging an apparently diverging Coq program, Xavier Leroy, 09/23/2019
        
        Re: [Coq-Club] Debugging an apparently diverging Coq program, William J. Bowman, 09/23/2019
        
        Re: [Coq-Club] Debugging an apparently diverging Coq program, Pierre Courtieu, 09/24/2019
  - Re: [Coq-Club] Debugging an apparently diverging Coq program, Jason -Zhong Sheng- Hu, 09/21/2019