normalization-bench
normalization-bench copied to clipboard
AndrasKovacs
Coq results should have separate cases for cbv, lazy, and vm_compute (and maybe native_compute)
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.
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?
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?
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).
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.
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.
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.