From 80ec4f7506fce64630c7e8551d73dbe42930d236 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 2 Mar 2026 12:10:39 -0500 Subject: [PATCH 1/3] chore(ci): split checkInitImports into its own test --- .github/workflows/lean_action_ci.yml | 4 +++ CONTRIBUTING.md | 7 +++-- lakefile.toml | 2 +- scripts/README.md | 2 +- scripts/RunTests.lean | 41 ---------------------------- 5 files changed, 11 insertions(+), 45 deletions(-) delete mode 100644 scripts/RunTests.lean diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index ac39c0abf..5ce93d04e 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -26,6 +26,10 @@ jobs: run: | set -e lake shake --add-public --keep-implied --keep-prefix Cslib + - name: "checkInitImports" + run: | + set -e + lake exe checkInitImports - uses: leanprover-community/lint-style-action@main with: mode: check diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e2591bcb7..114e08710 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -110,7 +110,7 @@ are - checking that all files import [Cslib.Init](/Cslib/Init.lean), which sets up some default linting and tactics -You can run these locally with `lake test`. +You can run these locally with `lake test` and `lake exe checkInitImports` respectively. ## Linting @@ -125,6 +125,9 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The There is a also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by running `lake exe mk_all --module` locally, which will make the required changes. +CSLib tests for minimized imports using `lake shake --add-public --keep-implied --keep-prefix`, which also comes with a `--fix` option. +See `lake shake --help` for the special comment syntax used to preserve imports required for tactics or typeclasses. + # Getting started CSLib is a community effort. To understand its scope and vision, please read the [CSLib whitepaper](https://arxiv.org/abs/2602.04846). @@ -328,4 +331,4 @@ There are two primary areas where generative AI can help: - generating/refining specifications (at the front-end or Boole level) - helping to prove Lean conjectures -Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable. \ No newline at end of file +Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable. diff --git a/lakefile.toml b/lakefile.toml index 81ea3e7d8..c5d060921 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,7 +1,7 @@ name = "cslib" version = "0.1.0" defaultTargets = ["Cslib"] -testDriver = "runTests" +testDriver = "CslibTests" lintDriver = "batteries/runLinter" [leanOptions] diff --git a/scripts/README.md b/scripts/README.md index 1921d5fe7..df8e55c30 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -44,7 +44,7 @@ to learn about it as well! - Optional: `zulip-send` CLI for automatic Zulip notifications **Init Imports** -- `CheckInitImports.lean` (usually run from `lake test`) checks that all files transitively import `Cslib.Init`. +- `CheckInitImports.lean` (run by `lake exe checkInitImports`) checks that all files transitively import `Cslib.Init`. **Linting** - `weekly_lint_report.sh` diff --git a/scripts/RunTests.lean b/scripts/RunTests.lean deleted file mode 100644 index 1cd4de5aa..000000000 --- a/scripts/RunTests.lean +++ /dev/null @@ -1,41 +0,0 @@ -/- -Copyright (c) 2025 Jesse Alama. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jesse Alama --/ - -/-! -# Test Runner - -This script runs all CSLib tests including: -- Building the CslibTests library -- Running init imports validation --/ - -def main (_ : List String) : IO UInt32 := do - -- build CslibTests - IO.println "building CslibTests..." - let CslibTestsResult ← IO.Process.spawn { - cmd := "lake" - args := #["build", "CslibTests"] - } >>= (·.wait) - - if CslibTestsResult != 0 then - IO.eprintln "\n✗ CslibTests build failed" - return CslibTestsResult - else - println! "" - - -- Run init imports check - IO.println "\nChecking init imports..." - let checkResult ← IO.Process.spawn { - cmd := "lake" - args := #["exe", "checkInitImports"] - } >>= (·.wait) - - if checkResult != 0 then - IO.eprintln "\n✗ Init imports check failed" - return checkResult - - IO.println "\n✓ All tests passed" - return 0 From f646b3af274797cdc73c00bde019b5c8713e1279 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 2 Mar 2026 12:11:59 -0500 Subject: [PATCH 2/3] old link --- CONTRIBUTING.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 114e08710..9425dac26 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -103,8 +103,7 @@ parenthetical containing what area of the library the PR is working on. ## Testing -There is a [series of tests](/scripts/RunTests.lean) that runs for each PR. The components of this -are +There is a series of tests that runs for each PR. The components of this are - running the tests found in [CslibTests](/CslibTests) - checking that all files import [Cslib.Init](/Cslib/Init.lean), which sets up some default linting From b694dd5bf2e7c2efa005dadddd844fcae13d10c6 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 2 Mar 2026 12:17:53 -0500 Subject: [PATCH 3/3] remove olf lakefile target --- lakefile.toml | 5 ----- 1 file changed, 5 deletions(-) diff --git a/lakefile.toml b/lakefile.toml index c5d060921..11a7b00d0 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -29,8 +29,3 @@ globs = ["CslibTests.+"] name = "checkInitImports" srcDir = "scripts" root = "CheckInitImports" - -[[lean_exe]] -name = "runTests" -srcDir = "scripts" -root = "RunTests"