Skip to content

fix: use commondir to resolve git directory in worktrees#13045

Open
kim-em wants to merge 1 commit intomasterfrom
fix-worktree-git-revision
Open

fix: use commondir to resolve git directory in worktrees#13045
kim-em wants to merge 1 commit intomasterfrom
fix-worktree-git-revision

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Mar 22, 2026

This PR fixes git revision detection in worktrees where the worktree's gitdir path passes through another git repository.

The vendored GetGitRevisionDescription.cmake module detects worktrees and then calls _git_find_closest_git_dir to find the shared git directory by walking up the filesystem looking for a .git entry. This fails when the worktree's gitdir is stored inside another git repository (e.g. when the project is a git submodule whose objects live at ~/.git/modules/... and ~ is itself a git repo) — the walk finds the wrong .git.

The fix reads the commondir file that git places in every worktree's gitdir, which directly points to the shared git object directory. Falls back to the old filesystem walk if commondir doesn't exist (shouldn't happen with any modern git, but safe to keep).

🤖 Prepared with Claude Code

This PR fixes git revision detection in worktrees where the worktree's
gitdir path passes through another git repository. The previous code
used `_git_find_closest_git_dir` which walks up the filesystem looking
for a `.git` entry, but this finds the wrong repository when the
worktree gitdir is stored inside another git repo (e.g. when the
project is a git submodule of a parent repo that also uses git).

Instead, read the `commondir` file that git places in every worktree's
gitdir, which directly points to the shared git object directory. Fall
back to the old filesystem walk if `commondir` doesn't exist.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@kim-em kim-em added the changelog-no Do not include this PR in the release changelog label Mar 22, 2026
@kim-em kim-em changed the title fix(build): use commondir to resolve git directory in worktrees fix: use commondir to resolve git directory in worktrees Mar 22, 2026
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 23, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ae39633d171bbb1b4df79e27c8cabe3f17b8ee1 --onto 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-23 00:14:05)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8ae39633d171bbb1b4df79e27c8cabe3f17b8ee1 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-23 00:14:07)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants