The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Mon, Sep 23, 2019 at 7:19 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

have you tried to extract to ocaml or haskell to reduce noise from Prop?

"Program Fixpoint" produces terms that don't play well with extraction: https://github.com/coq/coq/issues/10757

The problem could come from accessibility proofs that don't compute.  The following trick can help: https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00034.html

- Xavier Leroy

 

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of William J. Bowman <wilbowma AT ccs.neu.edu>
Sent: September 20, 2019 8:46 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program

 

I don’t think that’s the problem. Another model does get stuck on that equality and returns the if statement waiting for an interpretation of “==“. I didn’t expect Program to be efficient, but I do expect it to terminate quickly on this example, without using 20 GB of memory.

I’ll see if I can reduce the other model to something as small.

-- 

Sent from my phoneamajig

On Sep 20, 2019, at 17:35, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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

-- Abhishek

http://www.cs.cornell.edu/~aa755/

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