Testing out Coq / native_compute with flambda

[JasonGross]

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 Coq packages I've provided don't use flambda, but it's possible install OCaml via opam with flambda support / optimizations, and then build Coq (/ install Coq on opam?) with flambda, which should automatically translate to the native compiler. Coq's INSTALL.md suggests installing ocaml version 4.10.0+flambda.

@ejgallego and @maximedenes might be interested in this benchmark

[ejgallego]

The native compiler will not call flambda with optimization, see this code in nativelibs

  let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in

you would like to use something such as -O3 -funbox-closures ; this is quite expensive in terms of compilation time; native also uses some internals of OCaml that could make the above flags not work.

[JasonGross]

Also, @AndrasKovacs it's not clear to me whether your times include compilation time or just runtime, for the compiled languages. The timing on native_compute includes both. In Coq 8.12, you can see a breakdown via Set NativeCompute Timing. In older versions of Coq, you could pass -debug to coqc, but you'd get somewhat useless times, as it would report user times rather than real times. See also https://github.com/coq/coq/pull/11963

[AndrasKovacs]

@JasonGross testing native_compute with expressions like (const n10 t8M) ran in about 70ms (perhaps there's some caching going on in aux files?), which suggests that compilation does not significantly change the results. This is something though which I should mention in the docs.