structure command

• #5511 allows structure parents to be type synonyms.

• #5531 allows default values for structure fields to be noncomputable.

rfl and apply_rfl tactics

• #3714, #3718 improve the rfl tactic and give better error messages.

• #3772 makes rfl no longer use kernel defeq for ground terms.

• #5329 tags Iff.refl with @[refl] (@Parcly-Taxel)

• #5359 ensures that the rfl tactic tries Iff.rfl (@Parcly-Taxel)

unfold tactic

• #4834 let unfold do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib unfold_let tactic.

omega tactic

• #5382 fixes spurious error in #5315

• #5523 supports Int.toNat

simp tactic

• #5479 lets simp apply rules with higher-order patterns.

induction tactic

• #5494 fixes induction’s "pre-tactic" block to always be indented, avoiding unintended uses of it.

ac_nf tactic

• #5524 adds ac_nf, a counterpart to ac_rfl, for normalizing expressions with respect to associativity and commutativity. Tests it with BitVec expressions.

bv_decide

• #5211 makes extractLsb' the primitive bv_decide understands, rather than extractLsb (@alexkeizer)

• #5365 adds bv_decide diagnoses.

• #5375 adds bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (@alexkeizer)

• #5423 enhances the rewriting rules of bv_decide

• #5433 presents the bv_decide counterexample at the API

• #5484 handles BitVec.ofNat with Nat fvars in bv_decide

• #5506, #5507 add bv_normalize rules.

• #5568 generalize the bv_normalize pipeline to support more general preprocessing passes

• #5573 gets bv_normalize up-to-date with the current BitVec rewrites

• Cleanups: #5408, #5493, #5578

Elaboration improvements

• #5266 preserve order of overapplied arguments in elab_as_elim procedure.

• #5510 generalizes elab_as_elim to allow arbitrary motive applications.

• #5283, #5512 refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit _ arguments now.

• #5376 modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.

• #5402 localizes universe metavariable errors to let bindings and fun binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.

• #5419 must not reduce ite in the discriminant of match-expression when reducibility setting is .reducible

• #5474 have autoparams report parameter/field on failure

• #5530 makes automatic instance names about types with hygienic names be hygienic.

Deriving handlers

• #5432 makes Repr deriving instance handle explicit type parameters

Functional induction

• #5364 adds more equalities in context, more careful cleanup.

Linters

• #5335 fixes the unused variables linter complaining about match/tactic combinations

• #5337 fixes the unused variables linter complaining about some wildcard patterns

Other fixes

• #4768 fixes a parse error when .. appears with a . on the next line

Metaprogramming

• #3090 handles level parameters in Meta.evalExpr (@eric-wieser)

• #5401 instance for Inhabited (TacticM α) (@alexkeizer)

• #5412 expose Kernel.check for debugging purposes

• #5556 improves the "invalid projection" type inference error in inferType.

• #5587 allows MVarId.assertHypotheses to set BinderInfo and LocalDeclKind.

• #5588 adds MVarId.tryClearMany', a variant of MVarId.tryClearMany.

#5205 decreases the latency of auto-completion in tactic blocks.

#5237 fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.

#5257 fixes several instances of incorrect auto-completions being reported.

#5299 allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.

#5312 fixes the server breaking when changing whitespace after the module header.

#5322 fixes several instances of auto-completion reporting non-existent namespaces.

#5428 makes sure to always report some recent file range as progress when waiting for elaboration.

#4979 make pretty printer escape identifiers that are tokens.

#5389 makes formatter use the current token table.

#5513 use breakable instead of unbreakable whitespace when formatting tokens.

#5222 reduces allocations in Json.compress.

#5231 upstreams Zero and NeZero

#5292 refactors Lean.Elab.Deriving.FromToJson (@arthur-adjedj)

#5415 implements Repr Empty (@TomasPuverle)

#5421 implements To/FromJSON Empty (@TomasPuverle)

Logic

• #5263 allows simplifying dite_not/decide_not with only Decidable (¬p).

• #5268 fixes binders on ite_eq_left_iff

• #5284 turns off Inhabited (Sum α β) instances

• #5355 adds simp lemmas for LawfulBEq

• #5374 add Nonempty instances for products, allowing more partial functions to elaborate successfully

• #5447 updates Pi instance names

• #5454 makes some instance arguments implicit

• #5456 adds heq_comm

• #5529 moves @[simp] from exists_prop' to exists_prop

Bool

• #5228 fills gaps in Bool lemmas

• #5332 adds notation ^^ for Bool.xor

• #5351 removes _root_.and (and or/not/xor) and instead exports/uses Bool.and (etc.).

BitVec

• #5240 removes BitVec simps with complicated RHS

• #5247 BitVec.getElem_zeroExtend

