Repository navigation
Conversation
added 3 commits
September 23, 2026 12:42
Adds a `lake-check` input that runs `lake check` (added in Lean `v4.35.0-rc1`): it builds the project, exports it, and replays the result through one or more kernels inside a bubblewrap sandbox, erroring on any use of a non-standard axiom. `lake-check: "true"` uses Lean's own kernel. `"paranoid"` (`--paranoid`, added in `v4.35.0-rc2`) additionally runs every checker the toolchain bundles: `leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and `con-ron`. Release toolchains ship all five, so nothing is cloned or compiled. Support is feature-detected from the content of `lake check --help` rather than from version strings, because toolchains are frequently nightlies or PR builds whose versions do not order usefully. A Lake without `lake check` prints its top-level help and still exits 0, so the detection cannot key off the exit status. A requested check that cannot run is an error rather than a silent pass. The sandbox is probed before the check runs, because `lake check` exits 1 both when it rejects a project and when bubblewrap fails to start, and reporting a sandbox failure as a rejection would blame the project for a setup problem. The probe's diagnostic decides which remedy the error names: a denied uid map means the runner restricts user namespaces, while a denied `pivot_root` means the job is in a container and needs a privileged one. This script does not build the project. `lake check` builds it inside the sandbox, and whether it is also built on the runner first is the `build` input's business, so running one unconditionally here would override that choice.
`nanoda: true` currently installs a Rust toolchain, clones and builds `lean4export`, then clones and builds `nanoda_lib` from a branch rather than a release, on every run. Recent release toolchains ship `leanexport` and `nanoda_bin` already, matched to each other and to the compiler that produced the oleans, so prefer those when they are present. Older toolchains keep the source-build path unchanged. The axioms permitted are the same either way, so this changes what the step costs and not what it accepts. Also deprecates `nanoda` and `nanoda-allow-sorry` in favour of `lake-check: paranoid`, which runs nanoda alongside every other bundled checker. The warning and the documentation are explicit that one case has no migration: `lake check` permits only the standard axioms and cannot be told to tolerate `sorryAx`, so a project that relies on `nanoda-allow-sorry: true` should stay on this input for now. The functional test asserts both that the check still passes on a toolchain that bundles the binaries and that no source build happened, since the saving is the point of the change.
`elan` sets the default toolchain without downloading it, so the precondition step ran 40ms after `elan-init` and found no toolchain directory at all. Move it after `lake update`, which is the first thing that actually uses the toolchain.
`lake init foo lib` on a current toolchain writes `name = "foo"` at the top level of `lakefile.toml`, with no `[package]` section and a library called `Foo`. Looking only for a package name therefore found nothing, and `nanoda` failed with "Could not detect module name from lakefile.toml or lakefile.lean" before it checked anything. Prefer `defaultTargets`, then the first `lean_lib`, then the `[package]` name. The first two name a module to export; a package name need not be one.
Resolve the CHANGELOG conflict with the SHA pinning of #193, and pin the checkout steps this PR adds to the same SHA. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Resolve the CHANGELOG conflict with the SHA pinning of #193, and pin the checkout steps this PR adds to the same SHA. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The deprecation of `nanoda` points users at `lake-check: paranoid`, which #190 adds, so this PR now builds on it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Keep this PR's CHANGELOG entries under Unreleased; the automatic merge had placed them inside the already-released v1.6.1 section. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
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
1 participant
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 makes
nanoda: trueuse theleanexportandnanoda_binthat recent release toolchains ship, instead of installing a Rust toolchain and buildinglean4exportandnanoda_libfrom source on every run. The bundled binaries are matched to each other and to the compiler that produced the.oleanfiles, where the source path pinnednanoda_libto a branch rather than a release. Toolchains that ship neither keep the existing path unchanged.The permitted axioms are identical on both paths, so this changes what the step costs, not what it accepts.
It also deprecates
nanodaandnanoda-allow-sorryin favour oflake-check: paranoid, which runs nanoda alongside every other bundled checker. One case has no migration, and the warning and the documentation say so rather than implying a clean swap:lake checkpermits only the standard axioms and cannot be told to toleratesorryAx, so a project relying onnanoda-allow-sorry: trueshould stay on this input for now.lake check --allow-sorrywould close that gap, and is worth requesting upstream.Nothing here delegates
nanodatolake check. Doing so would widen the check from one kernel to five for someone who asked only for nanoda, and would change the axiom policy underneath projects that carry asorry.A functional test asserts both halves of the claim: that the check still passes on a toolchain bundling the binaries, and that no source build happened, since avoiding that is the point.
🤖 Prepared with Claude+Codex