Lentil pins Lean v4.28.0. Please bump (or add CI coverage) for v4.30.0
and v4.31.0 so downstream projects on recent toolchains can require
Lentil instead of vendoring it.
The semantic core — Basic.lean, Util.lean, Utils/{MetaUtil,SyntaxUtil,MiscLemmas}.lean
— is Mathlib-free (Lean + Batteries only) and compiles unmodified under
v4.30.0 in our downstream build, so this looks like a lean-toolchain +
Batteries pin bump rather than a source change. (We haven't exercised
ProofMode, so that may need separate checking.)
Happy to open a PR with the toolchain/manifest bump.
Lentil pins Lean
v4.28.0. Please bump (or add CI coverage) forv4.30.0and
v4.31.0so downstream projects on recent toolchains canrequireLentil instead of vendoring it.
The semantic core —
Basic.lean,Util.lean,Utils/{MetaUtil,SyntaxUtil,MiscLemmas}.lean— is Mathlib-free (
Lean+Batteriesonly) and compiles unmodified underv4.30.0in our downstream build, so this looks like alean-toolchain+Batteriespin bump rather than a source change. (We haven't exercisedProofMode, so that may need separate checking.)Happy to open a PR with the toolchain/manifest bump.