[kim-em]

This PR 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. The reference manual places this among the other ways to validate a proof, in Validating a Lean Proof. 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.

The script does not build the project itself. lake check builds it inside the sandbox, and whether it is also built on the runner first is the build input's business: leaving build on is faster, because lake check then starts from a populated .lake, while build: false keeps the project's code off the runner. Building unconditionally here would take that choice away.

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 own diagnostic picks the remedy the error names: a denied uid map means the runner restricts user namespaces, while a denied pivot_root means the job is running in a container and needs a privileged one.

Those two cases are the two runner families this was tested against. GitHub-hosted runners restrict user namespaces, so they need them granted before lean-action is called, which the README shows. Namespace runners fail differently, at pivot_root, for root as well as for the job user, and need namespace-features:container.privileged=true with the -with-features suffix on the machine label; such a container permits user namespaces too, so it needs nothing else. Automating the GitHub-hosted case is deliberately left to a follow-up, because it means running sudo to change a runner's security posture and deserves its own review.

Two functional tests, pinned to v4.35.0-rc2, cover this: paranoid on a privileged Namespace runner, asserting it passes on a clean package and fails once a sorry is introduced, and one asserting an unsupported toolchain fails loudly. The second pins the legacy toolchain rather than the moving default, so that it cannot quietly stop testing feature detection once the default gains lake check.

🤖 Prepared with Claude+Codex

[austinletson]

Thanks @kim-em. Looking forward to using lake check!

Would you be open to simplifying run_lake_check.sh in the spirit of being a wrapper around upstream lake messages, encoding only the failure modes that must be handled in lean-action?

Some of the script reproduces errors Lake already reports clearly, and the rest adds complexity we may not need. Running it locally:

Toolchain	Command	Lake's output	Exit
v4.26.0	lake check	error: unknown command 'check'	1
v4.26.0 / v4.35.0-rc1	lake check --paranoid	error: unknown long option '--paranoid'	1

So I think we can drop the help-text feature detection, the --paranoid detection, the ^bwrap: log scraping, and the exit-code-to-message mapping.

I'd keep the mode validation, the uname check (otherwise macOS runners fail in the bubblewrap install with a misleading message), the bubblewrap install, the lake-check-status output, and the sandbox probe with its runner-specific hints. A sandbox failure is the most likely first failure on ubuntu-latest, and the raw bwrap error (e.g. setting up uid map: Permission denied) doesn't tell users what to do.

One ordering caveat: since the probe runs before lake check, an old toolchain on ubuntu-latest would hit the sandbox error before the version error. Stating the version requirement in the failure messages, e.g. "lake check requires Lean v4.35.0-rc1+ (paranoid: rc2+)", would cover that. The lake_check_unsupported test would then need to run where the sandbox works (e.g. after a sudo sysctl step on ubuntu-latest) to keep exercising the version path.

Thoughts?