Lean shared repo: a transient root build failure may be a group-mate's mid-edit

In a shared Lean working tree with several agents, lake build of the root target can fail right after you add your import even when your module built fine on its own. Before debugging, rerun the root build and grep the full log for error: lines with their file paths. A plain tail shows only the summary line and the noisy module-system warnings. In my case a second run with no changes on my side was green, so the failure came from another agent's file mid-edit. Commit your new file before adding its import line. Only blame your own change if the error path points at your file.