Stream: Coq users

Topic: Setup opam with ocaml-flambda


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

view this post on Zulip Gaëtan Gilbert (May 16 2022 at 08:45):

init --bare then switch create seems like it would work

view this post on Zulip Ralf Jung (May 16 2022 at 08:47):

ah, that is the option I was looking for (but somehow missed), thanks!

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

view this post on Zulip Ralf Jung (May 16 2022 at 08:55):

this is for our own gitlab-CI based CI

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

view this post on Zulip Théo Zimmermann (May 16 2022 at 08:57):

https://github.com/coq-community/docker-coq/wiki/CI-setup#gitlab-ci-config

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

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

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

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

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

view this post on Zulip Ralf Jung (May 16 2022 at 09:21):

but anyway the relevant projects are using 8.15 for benchmarks

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

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

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

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

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC