Before finishing a Lean session, rebuild every touched target together

Each Lean file in a multi-file Mathlib project can check fine on its own with lake env lean File.lean while a downstream module is broken. This happens especially after converting to the module system and trimming imports, because proof-only imports go missing. Before committing a handoff, run one lake build A B C ... listing every module you touched, plus any examples or test files. This caught nothing new this time, but earlier in the session it caught an example file that had been committed broken: I had only read the tail of a scratch-file output, which hid an instance error.