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.

[proux01]

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.

Could we rename the repo back to opam-coq-archive like it used to be?

[MSoegtropIMC]

@proux01 : since users have to explicitly give the repo name when creating a dev switch - also Coq Platform scripts do this - this will lead to questions and some trickery in the Coq Platform scripts.

Again my question: can't we just rename it in CI on checkout? As far as I can see we are discussing a top level repo name which can have any folder name on checkout.

[gares]

Apparently the github action to do the git checkout supports this already:
https://github.com/actions/checkout?tab=readme-ov-file#checkout-multiple-repos-side-by-side

[MSoegtropIMC]

Apparently the github action to do the git checkout supports this already:

So we just have to give a path option and fix a few places in the scripts?

[MSoegtropIMC]

I can add these to changes to this PR, but I wonder how I would test it. The CI for this PR did pass as it. What would I have to do to experience the CI failure?

[gares]

ah no, we are using gitlab, so no, we don't use the github checkout action. I'll check if there is something equivalent.

I think a way to test it is to edit a package that calls dune subst

[gares]

Here: https://docs.gitlab.com/ee/ci/runners/configure_runners.html#custom-build-directories

So I suggest you add a line here

opam/.gitlab-ci.yml

Line 8 in c5f59b9

OPAMJOBS: "2"

and make a whitespace change to https://github.com/coq/opam/blob/master/extra-dev/packages/coq-elpi/coq-elpi.dev/opam

[MSoegtropIMC]

Thanks, I will try it later today or tomorrow.

What I find mildly confusing in the docs you linked is the line:

By default, GitLab Runner clones the repository in a unique subpath of the $CI_BUILDS_DIR directory

I would read that such that the default path is mktmp like random generated.

[silene]

Actually, the documentation almost shows what the default is, that is, $CI_BUILD_DIR/group/project (with CI_BUILD_DIR being just /builds). So, setting GIT_CLONE_PATH to $CI_BUILDS_DIR/foobar should indeed prevent opam from appearing in the parent of the working directory.

[MSoegtropIMC]

I just saw that @SkySkimmer removed the dune upper bound in coq-core.dev via e7ea74c already.

I guess the fix to the CI system + adjustments in branch dev packages is still required, so I will proceed with improving this PR. In case this is considered obsolete, please let me know.

[SkySkimmer]

I just saw that @SkySkimmer removed the dune upper bound in coq-core.dev via e7ea74c already.

That's just because it's on rocq-runtime

[MSoegtropIMC]

The fine print of the docs say:

This can only be used when custom_build_dir is enabled in the runner’s configuration.

and indeed I get the error:

ERROR: Job failed: setting GIT_CLONE_PATH is not allowed, enable `custom_build_dir` feature

I don't know much about our runner setup on gitlab. Can we change the runner setup? Is there a security risk associated with enabling this?

[silene]

With the "docker" executor and its siblings, I don't think there is any security issue, since the build directory is still supposed to be a child of CI_BUILDS_DIR, so the runner will not overwrite anything critical. (With the other executors, however, I can imagine how it would be a security breach to allow the runner to dump user-controlled files anywhere under CI_BUILDS_DIR.)

Anyway, your original proposal of doing some kind of mv as the first step of the before_script script should still work.