Integrate dune 3.8.1 as soon as possible

[erikmd]

Namely, when dune.3.8.0 goes live in opam: https://opam.ocaml.org/packages/dune/

Related: ocaml/opam-repository#23814
& https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs-.26-users/topic/Dune.203.2E8.20with.20Coq.20composition.20in.20CI/near/361264335

[Alizter]

It is now available in opam repo. So far there have only been two bugs reported both not affecting the platform.

• Dune crashes when looking for COQ_NATIVE_COMPILER_DEFAULT when it is missing in Coq < 8.13.
• Dune does not know how to handle COQPATHs with overlapping theory prefixes. This only affects mathcomp users on nix ATM.

[erikmd]

Hi @Alizter, OK thanks!

Dune crashes when looking for COQ_NATIVE_COMPILER_DEFAULT when it is missing in Coq < 8.13.

Does this mean that dune.3.8.0 is incompatible with 8.4 ≤ Coq ≤ 8.12 ?

In which case, I'm afraid we cannot do the bump now, given dune is installed in the same base image used for any Coq version, only specialized w.r.t. the ocaml version.

[erikmd]

@Alizter

COQPATHs with overlapping theory prefixes

can you be more specific? you mean coq packages that install to the same folder …/user-contrib/mathcomp/?

anyway, could you link to the issue(s) on this bug if there are already some?

[Alizter]

For the native compiler issue we have ocaml/dune#7846. This will only be triggered when the coq.theory stanza does not have a mode set. There will be a fix for this in 3.8.1. ocaml/dune#7847 The issue stems from dune asking for coqc --config and looking for the variable and failing.

The COQPATH issue is as you describe. However this only affects how we package things in nix. When you have say mathcomp/ssreflect and mathcomp/algebra installed in user-contrib (as opam will do) this is not a problem. However when we look for directories in COQPATH, dune will currently think there are two conflicting theories named mathcomp. This is a bug and I hope to fix it for 3.8.1 as well, but it shouldn't be a problem for the platform. ocaml/dune#7790

[erikmd]

OK! so I'd say, let's wait for 3.8.1 👍

[Alizter]

@erikmd 3.8.1 has been released and is in opam. There are a few more bugs to fix for 3.8.2 but they shouldn't affect anything here.

[erikmd]

@Alizter thanks a lot for your heads-up / reactivity / valuable feedback!

[erikmd]

FYI: the first coqorg/base pipeline is on-going; stay tuned.

[erikmd]

FYI: the second coqorg/coq pipeline is on-going; stay tuned.

[erikmd]

After necessary tweaks by @Zimmi48 in coqbot to workaround random failures at docker pull time in gitlab.inria.fr,
the third mathcomp/mathcomp pipeline went fine.

And I updated the list of supported tags accordingly
https://hub.docker.com/r/mathcomp/mathcomp#supported-tags
— Thanks @proux01 for raising that documentation issue; I've just added a comment in the mathcomp wiki.

So now, this issue can be closed.

Thank you all @proux01 @Zimmi48 @Alizter !