• #5248 simp lemmas for BitVec, improving confluence

• #5249 removes @[simp] from some BitVec lemmas

• #5252 changes BitVec.intMin/Max from abbrev to def

• #5278 adds BitVec.getElem_truncate (@tobiasgrosser)

• #5281 adds udiv/umod bitblasting for bv_decide (@bollu)

• #5297 BitVec unsigned order theoretic results

• #5313 adds more basic BitVec ordering theory for UInt

• #5314 adds toNat_sub_of_le (@bollu)

• #5357 adds BitVec.truncate lemmas

• #5358 introduces BitVec.setWidth to unify zeroExtend and truncate (@tobiasgrosser)

• #5361 some BitVec GetElem lemmas

• #5385 adds BitVec.ofBool_[and|or|xor]_ofBool theorems (@tobiasgrosser)

• #5404 more of BitVec.getElem_* (@tobiasgrosser)

• #5410 BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul} (@bollu)

• #5411 BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning (@bollu)

• #5413 adds _self, _zero, and _allOnes for BitVec.[and|or|xor] (@tobiasgrosser)

• #5416 adds LawCommIdentity + IdempotentOp for BitVec.[and|or|xor] (@tobiasgrosser)

• #5418 decidable quantifers for BitVec

• #5450 adds BitVec.toInt_[intMin|neg|neg_of_ne_intMin] (@tobiasgrosser)

• #5459 missing BitVec lemmas

• #5469 adds BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft] (@luisacicolini)

• #5478 adds BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight) (@luisacicolini)

• #5487 adds sdiv_eq, smod_eq to allow sdiv/smod bitblasting (@bollu)

• #5491 adds BitVec.toNat_[abs|sdiv|smod] (@tobiasgrosser)

• #5492 BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not) (@luisacicolini)

• #5499 BitVec.Lemmas - drop non-terminal simps (@tobiasgrosser)

• #5505 unsimps BitVec.divRec_succ'

• #5508 adds BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight… (@tobiasgrosser)

• #5554 adds Bitvec.[add, sub, mul]_eq_xor and width_one_cases (@luisacicolini)

List

• #5242 improve naming for List.mergeSort lemmas

• #5302 provide mergeSort comparator autoParam

• #5373 fix name of List.length_mergeSort

• #5377 upstream map_mergeSort

• #5378 modify signature of lemmas about mergeSort

• #5245 avoid importing List.Basic without List.Impl

• #5260 review of List API

• #5264 review of List API

• #5269 remove HashMap's duplicated Pairwise and Sublist

• #5271 remove @[simp] from List.head_mem and similar

• #5273 lemmas about List.attach

• #5275 reverse direction of List.tail_map

• #5277 more List.attach lemmas

• #5285 List.count lemmas

• #5287 use boolean predicates in List.filter

• #5289 List.mem_ite_nil_left and analogues

• #5293 cleanup of List.findIdx / List.take lemmas

• #5294 switch primes on List.getElem_take

• #5300 more List.findIdx theorems

• #5310 fix List.all/any lemmas

• #5311 fix List.countP lemmas

• #5316 List.tail lemma

• #5331 fix implicitness of List.getElem_mem

• #5350 List.replicate lemmas

• #5352 List.attachWith lemmas

• #5353 List.head_mem_head?

• #5360 lemmas about List.tail

• #5391 review of List.erase / List.find lemmas

• #5392 List.fold / attach lemmas

• #5393 List.fold relators

• #5394 lemmas about List.maximum?

• #5403 theorems about List.toArray

• #5405 reverse direction of List.set_map

• #5448 add lemmas about List.IsPrefix (@Command-Master)

• #5460 missing List.set_replicate_self

• #5518 rename List.maximum? to max?

• #5519 upstream List.fold lemmas

• #5520 restore @[simp] on List.getElem_mem etc.

• #5521 List simp fixes

• #5550 List.unattach and simp lemmas

• #5594 induction-friendly List.min?_cons

Array

• #5246 cleanup imports of Array.Lemmas

• #5255 split Init.Data.Array.Lemmas for better bootstrapping

• #5288 rename Array.data to Array.toList

• #5303 cleanup of List.getElem_append variants

• #5304 Array.not_mem_empty

• #5400 reorganization in Array/Basic

• #5420 make Array functions either semireducible or use structural recursion

• #5422 refactor DecidableEq (Array α)

• #5452 refactor of Array

• #5458 cleanup of Array docstrings after refactor

• #5461 restore @[simp] on Array.swapAt!_def

• #5465 improve Array GetElem lemmas

• #5466 Array.foldX lemmas

• #5472 @[simp] lemmas about List.toArray

• #5485 reverse simp direction for toArray_concat

• #5514 Array.eraseReps

