doc: expand the lake test and lint driver section#855
Merged
Conversation
This PR expands the "Test and Lint Drivers" chapter in the Lake reference to cover what a test or lint driver actually is (a target — executable, script, or library — not a test framework), with verified `lakefile.toml` examples and prose instructions for `lakefile.lean`. New material: * exit-code semantics for executable/script drivers and the elaboration-error contract for library drivers, * configuring with `testDriver`/`lintDriver` versus `@[test_driver]`/ `@[lint_driver]` attributes, including the single-driver constraint, * the `<pkg>/<name>` syntax for drivers in dependency packages, * `lake test` and `lake lint` argument handling, including how `testDriverArgs`/`lintDriverArgs` compose with arguments after `--`, * the library-driver argument restriction, * notes on `lake check-test` and `lake check-lint`. 🤖 Prepared with Claude Code
Vale flagged em dashes with surrounding spaces and the bare word 'lakefile'. Rewrite the prose without em dashes and replace 'in the same lakefile'/'in the lakefile' with 'in the same configuration'/ elided forms that Vale accepts. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Address review feedback on the previous draft: * Add a paragraph explaining that `lake lint` also runs Lake's builtin linter when enabled, and that positional `MODULE` arguments go to the builtin linter, not to the configured driver. `lake lint Mathlib` and `lake lint -- Mathlib` are different things. * Note that `check-lint` exits 0 also when `builtinLint := true` is set. * Fix the opening sentence of "Test and Lint Drivers" to acknowledge that library test drivers are exercised by elaboration, not run. * Reword "drivers in dependencies aren't run" as "Lake doesn't automatically run each dependency package's driver" so that the `<pkg>/<name>` form, covered later, doesn't read as a contradiction. * Soften "the attribute form is the more common style" to "often convenient". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-bors Bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 1, 2026
This PR configures the `mathlib` package so that the standard `lake lint` command is equivalent to `lake exe runLinter Mathlib`, by setting ``` lintDriver := "batteries/runLinter" lintDriverArgs := #["Mathlib"] ``` on the `package mathlib` declaration. `runLinter` is already a `lean_exe` in batteries, so the `<pkg>/<name>` syntax lets mathlib reuse it directly. The CI workflows in `build_template.yml` and `nolints.yml` are also switched from invoking `lake exe runLinter [args] Mathlib` to `lake lint -- [args]` so there's a single source of truth for "lint mathlib", and so that local users get the same behaviour as CI. ### Behavior change for local users Before this PR, `lake lint` in a Mathlib checkout errored out with "no lint driver configured" and was essentially unused. After this PR, `lake lint` runs the full Batteries linter over all of Mathlib, which is a substantial multi-minute job. Anyone who has scripts or muscle memory expecting `lake lint` to be a no-op should be aware. The previous direct invocation, `lake exe runLinter Mathlib`, continues to work for anyone who prefers it. The `scripts/bench/lint/` benchmark intentionally keeps the direct `lake exe runLinter Mathlib` invocation so its measurements are not affected by anything `lake lint` may do above the linter. Motivated by a recent Zulip discussion in which it became clear that very few people know `lake lint` exists, partly because few packages bother to configure a lint driver: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively Companion to leanprover/reference-manual#855 (which documents the mechanism in the Lean reference manual). 🤖 Prepared with Claude Code
b-mehta
pushed a commit
to b-mehta/mathlib4
that referenced
this pull request
Jun 2, 2026
This PR configures the `mathlib` package so that the standard `lake lint` command is equivalent to `lake exe runLinter Mathlib`, by setting ``` lintDriver := "batteries/runLinter" lintDriverArgs := #["Mathlib"] ``` on the `package mathlib` declaration. `runLinter` is already a `lean_exe` in batteries, so the `<pkg>/<name>` syntax lets mathlib reuse it directly. The CI workflows in `build_template.yml` and `nolints.yml` are also switched from invoking `lake exe runLinter [args] Mathlib` to `lake lint -- [args]` so there's a single source of truth for "lint mathlib", and so that local users get the same behaviour as CI. ### Behavior change for local users Before this PR, `lake lint` in a Mathlib checkout errored out with "no lint driver configured" and was essentially unused. After this PR, `lake lint` runs the full Batteries linter over all of Mathlib, which is a substantial multi-minute job. Anyone who has scripts or muscle memory expecting `lake lint` to be a no-op should be aware. The previous direct invocation, `lake exe runLinter Mathlib`, continues to work for anyone who prefers it. The `scripts/bench/lint/` benchmark intentionally keeps the direct `lake exe runLinter Mathlib` invocation so its measurements are not affected by anything `lake lint` may do above the linter. Motivated by a recent Zulip discussion in which it became clear that very few people know `lake lint` exists, partly because few packages bother to configure a lint driver: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively Companion to leanprover/reference-manual#855 (which documents the mechanism in the Lean reference manual). 🤖 Prepared with Claude Code
david-christiansen
force-pushed
the
test-driver-doc
branch
from
c125f71 to
f605c85
Compare
Collaborator
|
Sorry for the slow turnaround here! I went through and added some more tests/examples and did some light prose editing. I'd like to look at it once more with fresh eyes before a merge. |
Bergschaf
pushed a commit
to Bergschaf/mathlib4
that referenced
this pull request
Jun 3, 2026
This PR configures the `mathlib` package so that the standard `lake lint` command is equivalent to `lake exe runLinter Mathlib`, by setting ``` lintDriver := "batteries/runLinter" lintDriverArgs := #["Mathlib"] ``` on the `package mathlib` declaration. `runLinter` is already a `lean_exe` in batteries, so the `<pkg>/<name>` syntax lets mathlib reuse it directly. The CI workflows in `build_template.yml` and `nolints.yml` are also switched from invoking `lake exe runLinter [args] Mathlib` to `lake lint -- [args]` so there's a single source of truth for "lint mathlib", and so that local users get the same behaviour as CI. ### Behavior change for local users Before this PR, `lake lint` in a Mathlib checkout errored out with "no lint driver configured" and was essentially unused. After this PR, `lake lint` runs the full Batteries linter over all of Mathlib, which is a substantial multi-minute job. Anyone who has scripts or muscle memory expecting `lake lint` to be a no-op should be aware. The previous direct invocation, `lake exe runLinter Mathlib`, continues to work for anyone who prefers it. The `scripts/bench/lint/` benchmark intentionally keeps the direct `lake exe runLinter Mathlib` invocation so its measurements are not affected by anything `lake lint` may do above the linter. Motivated by a recent Zulip discussion in which it became clear that very few people know `lake lint` exists, partly because few packages bother to configure a lint driver: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively Companion to leanprover/reference-manual#855 (which documents the mechanism in the Lean reference manual). 🤖 Prepared with Claude Code
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Contributor
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 00dfd62. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR expands the "Test and Lint Drivers" chapter in the Lake reference to make
lake testandlake lintsubstantially easier to follow on a first read. The previous text was a single short paragraph that mentioned@[test_driver]once without an example. The new section covers:lakefile.tomlexample for bothtestDriverandlintDriver,lakefile.leanconfiguration (without a code example, since the surrounding chapter is currently in a:::TODObecause importing Lake's attributes crashes the compiler),<pkg>/<name>syntax for drivers defined in dependency packages,testDriverArgsandlintDriverArgscompose with arguments passed after--on the command line,lake check-testandlake check-lint.Motivated by a recent Zulip thread asking for better documentation:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively/near/598083186
🤖 Prepared with Claude Code