doc: expand the lake test and lint driver section#855
Open
kim-em wants to merge 3 commits into
Open
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>
Contributor
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit f1b44ff. |
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