Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
  • Date: Fri, 20 Sep 2019 17:35:38 -0700
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f51.google.com
  • Ironport-phdr: 9a23:PxwVPxFU1saL9XwyFwZVzZ1GYnF86YWxBRYc798ds5kLTJ7zoc6wAkXT6L1XgUPTWs2DsrQY0rGQ6furAjFIoc7Y9ixbKtoUD15NoP5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLucQanIVvJrwvxhbHrXdFdeRbzn5sKV6Pghrw/Mi98IN9/yhKp/4t68tMWrjmcqolSrBVEC4oOH0v6s3xshnDQwqP5n8CXWgTjxFFHQvL4gzkU5noqif1ufZz1yecPc3tULA7Qi+i4LtxSB/pkygIKTg0+3zKh8NqjaJbpBWhpwFjw4PRfYqYOuZycr/bcNgHQ2dKQ8RfWDFbAo6kYIQPAegOM+ZWoYf+ulUAswexCBK2C+/z0DJFnGP60bE43uknDArI3BYgH9ULsHnMsNj6L6cSUeGuzKnI0zrDbO5d1Cv76IfSdBAuvOyHULVqfsXKyUkvFhjFjlWOpozmJT+azOINvHKd7+V9T+6vim8nqx1+ojW0yccsj5PGhoMRylze6Sp5x4M1KMS+RUVmb9CkF55QuDubN4twWs4tX2ZouDw8yrIYvZ67eDIGx4o6yB7Cc/CHfImI4g7jVOaMOjh0nm5qeLW6hxu07EOuyfX8W9Gq3FpWqidJiNrBu3AX2xDO68WKS+Fx80e81TuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbGy/5gkT2jKuPekUl/eik9v3rYrvmq5OBLYN0hQb+MqMhmsy7H+s0KBQBX2+e+eik1b3j+1P2QKlSg/EojqXUtIrWKMcbq6KjHgNY04cu5wy/Aju7yNgYmGMILFNBeBKJlYjpPFTOLejiAvikg1SskSxrx/DYMb3iGJnCNH7Dn63nfblg8UJcyQszzcxQ559PBbEBJej8Wk71tNDCEhA5NAm0z/79CNphzoMeRX6PAqiBPazOtl+I//sjLPWIZI8IoznwMOMl5v7rjX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGRGwNp081SPHgwAmJVicWbHKvVYo94Cs6AcSoF9GQaJqqhemo1ie6BZ1bZShvDFmKHT+8fo+EWuwMZSHUK8lolDBCVLm9RKcu0BivsEnxzL8xfbmcwTERqZ+2jIs93ObUjxxnrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkwWM1KF5h7pTEtkBvqoUADd/DobVyqlBM/63Wg/FeY3UGlOvQ9HjADZoC9xsmpkBZEFyH9jkhRfGjXLzX+0l0oeTDZlxyZrymmDrLp8kmXnD3aglyVIhR5kXOA==

Perhaps they forgot to instantiate the atom type?  the computation would get stuck on (x == x'). `Program` often produces humongous functions.



On Fri, Sep 20, 2019 at 5:15 PM William J. Bowman <wjb AT williamjbowman.com> 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



Archive powered by MHonArc 2.6.18.

Top of Page