Repository navigation
Use toolchain Lake comparator for evaluation - #665
Merged
Merged
Conversation
kim-em
marked this pull request as ready for review
October 22, 2026 21:50
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
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.
Move generated workspaces from the standalone comparator/Landrun stack to the pinned toolchain's
lake comparator.lake testcontinues to enforce both Lean and bundled NanoDa, and scoring exposes the trusted shared package cache read-only inside Lake's bubblewrap sandboxes.The change removes separately built verifier tools, Landrun installation/version checks, and obsolete overrides. It ports the existing sandbox probes to Lake's isolation model, adds compact verdict/kernel-failure checks, regenerates all workspace drivers, and updates installation/security documentation. Mathematics and toolchain pins, statement adapters, submission whitelists, and score JSON are preserved. Historical replay remains independently pinned.
Prerequisite leanprover/lean-eval-submissions#2161 is merged and provisions bubblewrap for live jobs. Merging this PR switches newly archived submissions because the archive workflow freezes
lean-eval@main.Validation: warning-clean Lean builds and all Lean unit tests; 57 Python tests (one skipped); sandbox, secret-isolation, tool-path, descendant-cleanup, verdict and forced-NanoDa-failure probes passed locally. Full regeneration of 312 workspaces matches the committed drivers exactly. Final CI passed every job, including all eight catalog shards, aggregated inventory, installation, and exact-count scoring checks: https://github.com/leanprover/lean-eval/actions/runs/39858769533.
The real submissions adapter accepted the two expected proofs (including a definition hole and Lean Pool import), rejected the deliberately invalid third problem, and emitted the expected result JSON locally and on a fresh Namespace runner: https://github.com/leanprover/lean-eval/actions/runs/39859118231. A recorded accepted public submission, rwst/lean-eval@2f54444, also passed Lean and bundled NanoDa with current trusted adapters for
two_plus_tworevision 1.The companion cleanup leanprover/lean-eval-submissions#2162 removes the obsolete tool builds and selects Namespace 16 CPU / 32 GB. Server-dispatched jobs select the provisioning/cleanup revision through the existing protected dispatch-tag and Worker promotion workflow.