The Coq mailing list

[Nathaniel Yazdani <nyazdani AT cs.washington.edu>]

I’d second that suggestion. Especially with non-opaque obligation proofs, Compute can really spin out trying to aggressively reduce a stuck term like that.

Playing around with the linked Coq code, I got the problematic function call to normalize as desired using call-by-name evaluation, Eval cbn in $TERM, after flagging the six obligation proofs, Subst_func_obligation_{1,2,3,4,5,6}, as Opaque.

Nate

On Sep 20, 2019, at 8:35 PM, 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