Skip to content

[ci] make the documentation build immune to the git-maintenance race - #1139

Merged
strub merged 1 commit into
mainfrom
ci-docs-git-maintenance
Sep 11, 2026
Merged

[ci] make the documentation build immune to the git-maintenance race#1139
strub merged 1 commit into
mainfrom
ci-docs-git-maintenance

Conversation

@strub

@strub strub commented Sep 11, 2026

Copy link
Copy Markdown
Member

opam init intermittently failed in the documentation workflow with

Could not update repository "default": lstat failed on
.git/objects/maintenance.lock: No such file or directory

Since git 2.46, fetch and clone spawn a detached

git maintenance run --auto

job that races with opam scanning the repository it has just
cloned (ocaml/opam#7031). The opam-side fix (ocaml/opam#7073) only ships
in 2.6.0, still a release candidate, and does not cover the path pin on
the checkout.

Disable git background maintenance on the runner, and fetch the opam
repository over HTTP instead of git, which removes the clone the
maintenance job operates on. Also drop the deprecated dune-cache
input, superseded by cache.

`opam init` intermittently failed in the documentation workflow with

    Could not update repository "default": lstat failed on
    .git/objects/maintenance.lock: No such file or directory

Since git 2.46, fetch and clone spawn a detached `git maintenance run
--auto` job that races with opam scanning the repository it has just
cloned (ocaml/opam#7031). The opam-side fix (ocaml/opam#7073) only ships
in 2.6.0, still a release candidate, and does not cover the path pin on
the checkout.

Disable git background maintenance on the runner, and fetch the opam
repository over HTTP instead of git, which removes the clone the
maintenance job operates on. Also drop the deprecated `dune-cache`
input, superseded by `cache`.
@strub
strub force-pushed the ci-docs-git-maintenance branch from a677451 to bad6502 Compare September 11, 2026 15:29
@strub strub self-assigned this Sep 11, 2026
@strub strub added chore Ungrateful tasks that need done but that nobody wants to do yolo-pr Don't bother reviewing, I will merge labels Sep 11, 2026
@strub
strub merged commit 63999f5 into main Sep 11, 2026
5 checks passed
@strub
strub deleted the ci-docs-git-maintenance branch September 11, 2026 15:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

chore Ungrateful tasks that need done but that nobody wants to do yolo-pr Don't bother reviewing, I will merge

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant