Kernel now uses full-width counts and indices (
de275a3)
Lean’s kernel and runtime stop truncating sizes, indices, task priorities, and inductive parameter counts to 32 bits. This fixes silent misbehavior for huge values and requires matching updates across core C++ headers and kernel code.
Runtime.deepCopy lands for object graphs (
588ab22)
A new Runtime.deepCopy primitive copies an entire object graph into fresh memory while preserving sharing. It supports the usual managed runtime objects, but explicitly excludes external objects and some mutable/runtime-state types until they become immutable.
Typeclass resolution cache becomes much more reusable (
9976cbd)
Lean now records which local instance classes and global instance-class changes a typeclass search actually consulted, so cache entries can be shared across more local contexts and invalidated more precisely. The result is a measurable build-time win for large projects like Mathlib.
vcgen gets better at simplifying and stepping through have/let bindings (
4ce1da3)
Verification-condition generation can now step past a have at the head of a spec precondition, mirroring the existing handling for let at the head of a program. This fixes goals that previously got stuck after elaboration and improves how vcgen reduces nested bindings.
vcgen now reduces matches on literal discriminants (ec23d65)
Verification conditions can now simplify match expressions whose discriminant is a literal, such as a string constant. That lets more goals collapse directly to the expected result instead of leaving an unreduced case split behind.
grind linarith handles ordered types without OrderedAdd (7633a28)
grind linarith no longer crashes on order facts over types like Fin and BitVec that have an order but no OrderedAdd instance. Those facts are now ignored in the linarith path and fall back to normal grind behavior when appropriate.
lia/grind keep variables introduced during backtracking (0aa84f0)
A kernel type-mismatch bug in proof terms generated by lia and grind is fixed by preserving variables created during model search/backtracking. This addresses failures in elimination steps that reused a variable introduced in a refuted branch.
Std.Time formatting and parsing are much more round-trippable (
07f1879)
The time library now parses many patterns back into the same values it formats, including flexible day periods, signed years, zone offsets with seconds, and more precise week/ordinal-date behavior. It also corrects several locale and pre-1970 edge cases in date/time formatting.
HTTP/1.1 headers use a simpler, faster multimap (14ad5ba)
Std.Http.Headers switches from an indexed multimap to a simpler array-backed multimap, making header construction and edits faster. The internal indexing module is removed in favor of a scan-based implementation.
HTTP/1.1 encoding now emits a single ByteArray (5d48bb6)
HTTP structure encoding is reworked to produce raw ByteArrays, cutting overhead in the request/response writer path. This is a substantial internal performance change for HTTP message generation.
Std.Http parser becomes more tolerant of split chunk extensions/trailers (
59d90ff)
The HTTP/1.1 parser now waits for more input when a chunk extension or trailer is split across reads instead of failing immediately. That makes incremental parsing more robust in streaming scenarios.
Runtime.deepCopy and VCGen changes tighten runtime and verification behavior (b04aef7)
Borrow inference avoids marking join-point parameters as borrowed when they receive owned literals, fixing a memory leak in compiled code. Separately, VCGen gets additional support for simplifying have bindings and more precise error handling around Std.Do/Std.WP goals.
Other misc changes
- CI/workflow updates, including PR auto-close and nightly-release policy tweaks.
- Small refactors in BV decide, equation-lemma generation, and LCNF helpers.
- Stage0 update and minor internal cleanups.
- Misc test additions and regressions for the above fixes.