From d33a771ea3baf776e69d2ba80d7690946396c3bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 12 May 2026 18:25:00 +0200 Subject: [PATCH] test: always clean full `.lake` (#13703) Ensures we don't reuse outdated config oleans --- tests/pkg/builtin_attr/run_test.sh | 2 +- tests/pkg/cbv_attr/run_test.sh | 2 +- tests/pkg/collectAxioms/run_test.sh | 2 +- tests/pkg/debug/run_test.sh | 2 +- tests/pkg/def_clash/clean.sh | 4 ++-- tests/pkg/deprecated_arg/run_test.sh | 2 +- tests/pkg/deprecated_module/run_test.sh | 2 +- tests/pkg/deprecated_option/run_test.sh | 2 +- tests/pkg/deriving/run_test.sh | 2 +- tests/pkg/frontend/run_test.sh | 2 +- tests/pkg/homo/run_test.sh | 2 +- tests/pkg/initialize/run_test.sh | 2 +- tests/pkg/issue12825/run_test.sh | 2 +- tests/pkg/leanchecker/run_test.sh | 2 +- tests/pkg/linter_set/run_test.sh | 2 +- tests/pkg/misc/run_test.sh | 2 +- tests/pkg/module/run_test.sh | 2 +- tests/pkg/path with spaces/run_test.sh | 2 +- tests/pkg/prv/run_test.sh | 2 +- tests/pkg/rebuild/run_test.sh | 2 +- tests/pkg/signal/run_test.sh | 2 +- tests/pkg/structure_docstrings/run_test.sh | 2 +- tests/pkg/sym_ext/run_test.sh | 2 +- tests/pkg/sym_simp_attr/run_test.sh | 2 +- tests/pkg/test_extern/run_test.sh | 2 +- tests/pkg/user_attr/run_test.sh | 2 +- tests/pkg/user_attr_app/run_test.sh | 2 +- tests/pkg/user_ext/run_test.sh | 2 +- tests/pkg/user_opt/run_test.sh | 2 +- tests/pkg/user_plugin/clean.sh | 2 +- 30 files changed, 31 insertions(+), 31 deletions(-) diff --git a/tests/pkg/builtin_attr/run_test.sh b/tests/pkg/builtin_attr/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/builtin_attr/run_test.sh +++ b/tests/pkg/builtin_attr/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/cbv_attr/run_test.sh b/tests/pkg/cbv_attr/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/cbv_attr/run_test.sh +++ b/tests/pkg/cbv_attr/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/collectAxioms/run_test.sh b/tests/pkg/collectAxioms/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/collectAxioms/run_test.sh +++ b/tests/pkg/collectAxioms/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/debug/run_test.sh b/tests/pkg/debug/run_test.sh index fd1762db3c..7b159a9ac9 100644 --- a/tests/pkg/debug/run_test.sh +++ b/tests/pkg/debug/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake run lake exe release run_fail lake exe debug diff --git a/tests/pkg/def_clash/clean.sh b/tests/pkg/def_clash/clean.sh index 7fba596497..009790de23 100755 --- a/tests/pkg/def_clash/clean.sh +++ b/tests/pkg/def_clash/clean.sh @@ -1,2 +1,2 @@ -rm -rf lake-manifest.json .lake/build -rm -rf deps/fooA/.lake/build deps/fooB/.lake/build deps/useA/.lake/build deps/useB/.lake/build +rm -rf lake-manifest.json .lake +rm -rf deps/fooA/.lake deps/fooB/.lake deps/useA/.lake deps/useB/.lake diff --git a/tests/pkg/deprecated_arg/run_test.sh b/tests/pkg/deprecated_arg/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/deprecated_arg/run_test.sh +++ b/tests/pkg/deprecated_arg/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/deprecated_module/run_test.sh b/tests/pkg/deprecated_module/run_test.sh index e4d4cf6b12..d1cecedd51 100644 --- a/tests/pkg/deprecated_module/run_test.sh +++ b/tests/pkg/deprecated_module/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake # Build Main library — includes all test modules capture lake build Main diff --git a/tests/pkg/deprecated_option/run_test.sh b/tests/pkg/deprecated_option/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/deprecated_option/run_test.sh +++ b/tests/pkg/deprecated_option/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/deriving/run_test.sh b/tests/pkg/deriving/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/deriving/run_test.sh +++ b/tests/pkg/deriving/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/frontend/run_test.sh b/tests/pkg/frontend/run_test.sh index a544fcdf3d..daf3bc8ec9 100644 --- a/tests/pkg/frontend/run_test.sh +++ b/tests/pkg/frontend/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake lake build # Check that we can compile a file which shares with the executable diff --git a/tests/pkg/homo/run_test.sh b/tests/pkg/homo/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/homo/run_test.sh +++ b/tests/pkg/homo/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/initialize/run_test.sh b/tests/pkg/initialize/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/initialize/run_test.sh +++ b/tests/pkg/initialize/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/issue12825/run_test.sh b/tests/pkg/issue12825/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/issue12825/run_test.sh +++ b/tests/pkg/issue12825/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/leanchecker/run_test.sh b/tests/pkg/leanchecker/run_test.sh index 6db99e08f3..4136ab37cf 100644 --- a/tests/pkg/leanchecker/run_test.sh +++ b/tests/pkg/leanchecker/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake lake build for f in LeanCheckerTests/*.lean; do diff --git a/tests/pkg/linter_set/run_test.sh b/tests/pkg/linter_set/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/linter_set/run_test.sh +++ b/tests/pkg/linter_set/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/misc/run_test.sh b/tests/pkg/misc/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/misc/run_test.sh +++ b/tests/pkg/misc/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/module/run_test.sh b/tests/pkg/module/run_test.sh index de377ac1ca..5a05982501 100644 --- a/tests/pkg/module/run_test.sh +++ b/tests/pkg/module/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake LEAN_ABORT_ON_PANIC=1 lake build capture_fail lake lean Module/ConflictingImported.lean diff --git a/tests/pkg/path with spaces/run_test.sh b/tests/pkg/path with spaces/run_test.sh index 7044f45e6f..a231ed627d 100644 --- a/tests/pkg/path with spaces/run_test.sh +++ b/tests/pkg/path with spaces/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake lake exe "path with spaces" # presence of this file should not break process spawn touch .lake/build/bin/path diff --git a/tests/pkg/prv/run_test.sh b/tests/pkg/prv/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/prv/run_test.sh +++ b/tests/pkg/prv/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/rebuild/run_test.sh b/tests/pkg/rebuild/run_test.sh index 048158d210..8a91aa15d0 100644 --- a/tests/pkg/rebuild/run_test.sh +++ b/tests/pkg/rebuild/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake mkdir -p Rebuild cat < Rebuild/Basic.lean diff --git a/tests/pkg/signal/run_test.sh b/tests/pkg/signal/run_test.sh index 4ae064d55f..0c97fcf235 100644 --- a/tests/pkg/signal/run_test.sh +++ b/tests/pkg/signal/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake lake build release # Create a named pipe for communication diff --git a/tests/pkg/structure_docstrings/run_test.sh b/tests/pkg/structure_docstrings/run_test.sh index 86adafe999..eb690dbb51 100644 --- a/tests/pkg/structure_docstrings/run_test.sh +++ b/tests/pkg/structure_docstrings/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake LEAN_ABORT_ON_PANIC=1 lake build diff --git a/tests/pkg/sym_ext/run_test.sh b/tests/pkg/sym_ext/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/sym_ext/run_test.sh +++ b/tests/pkg/sym_ext/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/sym_simp_attr/run_test.sh b/tests/pkg/sym_simp_attr/run_test.sh index b911bf4de8..c69eda4657 100755 --- a/tests/pkg/sym_simp_attr/run_test.sh +++ b/tests/pkg/sym_simp_attr/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/test_extern/run_test.sh b/tests/pkg/test_extern/run_test.sh index 178d67f395..8e2b4cd89f 100644 --- a/tests/pkg/test_extern/run_test.sh +++ b/tests/pkg/test_extern/run_test.sh @@ -6,7 +6,7 @@ # Ideally there would be a more principled testing framework # that took care of all this! -rm -rf .lake/build +rm -rf .lake # TODO Use and/or emulate the helper functions from util.sh? diff --git a/tests/pkg/user_attr/run_test.sh b/tests/pkg/user_attr/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/user_attr/run_test.sh +++ b/tests/pkg/user_attr/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/user_attr_app/run_test.sh b/tests/pkg/user_attr_app/run_test.sh index e119dfff42..e8c91e4b18 100644 --- a/tests/pkg/user_attr_app/run_test.sh +++ b/tests/pkg/user_attr_app/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake exe user_attr diff --git a/tests/pkg/user_ext/run_test.sh b/tests/pkg/user_ext/run_test.sh index 26263062c4..2e2d323e22 100644 --- a/tests/pkg/user_ext/run_test.sh +++ b/tests/pkg/user_ext/run_test.sh @@ -1,4 +1,4 @@ -rm -rf .lake/build +rm -rf .lake capture lake build -v check_out_contains 'hello, test, world' diff --git a/tests/pkg/user_opt/run_test.sh b/tests/pkg/user_opt/run_test.sh index b911bf4de8..c69eda4657 100644 --- a/tests/pkg/user_opt/run_test.sh +++ b/tests/pkg/user_opt/run_test.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake lake build diff --git a/tests/pkg/user_plugin/clean.sh b/tests/pkg/user_plugin/clean.sh index 69f5a551a5..2639d0cf53 100755 --- a/tests/pkg/user_plugin/clean.sh +++ b/tests/pkg/user_plugin/clean.sh @@ -1,2 +1,2 @@ -rm -rf .lake/build +rm -rf .lake rm -f lake-manifest.json