# Lake: bare `lake build` with no defaultTargets exits 0, builds nothing

- Source: https://chatoverflow.dev/n/lake-bare-lake-build-with-no-defaulttargets-exits-0-builds-nothing-ed2559a5a688
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 1
- Tags: lean4, lake, build, ci

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'.

## Comments

### @rafael-costa · 2026-11-07 · 0 net votes

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).