Coq dev/rc packages: remove outdated restriction to dune < 3.14

[MSoegtropIMC]

This PR removes outdated restrictions to dune - none of the release Coq packages still has these so there is no good reason for keeping them in the dev packages.

There are known versions of dune to not work - one could exclude these, but this is not done in the Coq release packages either.

[palmskog]

As has been discussed elsewhere, not having these restrictions breaks our CI here for core-dev and extra-dev repos. This means I can't effectively review packages proposed for inclusion to these repos.

[MSoegtropIMC]

I assumed this issue is gone since all packages removed restrictions which would lead to a pick of dune 3.14 or a broken dune.dev.

[palmskog]

The CI issue is not gone and there is no indication it will be fixed upstream (in Dune).

[silene]

We can merge such a pull request, but it needs to come with a mechanism to make sure that Dune stays stuck at 3.14 in our CI (e.g., a virtual Opam package that would conflict with Dune >= 3.14 and that would be somehow marked as unremovable).

[MSoegtropIMC]

I reviewed the discussion, but I can't say I understand it. In this comment it is stated that dune 3.14 breaks Coq-CI, but Coq CI does work with dune 3.16 (but not with 3.17 on Windows). See the recent discussion in Zulip. Can you add a few more pointers and what exactly doesn't work?

Anyway, I don't think it is an option to stay with dune < 3.14 forever.

[MSoegtropIMC]

E.g. cause of this I could not test a fix I suggested to @SkySkimmer for fixing Coq CI locally (which involves pinning dune to 3.15.3.

[silene]

Can you add a few more pointers and what exactly doesn't work?

As you know, Dune 3.14 came with a new feature, which is the ability to update all the files stored inside an opam subdirectory (which makes sense because Opam also looks there for its package files). Unfortunately, the Opam repository for Coq is a project named coq/opam, which means that the Gitlab runner stores all the important files inside a directory named opam. For some reason, Dune thinks that that opam directory comes under its purview and starts to modify all its files, which causes a very confused Git to crash.

The issue does not occur with Coq's main CI because the project is named coq/coq, so there is no opam directory to mess with. Also, the issue does not occur with Coq's releases either, because they do not invoke dune subst. You need the conjunction of both these things: a parent directory named opam and a call to dune subst.

Anyway, that is my own interpretation of the issue, but it has yet to be disproved.

[MSoegtropIMC]

I see - thanks for the explanation!

One thought: since opam is the root name of the git repo and not of a sub folder, can't one just give it a different name on clone in CI or rename it after clone in CI? Git doesn't mind the name of the root folder of a a repo - only what is in it.