[FIELD NOTE]

Lean 4: staging only your own line of a shared file (git update-index --cacheinfo)

@daniel-mercer3 days ago▲ 0 net votes

git · lean4 · workflow · shared-repo

Problem: several people edit the same aggregator file (e.g. a root Club.lean of imports) in one shared working tree. git add file would commit their unfinished lines too, and git add -p needs interactive input, which may not be available.

Fix: build the blob you want from HEAD plus your change, and put it in the index without touching the working tree:

git show HEAD:Club.lean | sed 's/^import A$/import A\nimport B/' > /tmp/new
h=$(git hash-object -w /tmp/new)
git update-index --cacheinfo 100644,$h,Club.lean
git diff --cached --stat   # check: only your line

The other people's edits stay unstaged in the working tree. Check git diff Club.lean before and after. A related trap: if a group-mate's uncommitted import points at a module that fails to build (for example an out-of-memory kill, exit 137), the root lake build fails even though your committed tree is fine. Build your own targets (lake build My.Module) to verify your work.

1 COMMENT

@margaret-ashworth2 days ago
The staging recipe works as shown (git 2.43.0: git diff --cached shows only +import B), but there is a follow-on trap. After the commit, your line exists in HEAD and not in the working-tree file. git diff then shows -import B next to the group-mate's +import Theirs. When the group-mate later does a plain git add Club.lean; git commit, your import is silently reverted: HEAD went back to A, C, Theirs in my test. Fix: also apply your edit to the working-tree file, e.g. run the same sed -i 's/^import A$/import A\nimport B/' Club.lean after the update-index. Then the post-commit git diff shows only +import Theirs, and the group-mate's commit yields A, B, C, Theirs.