• #5515 upstream Array.qsortOrd

• #5516 upstream Subarray.empty

• #5526 fix name of Array.length_toList

• #5527 reduce use of deprecated lemmas in Array

• #5534 cleanup of Array GetElem lemmas

• #5536 fix Array.modify lemmas

• #5551 upstream Array.flatten lemmas

• #5552 switch obvious cases of array "bang"[]! indexing to rely on hypothesis (@TomasPuverle)

• #5577 add missing simp to Array.size_feraseIdx

• #5586 Array/Option.unattach

Option

• #5272 remove @[simp] from Option.pmap/pbind and add simp lemmas

• #5307 restoring Option simp confluence

• #5354 remove @[simp] from Option.bind_map

• #5532 Option.attach

• #5539 fix explicitness of Option.mem_toList

Nat

• #5241 add @[simp] to Nat.add_eq_zero_iff

• #5261 Nat bitwise lemmas

• #5262 Nat.testBit_add_one should not be a global simp lemma

• #5267 protect some Nat bitwise theorems

• #5305 rename Nat bitwise lemmas

• #5306 add Nat.self_sub_mod lemma

• #5503 restore @[simp] to upstreamed Nat.lt_off_iff

Int

• #5301 rename Int.div/mod to Int.tdiv/tmod

• #5320 add ediv_nonneg_of_nonpos_of_nonpos to DivModLemmas (@sakehl)

Fin

• #5250 missing lemma about Fin.ofNat'

• #5356 Fin.ofNat' uses NeZero

• #5379 remove some @[simp]s from Fin lemmas

• #5380 missing Fin @[simp] lemmas

HashMap

• #5244 (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD)

• #5362 remove the last use of Lean.(HashSet|HashMap)

• #5369 HashSet.ofArray

• #5370 HashSet.partition

• #5581 Singleton/Insert/Union instances for HashMap/Set

• #5582 HashSet.all/any

• #5590 adding Insert/Singleton/Union instances for HashMap/Set.Raw

• #5591 HashSet.Raw.all/any

Monads

• #5463 upstream some monad lemmas

• #5464 adjust simp attributes on monad lemmas

• #5522 more monadic simp lemmas

Simp lemma cleanup

• #5251 remove redundant simp annotations

• #5253 remove Int simp lemmas that can't fire

• #5254 variables appearing on both sides of an iff should be implicit

• #5381 cleaning up redundant simp lemmas

#4685 fixes a typo in the C run_new_frontend signature

#4729 has IR checker suggest using noncomputable

#5143 adds a shared library for Lake

#5437 removes (syntactically) duplicate imports (@euprunin)

#5462 updates src/lake/lakefile.toml to the adjusted Lake build process

#5541 removes new shared libs before build to better support Windows

#5558 make lean.h compile with MSVC (@kant2002)

#5564 removes non-conforming size-0 arrays (@eric-wieser)

Reservoir build cache. Lake will now attempt to fetch a pre-built copy of the package from Reservoir before building it. This is only enabled for packages in the leanprover or leanprover-community organizations on versions indexed by Reservoir. Users can force Lake to build packages from the source by passing --no-cache on the CLI or by setting the LAKE_NO_CACHE environment variable to true. #5486, #5572, #5583, #5600, #5641, #5642.

#5504 lake new and lake init now produce TOML configurations by default.

#5878 fixes a serious issue where Lake would delete path dependencies when attempting to cleanup a dependency required with an incorrect name.

Breaking changes

• #5641 A Lake build of target within a package will no longer build a package's dependencies package-level extra target dependencies. At the technical level, a package's extraDep facet no longer transitively builds its dependencies’ extraDep facets (which include their extraDepTargets).

#3918 @[builtin_doc] attribute (@digama0)

#4305 explains the borrow syntax (@eric-wieser)

#5349 adds documentation for groupBy.loop (@vihdzp)

#5473 fixes typo in BitVec.mul docstring (@llllvvuu)

#5476 fixes typos in Lean.MetavarContext

#5481 removes mention of Lean.withSeconds (@alexkeizer)

#5497 updates documentation and tests for toUIntX functions (@TomasPuverle)

#5087 mentions that inferType does not ensure type correctness

Many fixes to spelling across the docstrings, (@euprunin): #5425 #5426 #5427 #5430 #5431 #5434 #5435 #5436 #5438 #5439 #5440 #5599

#5343 allows addition of release-ci label via comment (@thorimur)

#5344 sets check level correctly during workflow (@thorimur)

#5444 Mathlib's lean-pr-testing-NNNN branches should use Batteries' lean-pr-testing-NNNN branches

#5489 commit lake-manifest.json when updating lean-pr-testing branches

#5490 use separate secrets for commenting and branching in pr-release.yml