feat: add lake check to check a project against external checkers - #14990
Open
Kha wants to merge 3 commits into
Open
feat: add lake check to check a project against external checkers#14990Kha wants to merge 3 commits into
lake check to check a project against external checkers#14990Kha wants to merge 3 commits into
Conversation
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
leanprover-bot
added
the
breaks-manual
Collaborator
|
Reference manual CI status:
|
Member
Author
|
The adaptation PR for this PR is leanprover/downstream-lean4#33. |
github-actions
Bot
added
the
mathlib4-nightly-available
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Sep 2, 2026
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
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>
…ocess This PR collapses `lake check`'s four sandboxed invocations into two. `lake resolve-deps` materializes the project's dependencies, still the only step allowed to reach the network, and a second `lake` resolves the targets, builds them and dumps the export, all in one process. Only the export crosses back. The inner half is `lake check` itself, selected by the `LAKE_CHECK_EXPORT` environment variable that the outer half sets when it spawns, so no new command-line surface is added. It loads the workspace, fetches the root package's `modules` facet, builds the default targets and writes the export to standard out, leaving standard error for progress. It is also the half that a platform without a sandbox would run directly, since it is exactly the work that has to happen next to the project. What this removes: `safeQueryModules` and the parsing of module names out of its output, `exportModules` and the separate `leanexport` spawn, and, because the exporting process now loads the workspace itself, the `(LEAN_PATH, PATH)` round trip. Resolution keeps its own process precisely so the network stays confined to it, but it no longer has to report anything back, so it is `lake resolve-deps` rather than `lake env` parsed for its output. The module list never crosses a process boundary, which matters beyond tidiness: passing it as arguments would not survive a platform whose command line is capped in the tens of kilobytes. `LeanExport.dumpEnv` is the export loop that the `leanexport` binary's `main` already had, lifted so that both callers share it rather than keeping two copies that can drift. The binary's output is byte-identical. `lake challenge` is untouched and keeps `safeResolveWorkspace`, `safeLakeBuild` and `safeExport`. Note that the process holding the untrusted `.olean` files is now Lake rather than the smaller `leanexport`. The containment is the same, and the process that reports the verdict still never maps them, which is what the wording in `Lake.Check` and in `lake help check` now says. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 2, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 2, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Sep 2, 2026
Member
|
@Kha The |
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
3 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