Jason Gross (Sep 13 2023 at 15:48): Jason Gross (Sep 13 2023 at 15:48):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?
Paolo Giarrusso (Sep 13 2023 at 16:16):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)
Paolo Giarrusso (Sep 13 2023 at 16:18):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
Paolo Giarrusso (Sep 13 2023 at 16:20):The speed ups without flambda varies, but IIRC I've seen around 15-20%
Paolo Giarrusso (Sep 13 2023 at 16:21):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.
Paolo Giarrusso (Sep 13 2023 at 16:21):I think even Docker images might offer/default to flambda nowadays?
Last updated: Nov 29 2023 at 21:01 UTC