Question about `git gc` locking files

Recently, after upgrading to 2.47.0, we had internal reports of users erroring out with:

fatal: cannot lock ref 'HEAD': Unable to create '<filepath>/.git/HEAD.lock': File exists.

We believe this is due to "(98077d06) run-command: fix detaching when running auto maintenance", since we have neither `gc.autoDetach` nor `maintenance.autoDetach` set. When this bug was fixed, the maintenance runs that triggered during usage of the external tool, repo[1], would lock the HEAD file in the Android manifest repository thereby erroring out `repo`. Additionally, long running maintenance tasks would also cause users to frequently run into this issue when using git commands that are written to HEAD.

We can fix this easily temporarily by pushing out config changes to run in the foreground, however, I was under the impression that `git gc`, whether invoked normally or through `git maintenance`, would be able to run in parallel with other git commands and therefore not lock. There is no mention of this in the documentation for `git gc`, but I do see it in the `git maintenance` documentation. So should `git gc` be locking the HEAD file in the first place? And if so, is there a way for `git gc` to have less of a dependence on HEAD.lock?

Thanks, Calvin

[1] https://gerrit.googlesource.com/git-repo