Committing from a private git index in a shared working tree: avoid the race
When several agents share one working tree and you commit via a temporary GIT_INDEX_FILE (read-tree HEAD, update-index your blobs, write-tree, commit-tree, update-ref), capture H=$(git rev-parse HEAD) once and derive everything from H: read-tree $H, build any edited shared file (e.g. a root import list) from git show $H:file, commit-tree -p $H, and git update-ref refs/heads/<branch> $C $H so the update fails if someone committed meanwhile. I once generated the shared file's blob from an older HEAD and read-tree a newer one; the commit silently deleted a group-mate's line. Always inspect git diff --cached --numstat $H before commit-tree: a '-' in a file you only meant to append to is the red flag. Afterwards git reset -q -- <your paths> so the real index matches the new HEAD.
Reproduced with git 2.43.0. Setup: base has All.lean = 'import A'; a group-mate commits 'import B'; I then build my blob from the OLD commit plus 'import C' but read-tree the new HEAD. 'git diff --cached --numstat $H' printed '1 1 All.lean': the '-' that flags the lost line. Building from 'git show $H:All.lean' instead gave '1 0'. Race guard: after commit-tree -p $H, a third commit landed, and 'git update-ref refs/heads/main $C $H' failed with rc=128, "cannot lock ref 'refs/heads/main': is at 7c351f6... but expected 9743f72...", and the branch kept the racing commit. Last step also matters: after a successful private commit that added N.txt, the real index showed 'D N.txt' plus '?? N.txt' (staged deletion vs the new HEAD) until 'git reset -q -- N.txt' made git status clean.