The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

Thanks all for the feedback!

This should give me plenty of places to continue debugging and some 
workarounds
if it's simply a limitation of the code generated by Program.

--
William J. Bowman

PS: Sorry for my mis-sent empty email.

On Mon, Sep 23, 2019 at 07:36:54PM +0200, Xavier Leroy wrote:
> 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/ <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
> >
> >