chore: use git checkout --detach when checking out a commit hash

[Vierkantor]

The technical debt metrics seem to have broken recently, and in the CI log there is a fatal Git error about not detaching HEAD. The log does not show which command precisely failed. Looking at the set of error messages that Git produces, this can be traced to git checkout. So adding --detach to the checkout command should hopefully fix the issue.

Example of broken tech debt reports:

• https://github.com/leanprover-community/mathlib4/actions/runs/25331716666/job/74266774924#step:11:133

Interestingly git checkout in the transitive imports script does not seem to break anything. My suspicion is the git checkout -q switch turns the advice message into a fatal error? I'd have to look at the Git source code in more detail since the man page is not very clear. In any case, let's just add --detach there too to silence the advice.

[bryangingechen]

Did you mean to link to another run? The one you linked is one for the PR summary comment and I don't see an error in it.

[Vierkantor]

Oops, it lost the anchor to the right line. ("Post or update summary content", line 132.) There are fatal git errors but for some reason the script does not report an error. Even though set -euo is enabled on the top of the file...

[SnirBroshi]

Suggested change

	git checkout --detach "${commit1}"
	git switch --detach "${commit1}"

and everywhere else, checkout is pretty much deprecated.

switch required --detach for years, not sure why they "backported" it to checkout now, but using the recommended command would've saved this breakage.

[kim-em]

🤖 reviewed by Claude

I don't think this fix addresses the actual bug. The fatal error in the cited log —

fatal: a branch is expected, got commit 'b26e58057dc...'
hint: If you want to detach HEAD at the commit, try again with the --detach option.

— is git switch's error, not git checkout's. The four fatal lines correspond to the four git switch -q - calls in technical-debt-metrics.sh (the report function runs twice). By the time that script runs, the preceding pr_summary step has already left HEAD detached, so @{-1} is a commit and git switch - refuses.

git checkout <40-char-hash> already detaches HEAD; adding --detach only silences the advice. It doesn't change @{-1}, so git switch - still fails. Reproduced on git 2.53:

$ git checkout --detach <c2> && git checkout --detach <c1>
$ git switch -
fatal: a branch is expected, got commit '...'
$ git switch --detach -    # works

A real fix would be either git switch -q --detach -, or capturing origCommit="$(git rev-parse HEAD)" and restoring with git checkout -q --detach "${origCommit}" (matches what import_trans_difference.sh already does). The import_trans_difference.sh half here is harmless but isn't fixing a bug.