Ralf Jung (May 16 2022 at 08:42): Ralf Jung (May 16 2022 at 08:42):(Not a Coq question but an opam question; I hope that is okay.)
I am doing some experimentation with ocaml versions for performance on CI (since 4.07.1, the fastest version so far, cannot be used for latest Coq any more). I heard flambda helps so I'd like to use ocaml with flambda on CI. I know how to set that up with opam locally via opam switch create $SWITCHNAME ocaml-variants.4.14.0+options ocaml-option-flambda; but on CI we are setting up opam from scratch so it's opam init ... -- and there doesn't seem to be a way to specify two compiler packages when using opam init, or is there? And if not, how can I avoid first init'ing opam with ocaml-variants and then rebuilding everything after installing ocaml-options-flambda?
Gaëtan Gilbert (May 16 2022 at 08:45):init --bare then switch create seems like it would work
Ralf Jung (May 16 2022 at 08:47):ah, that is the option I was looking for (but somehow missed), thanks!
Théo Zimmermann (May 16 2022 at 08:54):Note that if you use Docker-Coq images, all the ones with recent OCaml versions have flambda.
Ralf Jung (May 16 2022 at 08:55):this is for our own gitlab-CI based CI
Théo Zimmermann (May 16 2022 at 08:57):Note that I didn't say Docker-Coq-Action here, but just Docker-Coq. GitLab CI supports Docker images pretty well and we even have some documentation with examples of use in a GitLab context ;-)
Théo Zimmermann (May 16 2022 at 08:57):https://github.com/coq-community/docker-coq/wiki/CI-setup#gitlab-ci-config
Paolo Giarrusso (May 16 2022 at 09:14):@Ralf Jung FWIW, Coq 8.15 uses flambda automatically, but opam packages for older Coq versions need to be patched: https://github.com/Blaisorblade/opam-overlay/tree/master/packages/coq
Paolo Giarrusso (May 16 2022 at 09:17):See e.g. https://github.com/Blaisorblade/opam-overlay/blob/72a2fa8e0cfb948bca2cb76b1dae5b201392d690/packages/coq/coq.8.14.0+flambda/opam#L45. For even older Coq versions you might want changes also to disable native-compiler (see those packages).
Karl Palmskog (May 16 2022 at 09:18):@Paolo Giarrusso how about submitting those packages to here: https://github.com/coq/opam-coq-archive/tree/master/core-dev
We can at least make the knowledge more easily accessible, even if they may not fit in the general OCaml opam repo.
Ralf Jung (May 16 2022 at 09:19):Théo Zimmermann said:
Note that I didn't say Docker-Coq-Action here, but just Docker-Coq. GitLab CI supports Docker images pretty well and we even have some documentation with examples of use in a GitLab context ;-)
fair. but we have a well-working CI setup that predates Docker-Coq so so far we haven't looked into what it would take to switch, and what we would gain/lose by doing that.
Ralf Jung (May 16 2022 at 09:20):Paolo Giarrusso said:
Ralf Jung FWIW, Coq 8.15 uses flambda automatically, but opam packages for older Coq versions need to be patched: https://github.com/Blaisorblade/opam-overlay/tree/master/packages/coq
what does it mean for Coq to "use" flambda? flambda means Coq is compiled to a faster-running binary, isnt it?
Ralf Jung (May 16 2022 at 09:21):but anyway the relevant projects are using 8.15 for benchmarks
Paolo Giarrusso (May 16 2022 at 09:28):@Ralf Jung those packages use something closer to ocamlc -O3. Installing ocaml+flambda means that flambda was enabled, not that it's used automatically.
Ralf Jung (May 16 2022 at 09:34):oh, I didnt know flambda needed double opt-in (first ocaml-option-flambda and then also a compiler flag). makes one wonder why.^^
Paolo Giarrusso (May 16 2022 at 09:51):That ocamlc needs a compiler flag seems standard (like gcc/clang/ghc), builds with optimizations are slower after all. Why flambda is disabled altogether by default — that I don't know.
Ralf Jung (May 16 2022 at 09:53):when gcc/clang/etc gain a new optimization it is usually enabled by default though, it doesnt need something like -flambda-opts or -unbox-closures
Ralf Jung (May 16 2022 at 09:54):but anyway, looks like I dont have to worry about this with latest Coq so thats good. :-)
Last updated: Sep 28 2023 at 10:01 UTC