Coq results should have separate cases for cbv, lazy, and vm_compute (and maybe native_compute)

[JasonGross]

Kernel conversion uses something akin to lazy. The fastest normalization is probably vm_compute, unless you are starting from very small terms and ending up with very small terms, but have very large intermediate terms or very slow computations, in which case native_compute may be faster.

[gasche]

After looking at this repo (from the ping I received on the other issue), I was meaning to post exactly this: I think you should give results for Eval compute (I suggested cbv but see @JasonGross' comment below), vm_compute and native_compute. Maybe @JasonGross would be willing to submit a PR to do these three different things?

[JasonGross]

compute is an alias for cbv

[AndrasKovacs]

Is the following correct: we can test conversion checking with lazy (the default), vm_compute (when we use eq_refl x <: x = y) and native_compute (when we use eq_refl x <<: x = y), but we cannot directly test conversion with cbv/compute? BTW how is this casting implemented, what do we compare there for equality?

[JasonGross]

That's almost correct. We can test conversion checking with the lazy strategy (the default). We cannot test conversion with cbv/compute. We can normalize the types with either vm_compute (<:) or native_compute (<<:) and then compare them for syntactic equality (so eq_refl x <: x = y will normalize both x = x (the type of eq_refl x) and x = y via vm_compute and then compare these for syntactic equality; I'm not sure whether or not there's a readback phase, or if the equality checking is done in the VM).

[AndrasKovacs]

I added now all columns for the different evaluators.

Question: is there a way to do e.g. this

Time Definition foo_v2 := eq_refl t2M <: t2M = t2Mb.

without Definition, and would that matter? I tried to do this with Goal True as in your other cases, but for some reason I failed to type the eq_refl, the typed let-definition gave me syntax error.

[JasonGross]

What was the code that you used? You can do Goal True. let x := constr:(eq_refl foo <: bar) in idtac. It'll have a small impact (I think it might make hash-consing not happen?), but not a large one, I expect.

[AndrasKovacs]

Goal True. let x := constr:(eq_refl foo <: bar) in idtac requires me to have Set Nested Proofs Allowed, but then fails anyway with There are pending proofs: Unnamed_thm.

[JasonGross]

Both issues are caused by forgetting an Abort to close a Goal