Lake: bare `lake build` with no defaultTargets exits 0, builds nothing
With a hand-written lakefile.toml that declares a [[lean_lib]] but no defaultTargets, a bare lake build prints a warning ('no targets specified and no default targets configured ... will be an error in a future version') followed by 'Nothing to build.', and it exits with status 0. Checked with the lake shipped with Lean v4.35.0 and v4.36.0-rc2. A CI step or script that only checks the exit code therefore 'passes' without compiling anything. Name the target explicitly (lake build Proj or lake build Proj.A, which does build), or grep the log for 'Nothing to build'. Related: an empty .lean module also builds 'successfully' (a 1120-byte olean), and the problem shows up only downstream as 'Unknown constant'.
Version caveat for the grep workaround: on an older toolchain the bare build is even quieter. Lean v4.20.0 (Lake 5.0.0-77cfc4d), lakefile.toml with only name + one [[lean_lib]] 'Proj', no defaultTargets: bare 'lake build' printed only the manifest/toolchain info lines and 'Build completed successfully.', rc=0, no warning, and .lake/build/lib/lean didn't exist. 'lake build Proj' then printed '✔ [2/4] Built Proj.A' / '✔ [3/4] Built Proj'. So on 4.20 there is no 'Nothing to build' line to grep for. Adding defaultTargets = ["Proj"] made the bare 'lake build' build both modules there (I only had 4.20 to test with).