The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi Matthieu,

from experimenting a bit with this:

It the term I run my function on contains a nat which is given as a Section Parameter native_compute takes a few seconds and then fails with

Warning: Native compiler exited with status 127

[native-compiler-failed,native-compiler]

Error: Anomaly "Compilation failure."

Please report at http://coq.inria.fr/bugs/.

vm_compute computed for about 20 minutes and then the whole process just crashed because it ran out of memory.

If instead a fixed nat is used in the term then vm_compute as well as simpl and Compute handle the reduction pretty much instantly however native_compute also fails with the above error.

Not sure what to make of this though...

Cheers,

Merlin

Matthieu Sozeau <mattam AT mattam.org> schrieb am So., 28. Jan. 2018 um 11:24 Uhr:

Hi Merlin,

There might be many factors to slow computation, e.g. representation of data types, proofs in terms, mismatch between your assume evaluation strategy and the one implemented by Coq’s reduction functions. You might first want to try vm_compute or native_compute to have an idea if it is your encoding or just Coq’s relatively naïve default evaluator that is the culprit.

My 2 cents,
— Matthieu

Le dim. 28 janv. 2018 à 10:15, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :

Hi,

I have a complicated computation on which Coq takes a very long time (or never terminates?) to execute (Compute statement or simpl in interactive proofs) even on rather simple inputs (extremely simple inputs terminate immediately though).

Is there some option to debug what Coq is currently doing, similar to Set Typeclass Debug?

Or what is the recommended way to hunt down such complications?

Cheers,

Merlin