feat: add lake check to check a project against external checkers - #14990
Open
Kha wants to merge 2 commits into
Open
feat: add lake check to check a project against external checkers#14990Kha wants to merge 2 commits into
lake check to check a project against external checkers#14990Kha wants to merge 2 commits into
Conversation
This PR adds a `modules` facet to packages, so `lake query :modules` reports the Lean modules of a package's default targets: the modules of each default library, and the root of each default executable together with its local transitive imports. A default target that builds no Lean modules, such as a custom target, contributes nothing. Libraries have had a `modules` facet for some time. This is its package-level counterpart, and like it the facet is not buildable, so it is reached through `lake query` rather than `lake build`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR adds `lake check`, which builds a project's default targets, exports them, replays the result through the kernel, and reports the axioms that code rests on, failing on any beyond `propext`, `Classical.choice` and `Quot.sound`. There is no challenge to compare against. Nothing about the project is evaluated outside the sandbox. `lake env` resolves its dependencies and `lake query :modules` names the modules to check, both inside it, so the project's configuration is never elaborated in Lake's own address space; the build and the export follow in the same sandbox. As for `lake challenge`, this requires the project to carry a `lake-manifest.json`, since the sandbox cannot write one into the project directory. The exporter is given no declaration list, so the export covers everything in scope rather than only what the project declares, and a check costs roughly the same whatever the project's size: about a minute for a project holding a single theorem. The axiom report copes with that without a list of roots: an axiom that is merely importable is referred to by nothing, so the axioms that some other constant refers to are exactly the ones the code rests on. Note that the kernel accepts `sorryAx`, so a `sorry` is caught by this report and by nothing else. All the default targets' modules go through the pipeline together, in one sandboxed `lake build`, one export and one kernel replay. Since each module's export already covers its whole import closure, a pass per module would re-check what they share: on a two-root project the roots' exports agree on 6,437,744 of 6,437,817 lines, so the second pass would double the run for two extra constants. The sandbox invocations in `Lake.Check` get one definition each. `landrunSpawnArgs` builds the `IO.Process.SpawnArgs` that both `runSandBoxedWithStdout` and `runSandBoxedExitCode` use, and `runSandBoxed` is the latter plus the exit-code check. `runExternalKernel` goes through `runSandBoxedExitCode` rather than spawning `landrun` itself, keeping its own messages. `runExporter` holds the exporter's grants, which `safeExport` and `exportModules` had spelled out identically. The two commands share the tool resolution and the sandbox context through `mkContext`; the vendored comparison path is untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Kha
commented
Sep 1, 2026
| builtin_facet transDeps : Package => Array Package | ||
|
|
||
| /-- The Lean modules of the package's default targets. -/ | ||
| builtin_facet modules : Package => Array Module |
Member
Author
There was a problem hiding this comment.
@tydeu FYI, this is for retrieving the modules for lean4export under the sandbox
Kha
commented
Sep 1, 2026
| def exportModules (modules : Array Lean.Name) : M String := do | ||
| let moduleArgs := modules.map (·.toString) | ||
| IO.println s!"Exporting the declarations of {" ".intercalate moduleArgs.toList}" | ||
| runExporter moduleArgs |
Member
Author
There was a problem hiding this comment.
@hargoniX We might need a leanexport --stdin if we want this to not crash for Mathlib on Windows
leanprover-bot
added
the
breaks-manual
Collaborator
|
Reference manual CI status:
|
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 adds
lake check, a challenge-less variant oflake challenge, which builds the current project's default targets, exports them, replays the result through the kernel, and fails on any use of non-standard axioms.Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com