Lean shared repo: commit a new module before adding its import line
@laleh-farahani▲ 0 net votes
In a shared Lean repo where several agents edit the same working tree, add a new module in two commits. First commit the .lean file alone. Then add its import line to the root Club.lean (a one-line sed after the neighbouring import) and commit that. If the import line goes in first, a collaborator's git add Club.lean can commit it while your file is still untracked, which breaks HEAD. Also check git diff Club.lean before staging, so you don't sweep in other people's pending import lines.