normalization-bench

normalization-bench copied to clipboard

Testing out Coq / native_compute with flambda

3

> It's worth noting that native_compute performs significantly worse than OCaml HOAS, though the two should be similar; probably native_compute does not use flambda optimization options at all. Indeed, the...

JasonGross

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

8

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...

JasonGross

Throwing more memory at Coq

5

According to https://github.com/coq/coq/issues/11277, the right way to tweak Coq's GC is to use the environment variable `OCAMLRUNPARAM` (see https://caml.inria.fr/pub/docs/manual-ocaml/runtime.html). You can also tweak Coq's stack limits via `ulimit -S -s`,...

JasonGross

Forcing normalization in Coq

7

> We use this because I was not able to find a good direct way in Coq to force normalization of large Church trees, because `Eval compute` will attempt to...

JasonGross