ci: install landrun from master, drop comparator patch - #16
Merged
Conversation
kim-em
force-pushed
the
test-landrun-master
branch
from
April 17, 2026 09:01
a1588b2 to
6ac5da3
Compare
Henrik reports that landrun master already whitelists the ELF loader and handles elan's lake shim, so the patches/comparator-landrun.patch workaround should no longer be needed. Switch both CI workflows to install landrun from master, drop the comparator commit pin, and remove the patch entirely. Ref: leanprover/comparator#30 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
test-landrun-master
branch
from
April 17, 2026 23:33
f9b2c54 to
082c69f
Compare
Upstream lean4export master and comparator master have bumped to v4.30.0-rc2, but this repo's workspaces (and Mathlib) are still on v4.30.0-rc1. That toolchain skew produced "incompatible header" errors when lean4export tried to read Challenge.olean inside the sandbox. Pin lean4export to tag v4.30.0-rc1 and comparator to the commit that targets v4.30.0-rc1 (the same commit we used to pin for the patch). Keep the landrun @main fix — that is still the right change. Co-Authored-By: Claude Opus 4.7 (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.
Per Henrik's response in leanprover/comparator#30, landrun
masteralready whitelists the ELF loader and handles elan'slakeshim correctly. The@latesttag resolves to v0.1.15, which predates those fixes — that's why our workaround was ever needed.This PR:
go install github.com/zouuup/landrun/cmd/landrun@master0ff36dde148dfea82dbdcf3baf91d6e1a8195554(now tracks comparator master)patches/comparator-landrun.patchand itsgit applystepIf CI goes green here, we can close leanprover/comparator#30 with confirmation that landrun master fixes it.
Test plan
🤖 Prepared with Claude Code