Bound grind’s LIA search with liaSteps (
356a7e5)
grind now has a new liaSteps configuration option to cap how many search steps the linear integer arithmetic solver will take. This prevents case-split blowups on hard goals, but makes the solver intentionally incomplete once the limit is hit.
Fix grind ring so coefficient rewrites don’t lose information (d16f714)
The ring solver now avoids destructive simplifications that could weaken equations in rings without [NoNatZeroDivisors], closing a completeness bug. The change also handles constant polynomials more carefully and keeps the basis consistent when coefficient divisibility blocks a rewrite.
Add experimental trace postprocessing for postprocess_traces (
3c080a4)
Lean gains a new postprocess_traces post in cmd command plus a supporting Lean.PostprocessTraces module. It lets users transform trace trees after a command runs, which is useful for filtering, hoisting, and reshaping large trace outputs in the editor.
Add String.Internal.ugetUTF8Byte for faster byte access (
af2bbc3)
A new internal UTF-8 byte accessor takes a USize index instead of Nat, reducing boxing overhead in tight loops. The runtime and tests were updated to exercise the new primitive.
Add frame inference via @[frameproc] to vcgen (
501e4e8)
vcgen now supports automatic frame inference through a @[frameproc] registry and a generalized framing model. This is a substantial extension to the do-notation verification pipeline, broadening framing beyond lattice meet to arbitrary join-preserving operators.
Move initializer-execution APIs to BaseIO (
db5c0cb)
Lean.initializing, enableInitializersExecution, and isInitializerExecutionEnabled were moved from IO to BaseIO, and the C entrypoint was adjusted accordingly. This is an API/runtime change with a documented breaking behavior change for lean_enable_initializer_execution.
