What is the benefit of flambda for Coq? Should the website installation instructions suggest by default that users installing OCaml & opam for the first time use a version of OCaml with flambda, and provide a command line?
Flambda makes Coq faster, say 10-20%. It can also make native_compute compilation slower (I've benchmarked it a bit in the past) — and probably native_compute execution faster (untested)
I think we've seen report where flambda + native_compute doesn't work — they're hopefully exceptions but I haven't tested myself and forgot the details
The speed ups without flambda varies, but IIRC I've seen around 15-20%
So I've chosen flambda native-compiler=no around 2019, stuck with it, and happily deployed it in Bedrock — that's not enough evidence for all of Coq userbase, and definitely not for native_compute users, but it's some data.
I think even Docker images might offer/default to flambda nowadays?
Last updated: Nov 29 2023 at 21:01 UTC