From 30a3fde8aa2968acce441fa37436e51acf55f376 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 22 Apr 2026 23:27:29 -0400 Subject: [PATCH] feat: lake: empty build detection & `--allow-empty` (#13500) This PR adds a check for empty `lake build` invocations (as an empty build usually indicates a misconfiguration). Builds with no jobs will now print "Nothing to build." and invocations of `lake build` with no default targets configured will produce a warning. This will be promoted to an error in the future. The warning (and future error) can be suppressed with the new `--allow-empty` CLI option. --------- Co-authored-by: Claude Opus 4.7 (1M context) --- src/lake/Lake/Build/Run.lean | 11 ++++-- src/lake/Lake/CLI/Help.lean | 1 + src/lake/Lake/CLI/Main.lean | 8 ++++ tests/lake/tests/emptyBuild/clean.sh | 1 + tests/lake/tests/emptyBuild/lakefile.lean | 7 ++++ tests/lake/tests/emptyBuild/lakefile.toml | 5 +++ tests/lake/tests/emptyBuild/test.sh | 47 +++++++++++++++++++++++ 7 files changed, 76 insertions(+), 4 deletions(-) create mode 100755 tests/lake/tests/emptyBuild/clean.sh create mode 100644 tests/lake/tests/emptyBuild/lakefile.lean create mode 100644 tests/lake/tests/emptyBuild/lakefile.toml create mode 100755 tests/lake/tests/emptyBuild/test.sh diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 6ce42eb4c4..a7cc97ab78 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -284,11 +284,14 @@ def reportResult (cfg : BuildConfig) (out : IO.FS.Stream) (result : MonitorResul if result.failures.isEmpty then if cfg.showProgress && cfg.showSuccess then let numJobs := result.numJobs - let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs" - if cfg.noBuild then - print! out s!"All targets up-to-date ({jobs}).\n" + if numJobs == 0 then + print! out "Nothing to build.\n" else - print! out s!"Build completed successfully ({jobs}).\n" + let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs" + if cfg.noBuild then + print! out s!"All targets up-to-date ({jobs}).\n" + else + print! out s!"Build completed successfully ({jobs}).\n" else print! out "Some required targets logged failures:\n" result.failures.forM (print! out s!"- {·}\n") diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index bfacf95ce0..6ea8f0ff97 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -55,6 +55,7 @@ BASIC OPTIONS: --packages=file JSON file of package entries that override the manifest --reconfigure, -R elaborate configuration files instead of using OLeans --keep-toolchain do not update toolchain on workspace update + --allow-empty accept bare builds with no default targets configured --no-build exit immediately if a build target is not up-to-date --no-cache build packages locally; do not download build caches --try-cache attempt to download build caches for supported packages diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 5a126d15a5..a9e59aaf93 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -56,6 +56,7 @@ public structure LakeOptions where reconfigure : Bool := false oldMode : Bool := false trustHash : Bool := true + allowEmpty : Bool := false noBuild : Bool := false noCache : Option Bool := none failLv : LogLevel := .error @@ -247,6 +248,7 @@ def lakeLongOption : (opt : String) → CliM PUnit | "--old" => modifyThe LakeOptions ({· with oldMode := true}) | "--text" => modifyThe LakeOptions ({· with outFormat := .text}) | "--json" => modifyThe LakeOptions ({· with outFormat := .json}) +| "--allow-empty" => modifyThe LakeOptions ({· with allowEmpty := true}) | "--no-build" => modifyThe LakeOptions ({· with noBuild := true}) | "--no-cache" => modifyThe LakeOptions ({· with noCache := true}) | "--try-cache" => modifyThe LakeOptions ({· with noCache := false}) @@ -845,6 +847,12 @@ protected def build : CliM PUnit := do let ws ← loadWorkspace config let targetSpecs ← takeArgs let specs ← parseTargetSpecs ws targetSpecs + if specs.isEmpty && !opts.allowEmpty then + logWarning "no targets specified and no default targets configured\ + \n Note: This will be an error in a future version of Lake.\ + \n Hint: This warning (or error) can be suppressed with '--allow-empty'." + if opts.failLv ≤ .warning then + exit 1 specs.forM fun spec => unless spec.buildable do throw <| .invalidBuildTarget spec.info.key.toSimpleString diff --git a/tests/lake/tests/emptyBuild/clean.sh b/tests/lake/tests/emptyBuild/clean.sh new file mode 100755 index 0000000000..333b50aba2 --- /dev/null +++ b/tests/lake/tests/emptyBuild/clean.sh @@ -0,0 +1 @@ +rm -rf .lake lake-manifest.json produced.out diff --git a/tests/lake/tests/emptyBuild/lakefile.lean b/tests/lake/tests/emptyBuild/lakefile.lean new file mode 100644 index 0000000000..88383551af --- /dev/null +++ b/tests/lake/tests/emptyBuild/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package test + +lean_lib Lib where + globs := #[] diff --git a/tests/lake/tests/emptyBuild/lakefile.toml b/tests/lake/tests/emptyBuild/lakefile.toml new file mode 100644 index 0000000000..798a3e1405 --- /dev/null +++ b/tests/lake/tests/emptyBuild/lakefile.toml @@ -0,0 +1,5 @@ +name = "test" + +[[lean_lib]] +name = "Lib" +globs = [] diff --git a/tests/lake/tests/emptyBuild/test.sh b/tests/lake/tests/emptyBuild/test.sh new file mode 100755 index 0000000000..ee29f3038c --- /dev/null +++ b/tests/lake/tests/emptyBuild/test.sh @@ -0,0 +1,47 @@ +#!/usr/bin/env bash +source ../common.sh + +# This test covers the behavior of `lake build` +# with no default targets configured. + +test_empty_build() { +cfg_file=$1 +test_run -f $cfg_file update +test_out_diff <(cat << 'EOF' +warning: no targets specified and no default targets configured + Note: This will be an error in a future version of Lake. + Hint: This warning (or error) can be suppressed with '--allow-empty'. +Nothing to build. +EOF +) -f $cfg_file build +test_err_diff <(cat << 'EOF' +warning: no targets specified and no default targets configured + Note: This will be an error in a future version of Lake. + Hint: This warning (or error) can be suppressed with '--allow-empty'. +EOF +) -f $cfg_file build --wfail +test_out_diff <(cat << 'EOF' +Nothing to build. +EOF +) -f $cfg_file build --allow-empty --wfail +# Test the warning is not printed on a regular build. +# The configurations use `globs = []` to minimize build variance, +# and to verify that empty globs do not count as no jobs. +test_out_diff <(cat << 'EOF' +Build completed successfully (1 job). +EOF +) -f $cfg_file build Lib +} + +# Test Lean configuration with no default targets +./clean.sh +echo "# TEST: lakefile.lean" +test_empty_build lakefile.lean + +# Test TOML configuration with no default targets +./clean.sh +echo "# TEST: lakefile.toml" +test_empty_build lakefile.toml + +# Cleanup +rm -f produced.*