The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Eval hnf does fixpoint refolding, using the same algorithm as simpl (or cbn), I believe.  If you can figure out which fixpoint refolding is causing an issue, you can try to modify the definition of the fixpoint (e.g., try moving all section arguments to arguments of the fix, try moving the body of the fix to its own definition), or you could try marking various constants as opaque.

On a more mundane note, it's probably quite easy to get arbitrarily large terms under hnf which are small under lazy, e.g

let ... in .. creating a term that's exponential in the number of let's when inclined, followed by a constructor applied to an argument that let-binds the final outside let binder and then drops the variable and returns a small constant.

On Thu, May 23, 2019, 00:19 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I am trying to produce a definition by computation. 

`Eval lazy` and `Eval compute` finish within 3 seconds.

But `Eval hnf` never returns, at least not within 10 minutes. The memory consumption also grows gradually to 15GB at 10 minutes. My computer has at least 10 additional GB free.

Could this be a bug? "Eval hnf" is asking Coq for less work than "Eval compute"; so it is surprising that "Eval hnf" takes much more time and memory.

Is there a workaround?