Stream: Coq devs & plugin devs

Topic: flambda


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:20):

The speed ups without flambda varies, but IIRC I've seen around 15-20%

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 16:21):

I think even Docker images might offer/default to flambda nowadays?


Last updated: May 18 2024 at 10:02 UTC