feat: add leanchecker-args input#162
Open
kim-em wants to merge 1 commit into
Open
Conversation
Expose an analog to `build-args`/`test-args` for the leanchecker step so users can pass verbosity flags (`-v`) or restrict checking to specific module prefixes without forking the action. Also useful for passing environment-adjacent flags by prefixing the whole shell invocation; users wanting to cap leanchecker's in-process parallel fan-out on memory-constrained runners can set `LEAN_NUM_THREADS` at the workflow/job level. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
kim-em
added a commit
to Vilin97/merely-true
that referenced
this pull request
Apr 22, 2026
Add a pointer to leanprover/lean-action#162 and an explanation of the conditions under which this manual shell loop can be collapsed back to `leanchecker: true` with an appropriate argument or env var. No behaviour change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
kim-em
added a commit
to merely-true/merely-true
that referenced
this pull request
Apr 22, 2026
* chore: bump Lean and Mathlib from v4.24.0 to v4.29.0 - Update lean-toolchain to leanprover/lean4:v4.29.0 - Update lakefile.toml mathlib rev to v4.29.0 - Update lake-manifest.json with new dependency revisions - Add MerelyTrue/Basic.lean placeholder (required by Lake v4.29.0 which now errors if the glob target directory doesn't exist) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * chore: retrigger ci for PR #24 * chore: retrigger CI after package alignment fix * fix: adapt codebase to v4.29.0 Mathlib API changes After rebasing onto current main, the v4.29.0 toolchain exposed breakages across the Landau module and related files: - push_neg deprecated -> push Not - ContDiff.differentiable/continuous_fderiv/.differentiableAt now takes n ≠ 0 instead of 1 ≤ n (and ⊤ ≠ 0 for le_top) - integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable now wants ∀ x ∈ tsupport, DifferentiableAt rather than Differentiable - Finset.prod_eq_mul_prod_diff_singleton signature changed - add_le_add_left/right swapped orientations - hasFDerivAt_integral_of_dominated_of_fderiv_le takes s ∈ nhds x₀ - Real.logb namespace moved -> explicit import - fderiv_deriv -> fderiv_apply_one_eq_deriv - Explicit integral evaluation for linarith goal in Section3Helpers - Workarounds for Mul.mul metavariable resolution in normSq * 0/1 - Ring-rewrite helpers for nlinarith in VelocityDecayInstance - gcongr replaces mismatched add_le_add_left in LogBoundHelpers Local `lake build --wfail` is clean. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * ci: use leanchecker for Lean v4.29.0 * ci: add infra gate workflow * chore: retrigger CI for PR #24 * chore: retrigger CI for PR #24 * ci: clear stale project oleans before leanchecker * ci: run leanchecker sequentially on leaf modules * ci: document future simplification of sequential leanchecker loop Add a pointer to leanprover/lean-action#162 and an explanation of the conditions under which this manual shell loop can be collapsed back to `leanchecker: true` with an appropriate argument or env var. No behaviour change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com> Co-authored-by: Kim Morrison <kim@tqft.net>
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.
Adds a
leanchecker-argsinput analogous tobuild-args/test-args,whose contents are appended to the
lake env leancheckerinvocation(both for the bundled toolchain binary and the external
lean4checkerfallback).
Motivating use case
Downstream projects with mathlib as a dependency currently hit OOMs when
running
leanchecker: trueonubuntu-latest(7 GB). The cause is theparallel
IO.asTaskfan-out in src/LeanChecker.lean:each target module loads its own copy of the transitive import
environment, and Lean's task scheduler runs up to
hardware_concurrency()of them concurrently. With all-of-mathlib in the import closure, that
doesn't fit on a hosted runner.
A workaround is to cap Lean's task scheduler to 1 thread via
LEAN_NUM_THREADS=1, but to do that today users have to dropleanchecker: trueand reimplement the step manually. Example of whatprojects are resorting to (shell loop with subprocess-per-module):
https://github.com/merely-true/merely-true/blob/bump-v4.29.0/.github/workflows/lean_action_ci.yml
leanchecker-argsdoesn't directly solve the OOM, but it's the minimumuseful surface so those projects can add their own target list
(
leanchecker-args: "MyPkg.Core MyPkg.Utils") or verbose output (-v)without forking the action. Once a
--jobs/ sequential flag lands inleancheckeritself, users can flip it through this input with nofurther action changes required.
Changes
leanchecker-argsinput (default:"")scripts/run_leanchecker.shpasses$LEANCHECKER_ARGSviaeval,matching the pattern in
scripts/lake_build.shTest plan
leanchecker-args: "-v"on a small test project producesper-module replay output
leanchecker-args: "NonexistentMod"fails with the usual"Could not find any oleans" error (args are being passed through)
🤖 Prepared with Claude Code