chore(ci): split checkInitImports into its own test (#386)

Closes #380. This makes `CslibTests` the target for `lake test`,
ensuring that the `--iofail --wfail` flags are propagated. The previous
test runner is removed, with `lake exe checkInitImports` being moved
into a check in CI. This seems to be the standard solution at the
moment, but we should revisit in the future if multiple test targets are
supported (as drafted in
leanprover/lean4#10531).

Author: chenson2018

.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

CONTRIBUTING.md

@@ -103,14 +103,13 @@ 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
   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 +124,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 +330,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.
+Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable.

lakefile.toml

@@ -1,7 +1,7 @@
 name = "cslib"
 version = "0.1.0"
 defaultTargets = ["Cslib"]
-testDriver = "runTests"
+testDriver = "CslibTests"
 lintDriver = "batteries/runLinter"
 
 [leanOptions]
@@ -29,8 +29,3 @@ globs = ["CslibTests.+"]
 name = "checkInitImports"
 srcDir = "scripts"
 root = "CheckInitImports"
-
-[[lean_exe]]
-name = "runTests"
-srcDir = "scripts"
-root = "RunTests"

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`