review

RELEASES.md

@@ -10,7 +10,316 @@ of each version.
 
 v4.12.0
 ----------
-Development in progress.
+
+### Language features, tactics, and metaprograms
+
+* `bv_decide` tactic. This release introduces a new tactic for proving goals involving `BitVec` and `Bool`. It reduces the goal to a SAT instance that is refuted by an external solver, and the resulting LRAT proof is checked in Lean. This is used to synthesize a proof of the goal by reflection. As this process uses verified algorithms, proofs generated by this tactic use `Lean.ofReduceBool`, so this tactic includes the Lean compiler as part of the trusted code base. The external solver CaDiCaL is included with Lean and does not need to be installed separately to make use of `bv_decide`.
+
+  For example, we can use `bv_decide` to verify that a bit twiddling formula leaves at most one bit set:
+  ```lean
+  def popcount (x : BitVec 64) : BitVec 64 :=
+    let rec go (x pop : BitVec 64) : Nat → BitVec 64
+      | 0 => pop
+      | n + 1 => go (x >>> 2) (pop + (x &&& 1)) n
+    go x 0 64
+
+  example (x : BitVec 64) : popcount ((x &&& (x - 1)) ^^^ x) ≤ 1 := by
+    simp only [popcount, popcount.go]
+    bv_decide
+  ```
+  When the external solver fails to refute the SAT instance generated by `bv_decide`, it can report a counterexample:
+  ```lean
+  /--
+  error: The prover found a counterexample, consider the following assignment:
+  x = 0xffffffffffffffff#64
+  -/
+  #guard_msgs in
+  example (x : BitVec 64) : x < x + 1 := by
+    bv_decide
+  ```
+  
+  See `Lean.Elab.Tactic.BVDecide` for a more detailed overview, and look in `tests/lean/run/bv_*` for examples.
+
+  [#5013](https://github.com/leanprover/lean4/pull/5013), [#5074](https://github.com/leanprover/lean4/pull/5074), [#5100](https://github.com/leanprover/lean4/pull/5100), [#5113](https://github.com/leanprover/lean4/pull/5113), [#5137](https://github.com/leanprover/lean4/pull/5137), [#5203](https://github.com/leanprover/lean4/pull/5203), [#5212](https://github.com/leanprover/lean4/pull/5212), [#5220](https://github.com/leanprover/lean4/pull/5220).
+
+* `simp` tactic
+  * [#4988](https://github.com/leanprover/lean4/pull/4988) fixes a panic in the `reducePow` simproc.
+  * [#5071](https://github.com/leanprover/lean4/pull/5071) exposes the `index` option to the `dsimp` tactic, introduced to `simp` in [#4202](https://github.com/leanprover/lean4/pull/4202).
+  * [#5159](https://github.com/leanprover/lean4/pull/5159) fixes a panic at `Fin.isValue` simproc.
+  * [#5167](https://github.com/leanprover/lean4/pull/5167) and [#5175](https://github.com/leanprover/lean4/pull/5175) rename the `simpCtorEq` simproc to `reduceCtorEq` and makes it optional. (See breaking changes.)
+  * [#5187](https://github.com/leanprover/lean4/pull/5187) ensures `reduceCtorEq` is enabled in the `norm_cast` tactic.
+  * [#5073](https://github.com/leanprover/lean4/pull/5073) modifies the simp debug trace messages to tag with "dpre" and "dpost" instead of "pre" and "post" when in definitional rewrite mode. [#5054](https://github.com/leanprover/lean4/pull/5054) explains the `reduce` steps for `trace.Debug.Meta.Tactic.simp` trace messages.
+* `ext` tactic
+  * [#4996](https://github.com/leanprover/lean4/pull/4996) reduces default maximum iteration depth from 1000000 to 100.
+* `induction` tactic
+  * [#5117](https://github.com/leanprover/lean4/pull/5117) fixes a bug where `let` bindings in minor premises wouldn't be counted correctly.
+
+* `omega` tactic
+  * [#5157](https://github.com/leanprover/lean4/pull/5157) fixes a panic.
+
+* `conv` tactic
+  * [#5149](https://github.com/leanprover/lean4/pull/5149) improves `arg n` to handle subsingleton instance arguments.
+
+* [#5044](https://github.com/leanprover/lean4/pull/5044) upstreams the `#time` command.
+* [#5079](https://github.com/leanprover/lean4/pull/5079) makes `#check` and `#reduce` typecheck the elaborated terms.
+
+* **Incrementality**
+  * [#4974](https://github.com/leanprover/lean4/pull/4974) fixes regression where we would not interrupt elaboration of previous document versions.
+  * [#5004](https://github.com/leanprover/lean4/pull/5004) fixes a performance regression.
+  * [#5001](https://github.com/leanprover/lean4/pull/5001) disables incremental body elaboration in presence of `where` clauses in declarations.
+  * [#5018](https://github.com/leanprover/lean4/pull/5018) enables infotrees on the command line for ilean generation.
+  * [#5040](https://github.com/leanprover/lean4/pull/5040) and [#5056](https://github.com/leanprover/lean4/pull/5056) improve performance of info trees.
+  * [#5090](https://github.com/leanprover/lean4/pull/5090) disables incrementality in the `case .. | ..` tactic.
+
+* **Definitions**
+  * [#5016](https://github.com/leanprover/lean4/pull/5016) and [#5066](https://github.com/leanprover/lean4/pull/5066) add `clean_wf` tactic to clean up tactic state in `decreasing_by`. This can be disabled with `set_option debug.rawDecreasingByGoal false`.
+  * [#5055](https://github.com/leanprover/lean4/pull/5055) unifies equational theorems between structural and well-founded recursion.
+  * [#5041](https://github.com/leanprover/lean4/pull/5041) allows mutually recursive functions to use different parameter names among the “fixed parameter prefix”
+  * [#4154](https://github.com/leanprover/lean4/pull/4154) and [#5109](https://github.com/leanprover/lean4/pull/5109) add fine-grained equational lemmas for non-recursive functions. See breaking changes.
+  * [#5129](https://github.com/leanprover/lean4/pull/5129) unifies equation lemmas for recursive and non-recursive definitions. The `backward.eqns.deepRecursiveSplit` option can be set to `false` to get the old behavior. See breaking changes.
+  * [#5141](https://github.com/leanprover/lean4/pull/5141) adds `f.eq_unfold` lemmas. Now Lean produces the following zoo of rewrite rules:
+    ```
+    Option.map.eq_1      : Option.map f none = none
+    Option.map.eq_2      : Option.map f (some x) = some (f x)
+    Option.map.eq_def    : Option.map f p = match o with | none => none | (some x) => some (f x)
+    Option.map.eq_unfold : Option.map = fun f p => match o with | none => none | (some x) => some (f x)
+    ```
+    The `f.eq_unfold` variant is especially useful to rewrite with `rw` under binders.
+  * [#5136](https://github.com/leanprover/lean4/pull/5136) fixes bugs in recursion over predicates.
+
+* **Variable inclusion**
+  * [#5206](https://github.com/leanprover/lean4/pull/5206) documents that `include` currently only applies to theorems.
+
+* **Elaboration**
+  * [#4926](https://github.com/leanprover/lean4/pull/4926) fixes a bug where autoparam errors were associated to an incorrect source position.
+  * [#4833](https://github.com/leanprover/lean4/pull/4833) fixes an issue where cdot anonymous functions (e.g. `(· + ·)`) would not handle ambiguous notation correctly. Numbers the parameters, making this example expand as `fun x1 x2 => x1 + x2` rather than `fun x x_1 => x + x_1`.
+  * [#5037](https://github.com/leanprover/lean4/pull/5037) improves strength of the tactic that proves array indexing is in bounds.
+  * [#5119](https://github.com/leanprover/lean4/pull/5119) fixes a bug in the tactic that proves indexing is in bounds where it could loop in the presence of mvars.
+  * [#5072](https://github.com/leanprover/lean4/pull/5072) makes the structure type clickable in "not a field of structure" errors for structure instance notation.
+  * [#4717](https://github.com/leanprover/lean4/pull/4717) fixes a bug where mutual `inductive` commands could create terms that the kernel rejects.
+  * [#5142](https://github.com/leanprover/lean4/pull/5142) fixes a bug where `variable` could fail when mixing binder updates and declarations.
+
+* **Other fixes or improvements**
+  * [#5118](https://github.com/leanprover/lean4/pull/5118) changes the definition of the `syntheticHole` parser so that hovering over `_` in `?_` gives the docstring for synthetic holes.
+  * [#5173](https://github.com/leanprover/lean4/pull/5173) uses the emoji variant selector for ✅️,❌️,💥️ in messages, improving fonts selection.
+  * [#5183](https://github.com/leanprover/lean4/pull/5183) fixes a bug in `rename_i` where implementation detail hypotheses could be renamed.
+
+### Language server, widgets, and IDE extensions
+
+* [#4821](https://github.com/leanprover/lean4/pull/4821) resolves two language server bugs that especially affect Windows users. (1) Editing the header could result in the watchdog not correctly restarting the file worker, which would lead to the file seemingly being processed forever. (2) On an especially slow Windows machine, we found that starting the language server would sometimes not succeed at all. This PR also resolves an issue where we would not correctly emit messages that we received while the file worker is being restarted to the corresponding file worker after the restart.
+* [#5006](https://github.com/leanprover/lean4/pull/5006) updates the user widget manual.
+* [#5193](https://github.com/leanprover/lean4/pull/5193) updates the quickstart guide with the new display name for the Lean 4 extension ("Lean 4").
+* [#5185](https://github.com/leanprover/lean4/pull/5185) fixes a bug where over time "import out of date" messages would accumulate.
+* [#4900](https://github.com/leanprover/lean4/pull/4900) improves ilean loading performance by about a factor of two. Optimizes the JSON parser and the conversion from JSON to Lean data structures; see PR description for details.
+* **Other fixes or improvements**
+  * [#5031](https://github.com/leanprover/lean4/pull/5031) localizes an instance in `Lsp.Diagnostics`.
+
+### Pretty printing
+
+* [#4976](https://github.com/leanprover/lean4/pull/4976) introduces `@[app_delab]`, a macro for creating delaborators for particular constants. The `@[app_delab ident]` syntax resolves `ident` to its constant name `name` and then expands to `@[delab app.name]`.
+* [#4982](https://github.com/leanprover/lean4/pull/4982) fixes a bug where the pretty printer assumed structure projections were type correct (such terms can appear in type mismatch errors). Improves hoverability of `#print` output for structures.
+* [#5218](https://github.com/leanprover/lean4/pull/5218) and [#5239](https://github.com/leanprover/lean4/pull/5239) add `pp.exprSizes` debugging option. When true, each pretty printed expression is prefixed with `[size a/b/c]`, where `a` is the size without sharing, `b` is the actual size, and `c` is the size with the maximum possible sharing.
+
+### Library
+
+* [#5020](https://github.com/leanprover/lean4/pull/5020) swaps the parameters to `Membership.mem`. A purpose of this change is to make set-like `CoeSort` coercions to refer to the eta-expanded function `fun x => Membership.mem s x`, which can reduce in many computations. Another is that having the `s` argument first leads to better discrimination tree keys. (See breaking changes.)
+* `Array`
+  * [#4970](https://github.com/leanprover/lean4/pull/4970) adds `@[ext]` attribute to `Array.ext`.
+  * [#4957](https://github.com/leanprover/lean4/pull/4957) deprecates `Array.get_modify`.
+* `List`
+  * [#4995](https://github.com/leanprover/lean4/pull/4995) upstreams `List.findIdx` lemmas.
+  * [#5029](https://github.com/leanprover/lean4/pull/5029), [#5048](https://github.com/leanprover/lean4/pull/5048) and [#5132](https://github.com/leanprover/lean4/pull/5132) add `List.Sublist` lemmas, some upstreamed. [#5077](https://github.com/leanprover/lean4/pull/5077) fixes implicitness in refl/rfl lemma binders.  add `List.Sublist` theorems.
+  * [#5047](https://github.com/leanprover/lean4/pull/5047) upstreams `List.Pairwise` lemmas.
+  * [#5053](https://github.com/leanprover/lean4/pull/5053), [#5124](https://github.com/leanprover/lean4/pull/5124), and [#5161](https://github.com/leanprover/lean4/pull/5161) add `List.find?/findSome?/findIdx?` theorems.
+  * [#5039](https://github.com/leanprover/lean4/pull/5039) adds `List.foldlRecOn` and `List.foldrRecOn` recursion principles to prove things about `List.foldl` and `List.foldr`.
+  * [#5069](https://github.com/leanprover/lean4/pull/5069) upstreams `List.Perm`.
+  * [#5092](https://github.com/leanprover/lean4/pull/5092) and [#5107](https://github.com/leanprover/lean4/pull/5107) add `List.mergeSort` and a fast `@[csimp]` implementation.
+  * [#5103](https://github.com/leanprover/lean4/pull/5103) makes the simp lemmas for `List.subset` more aggressive.
+  * [#5106](https://github.com/leanprover/lean4/pull/5106) changes the statement of `List.getLast?_cons`.
+  * [#5123](https://github.com/leanprover/lean4/pull/5123) and [#5158](https://github.com/leanprover/lean4/pull/5158) add `List.range` and `List.iota` lemmas.
+  * [#5130](https://github.com/leanprover/lean4/pull/5130) adds `List.join` lemmas.
+  * [#5131](https://github.com/leanprover/lean4/pull/5131) adds `List.append` lemmas.
+  * [#5152](https://github.com/leanprover/lean4/pull/5152) adds `List.erase(|P|Idx)` lemmas.
+  * [#5127](https://github.com/leanprover/lean4/pull/5127) makes miscellaneous lemma updates.
+  * [#5153](https://github.com/leanprover/lean4/pull/5153) and [#5160](https://github.com/leanprover/lean4/pull/5160) add lemmas about `List.attach` and `List.pmap`.
+  * [#5164](https://github.com/leanprover/lean4/pull/5164), [#5177](https://github.com/leanprover/lean4/pull/5177), and [#5215](https://github.com/leanprover/lean4/pull/5215) add `List.find?` and `List.range'/range/iota` lemmas.
+  * [#5196](https://github.com/leanprover/lean4/pull/5196) adds `List.Pairwise_erase` and related lemmas.
+  * [#5151](https://github.com/leanprover/lean4/pull/5151) and [#5163](https://github.com/leanprover/lean4/pull/5163) improve confluence of `List` simp lemmas. [#5105](https://github.com/leanprover/lean4/pull/5105) and [#5102](https://github.com/leanprover/lean4/pull/5102) adjust `List` simp lemmas.
+  * [#5178](https://github.com/leanprover/lean4/pull/5178) removes `List.getLast_eq_iff_getLast_eq_some` as a simp lemma.
+  * [#5210](https://github.com/leanprover/lean4/pull/5210) reverses the meaning of `List.getElem_drop` and `List.getElem_drop'`.
+  * [#5214](https://github.com/leanprover/lean4/pull/5214) moves `@[csimp]` lemmas earlier where possible.
+* `Nat` and `Int`
+  * [#5104](https://github.com/leanprover/lean4/pull/5104) adds `Nat.add_left_eq_self` and relatives.
+  * [#5146](https://github.com/leanprover/lean4/pull/5146) adds missing `Nat.and_xor_distrib_(left|right)`.
+  * [#5148](https://github.com/leanprover/lean4/pull/5148) and [#5190](https://github.com/leanprover/lean4/pull/5190) improve `Nat` and `Int` simp lemma confluence.
+  * [#5165](https://github.com/leanprover/lean4/pull/5165) adjusts `Int` simp lemmas.
+  * [#5166](https://github.com/leanprover/lean4/pull/5166) adds `Int` lemmas relating `neg` and `emod`/`mod`.
+  * [#5208](https://github.com/leanprover/lean4/pull/5208) reverses the direction of the `Int.toNat_sub` simp lemma.
+  * [#5209](https://github.com/leanprover/lean4/pull/5209) adds `Nat.bitwise` lemmas.
+  * [#5230](https://github.com/leanprover/lean4/pull/5230) corrects the docstrings for integer division and modulus.
+* `Option`
+  * [#5128](https://github.com/leanprover/lean4/pull/5128) and [#5154](https://github.com/leanprover/lean4/pull/5154) add `Option` lemmas.
+* `BitVec`
+  * [#4889](https://github.com/leanprover/lean4/pull/4889) adds `sshiftRight` bitblasting.
+  * [#4981](https://github.com/leanprover/lean4/pull/4981) adds `Std.Associative` and `Std.Commutative` instances for `BitVec.[and|or|xor]`.
+  * [#4913](https://github.com/leanprover/lean4/pull/4913) enables `missingDocs` error for `BitVec` modules.
+  * [#4930](https://github.com/leanprover/lean4/pull/4930) makes parameter names for `BitVec` more consistent.
+  * [#5098](https://github.com/leanprover/lean4/pull/5098) adds `BitVec.intMin`. Introduces `boolToPropSimps` simp set for converting from boolean to propositional expressions.
+  * [#5200](https://github.com/leanprover/lean4/pull/5200) and [#5217](https://github.com/leanprover/lean4/pull/5217) rename `BitVec.getLsb` to `BitVec.getLsbD`, etc., to bring naming in line with `List`/`Array`/etc.
+  * **Theorems:** [#4977](https://github.com/leanprover/lean4/pull/4977), [#4951](https://github.com/leanprover/lean4/pull/4951), [#4667](https://github.com/leanprover/lean4/pull/4667), [#5007](https://github.com/leanprover/lean4/pull/5007), [#4997](https://github.com/leanprover/lean4/pull/4997), [#5083](https://github.com/leanprover/lean4/pull/5083), [#5081](https://github.com/leanprover/lean4/pull/5081), [#4392](https://github.com/leanprover/lean4/pull/4392)
+* `UInt`
+  * [#4514](https://github.com/leanprover/lean4/pull/4514) fixes naming convention for `UInt` lemmas.
+* `Std.HashMap` and `Std.HashSet`
+  * [#4943](https://github.com/leanprover/lean4/pull/4943) deprecates variants of hash map query methods. (See breaking changes.)
+  * [#4917](https://github.com/leanprover/lean4/pull/4917) switches the library and Lean to `Std.HashMap` and `Std.HashSet` almost everywhere.
+  * [#4954](https://github.com/leanprover/lean4/pull/4954) deprecates `Lean.HashMap` and `Lean.HashSet`.
+  * [#5023](https://github.com/leanprover/lean4/pull/5023) cleans up lemma parameters.
+
+* `Std.Sat` (for `bv_decide`)
+  * [#4933](https://github.com/leanprover/lean4/pull/4933) adds definitions of SAT and CNF.
+  * [#4953](https://github.com/leanprover/lean4/pull/4953) defines "and-inverter graphs" (AIGs) as described in section 3 of [Davis-Swords 2013](https://arxiv.org/pdf/1304.7861.pdf).
+
+* **Parsec**
+  * [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyong `String` such as `ByteArray`. (See breaking changes.)
+  * [#5115](https://github.com/leanprover/lean4/pull/5115) moves `Lean.Data.Parsec` to `Std.Internal.Parsec` for bootstrappng reasons.
+
+* `Thunk`
+  * [#4969](https://github.com/leanprover/lean4/pull/4969) upstreams `Thunk.ext`.
+
+* **IO**
+  * [#4973](https://github.com/leanprover/lean4/pull/4973) modifies `IO.FS.lines` to handle `\r\n` on all operating systems instead of just on Windows.
+  * [#5125](https://github.com/leanprover/lean4/pull/5125) adds `createTempFile` and `withTempFile` for creating temporary files that can only be read and written by the current user.
+
+* **Other fixes or improvements**
+  * [#4945](https://github.com/leanprover/lean4/pull/4945) adds `Array`, `Bool` and `Prod` utilities from LeanSAT.
+  * [#4960](https://github.com/leanprover/lean4/pull/4960) adds `Relation.TransGen.trans`.
+  * [#5012](https://github.com/leanprover/lean4/pull/5012) states `WellFoundedRelation Nat` using `<`, not `Nat.lt`.
+  * [#5011](https://github.com/leanprover/lean4/pull/5011) uses `≠` instead of `Not (Eq ...)` in `Fin.ne_of_val_ne`.
+  * [#5197](https://github.com/leanprover/lean4/pull/5197) upstreams `Fin.le_antisymm`.
+  * [#5042](https://github.com/leanprover/lean4/pull/5042) reduces usage of `refine'`.
+  * [#5101](https://github.com/leanprover/lean4/pull/5101) adds about `if-then-else` and `Option`.
+  * [#5112](https://github.com/leanprover/lean4/pull/5112) adds basic instances for `ULift` and `PLift`.
+  * [#5133](https://github.com/leanprover/lean4/pull/5133) and [#5168](https://github.com/leanprover/lean4/pull/5168) make fixes from running the simpNF linter over Lean.
+  * [#5156](https://github.com/leanprover/lean4/pull/5156) removes a bad simp lemma in `omega` theory.
+  * [#5155](https://github.com/leanprover/lean4/pull/5155) improves confluence of `Bool` simp lemmas.
+  * [#5162](https://github.com/leanprover/lean4/pull/5162) improves confluence of `Function.comp` simp lemmas.
+  * [#5191](https://github.com/leanprover/lean4/pull/5191) improves confluence of `if-then-else` simp lemmas.
+  * [#5147](https://github.com/leanprover/lean4/pull/5147) adds `@[elab_as_elim]` to `Quot.rec`, `Nat.strongInductionOn` and `Nat.casesStrongInductionOn`, and also renames the latter two to `Nat.strongRecOn` and `Nat.casesStrongRecOn` (deprecated in [#5179](https://github.com/leanprover/lean4/pull/5179)).
+  * [#5180](https://github.com/leanprover/lean4/pull/5180) disables some simp lemmas with bad discrimination tree keys.
+  * [#5189](https://github.com/leanprover/lean4/pull/5189) cleans up internal simp lemmas that had leaked.
+  * [#5198](https://github.com/leanprover/lean4/pull/5198) cleans up `allowUnsafeReducibility`.
+  * [#5229](https://github.com/leanprover/lean4/pull/5229) removes unused lemmas from some `simp` tactics.
+  * [#5199](https://github.com/leanprover/lean4/pull/5199) removes >6 month deprecations.
+
+### Lean internals
+
+* **Performance**
+  * Some core algorithms have been rewritten in C++ for performance.
+    * [#4910](https://github.com/leanprover/lean4/pull/4910) and [#4912](https://github.com/leanprover/lean4/pull/4912) reimplement `instantiateLevelMVars`.
+    * [#4915](https://github.com/leanprover/lean4/pull/4915), [#4922](https://github.com/leanprover/lean4/pull/4922), and [#4931](https://github.com/leanprover/lean4/pull/4931) reimplement `instantiateExprMVars`, 30% faster on a benchmark.
+  * [#4934](https://github.com/leanprover/lean4/pull/4934) has optimizations for the kernel's `Expr` equality test.
+  * [#4990](https://github.com/leanprover/lean4/pull/4990) fixes bug in hashing for the kernel's `Expr` equality test.
+  * [#4935](https://github.com/leanprover/lean4/pull/4935) and [#4936](https://github.com/leanprover/lean4/pull/4936) skip some `PreDefinition` transformations if they are not needed.
+  * [#5225](https://github.com/leanprover/lean4/pull/5225) adds caching for visited exprs at `CheckAssignmentQuick` in `ExprDefEq`.
+  * [#5226](https://github.com/leanprover/lean4/pull/5226) maximizes term sharing at `instantiateMVarDeclMVars`, used by `runTactic`.
+* **Diagnostics and profiling**
+  * [#4923](https://github.com/leanprover/lean4/pull/4923) adds profiling for `instantiateMVars` in `Lean.Elab.MutualDef`, which can be a bottleneck there.
+  * [#4924](https://github.com/leanprover/lean4/pull/4924) adds diagnostics for large theorems, controlled by the `diagnostics.threshold.proofSize` option.
+  * [#4897](https://github.com/leanprover/lean4/pull/4897) improves display of diagnostic results.
+* **Other fixes or improvements**
+  * [#4921](https://github.com/leanprover/lean4/pull/4921) cleans up `Expr.betaRev`.
+  * [#4940](https://github.com/leanprover/lean4/pull/4940) fixes tests by not writing directly to stdout, which is unreliable now that elaboration and reporting are executed in separate threads.
+  * [#4955](https://github.com/leanprover/lean4/pull/4955) documents that `stderrAsMessages` is now the default on the command line as well.
+  * [#4647](https://github.com/leanprover/lean4/pull/4647) adjusts documentation for building on macOS.
+  * [#4987](https://github.com/leanprover/lean4/pull/4987) makes regular mvar assignments take precedence over delayed ones in `instantiateMVars`. Normally delayed assignment metavariables are never directly assigned, but on errors Lean assigns `sorry` to unassigned metavariables.
+  * [#4967](https://github.com/leanprover/lean4/pull/4967) adds linter name to errors when a linter crashes.
+  * [#5043](https://github.com/leanprover/lean4/pull/5043) cleans up command line snapshots logic.
+  * [#5067](https://github.com/leanprover/lean4/pull/5067) minimizes some imports.
+  * [#5068](https://github.com/leanprover/lean4/pull/5068) generalizes the monad for `addMatcherInfo`.
+  * [f71a1f](https://github.com/leanprover/lean4/commit/f71a1fb4ae958fccb3ad4d48786a8f47ced05c15) adds missing test for [#5126](https://github.com/leanprover/lean4/issues/5126).
+  * [#5201](https://github.com/leanprover/lean4/pull/5201) restores a test.
+  * [#3698](https://github.com/leanprover/lean4/pull/3698) fixes a bug where label attributes did not pass on the attribute kind.
+  * Typos: [#5080](https://github.com/leanprover/lean4/pull/5080), [#5150](https://github.com/leanprover/lean4/pull/5150), [#5202](https://github.com/leanprover/lean4/pull/5202)
+
+### Compiler, runtime, and FFI
+
+* [#3106](https://github.com/leanprover/lean4/pull/3106) moves frontend to new snapshot architecture. Note that `Frontend.processCommand` and `FrontendM` are no longer used by Lean core, but they will be preserved.
+* [#4919](https://github.com/leanprover/lean4/pull/4919) adds missing include in runtime for `AUTO_THREAD_FINALIZATION` feature on Windows.
+* [#4941](https://github.com/leanprover/lean4/pull/4941) adds more `LEAN_EXPORT`s for Windows.
+* [#4911](https://github.com/leanprover/lean4/pull/4911) improves formatting of CLI help text for the frontend.
+* [#4950](https://github.com/leanprover/lean4/pull/4950) improves file reading and writing.
+  * `readBinFile` and `readFile` now only require two system calls (`stat` + `read`) instead of one `read` per 1024 byte chunk.
+  * `Handle.getLine` and `Handle.putStr` no longer get tripped up by NUL characters.
+* [#4971](https://github.com/leanprover/lean4/pull/4971) handles the SIGBUS signal when detecting stack overflows.
+* [#5062](https://github.com/leanprover/lean4/pull/5062) avoids overwriting existing signal handlers, like in [rust-lang/rust#69685](https://github.com/rust-lang/rust/pull/69685).
+* [#4860](https://github.com/leanprover/lean4/pull/4860) improves workarounds for building on Windows. Splits `libleanshared` on Windows to avoid symbol limit, removes the `LEAN_EXPORT` denylist workaround, adds missing `LEAN_EXPORT`s.
+* [#4952](https://github.com/leanprover/lean4/pull/4952) output panics into Lean's redirected stderr, ensuring panics ARE visible as regular messages in the language server and properly ordered in relation to other messages on the command line.
+* [#4963](https://github.com/leanprover/lean4/pull/4963) links LibUV.
+
+### Lake
+
+* [#5030](https://github.com/leanprover/lean4/pull/5030) removes dead code.
+* [#4770](https://github.com/leanprover/lean4/pull/4770) adds additional fields to the package configuration which will be used by Reservoir. See the PR description for details.
+
+
+### DevOps/CI
+* [#4914](https://github.com/leanprover/lean4/pull/4914) and [#4937](https://github.com/leanprover/lean4/pull/4937) improve the release checklist.
+* [#4925](https://github.com/leanprover/lean4/pull/4925) ignores stale leanpkg tests.
+* [#5003](https://github.com/leanprover/lean4/pull/5003) upgrades `actions/cache` in CI.
+* [#5010](https://github.com/leanprover/lean4/pull/5010) sets `save-always` in cache actions in CI.
+* [#5008](https://github.com/leanprover/lean4/pull/5008) adds more libuv search patterns for the speedcenter.
+* [#5009](https://github.com/leanprover/lean4/pull/5009) reduce number of runs in the speedcenter for "fast" benchmarks from 10 to 3.
+* [#5014](https://github.com/leanprover/lean4/pull/5014) adjusts lakefile editing to use new `git` syntax in `pr-release` workflow.
+* [#5025](https://github.com/leanprover/lean4/pull/5025) has `pr-release` workflow pass `--retry` to `curl`.
+* [#5022](https://github.com/leanprover/lean4/pull/5022) builds MacOS Aarch64 release for PRs by default.
+* [#5045](https://github.com/leanprover/lean4/pull/5045) adds libuv to the required packages heading in macos docs.
+* [#5034](https://github.com/leanprover/lean4/pull/5034) fixes the install name of `libleanshared_1` on macOS.
+* [#5051](https://github.com/leanprover/lean4/pull/5051) fixes Windows stage 0.
+* [#5052](https://github.com/leanprover/lean4/pull/5052) fixes 32bit stage 0 builds in CI.
+* [#5057](https://github.com/leanprover/lean4/pull/5057) avoids rebuilding `leanmanifest` in each build.
+* [#5099](https://github.com/leanprover/lean4/pull/5099) makes `restart-on-label` workflow also filter by commit SHA.
+* [#4325](https://github.com/leanprover/lean4/pull/4325) adds CaDiCaL.
+
+### Breaking changes
+
+* [LibUV](https://libuv.org/) is now required to build Lean. This change only affects developers who compile Lean themselves instead of obtaining toolchains via `elan`. We have updated the official build instructions with information on how to obtain LibUV on our supported platforms. ([#4963](https://github.com/leanprover/lean4/pull/4963))
+
+* Recursive definitions with a `decreasing_by` clause that begins with `simp_wf` may break. Try removing `simp_wf` or replacing it with `simp`. ([#5016](https://github.com/leanprover/lean4/pull/5016))
+
+* The behavior of `rw [f]` where `f` is a non-recursive function defined by pattern matching changed.
+
+  For example, preciously, `rw [Option.map]` would rewrite `Option.map f o` to `match o with … `. Now this rewrite fails because it will use the equational lemmas, and these require constructors – just like for `List.map`.
+
+  Remedies:
+  * Split on `o` before rewriting.
+  * Use `rw [Option.map.eq_def]`, which rewrites any (saturated) application of `Option.map`.
+  * Use `set_option backward.eqns.nonrecursive false` when *defining* the function in question.
+  ([#4154](https://github.com/leanprover/lean4/pull/4154))
+
+* The unified handling of equation lemmas for recursive and non-recursive functions can break existing code, as there now can be extra equational lemmas:
+
+  * Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed.
+
+  * Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained.
+
+    In this case either case analysis on the parameters before rewriting helps, or setting the option `backward.eqns.deepRecursiveSplit false` while *defining* the function.
+
+  ([#5129](https://github.com/leanprover/lean4/pull/5129), [#5207](https://github.com/leanprover/lean4/pull/5207))
+
+* The `reduceCtorEq` simproc is now optional, and it might need to be included in lists of simp lemmas, like `simp only [reduceCtorEq]`. This simproc is responsible for reducing equalities of constructors. ([#5167](https://github.com/leanprover/lean4/pull/5167))
+
+* `Nat.strongInductionOn` is now `Nat.strongRecOn` and `Nat.caseStrongInductionOn` to `Nat.caseStrongRecOn`. ([#5147](https://github.com/leanprover/lean4/pull/5147))
+
+* The parameters to `Membership.mem` have been swapped, which affects all `Membership` instances. ([#5020](https://github.com/leanprover/lean4/pull/5020))
+
+* The meanings of `List.getElem_drop` and `List.getElem_drop'` have been reversed and the first is now a simp lemma. ([#5210](https://github.com/leanprover/lean4/pull/5210))
+
+* The `Parsec` library has moved from `Lean.Data.Parsec` to `Std.Internal.Parsec`. The `Parsec` type is now more general with a parameter for an iterable. Users parsing strings can migrate to `Parser` in the `Std.Internal.Parsec.String` namespace, which also includes string-focused parsing combinators. ([#4774](https://github.com/leanprover/lean4/pull/4774))
+
+* The `Lean` module has switched from `Lean.HashMap` and `Lean.HashSet` to `Std.HashMap` and `Std.HashSet` ([#4943](https://github.com/leanprover/lean4/pull/4943)). `Lean.HashMap` and `Lean.HashSet` are now deprecated ([#4954](https://github.com/leanprover/lean4/pull/4954)) and will be removed in a future release. Users of `Lean` APIs that interact with hash maps, for example `Lean.Environment.const2ModIdx`, might encounter minor breakage due to the following changes from `Lean.HashMap` to `Std.HashMap`:
+  * query functions use the term `get` instead of `find`, ([#4943](https://github.com/leanprover/lean4/pull/4943))
+  * the notation `map[key]` no longer returns an optional value but instead expects a proof that the key is present in the map. The previous behavior is available via the `map[key]?` notation.
+
 
 v4.11.0
 ----------
@@ -21,7 +330,7 @@ v4.11.0
 
   See breaking changes below.
 
-  PRs: [#4883](https://github.com/leanprover/lean4/pull/4883), [1242ff](https://github.com/leanprover/lean4/commit/1242ffbfb5a79296041683682268e770fc3cf820), [#5000](https://github.com/leanprover/lean4/pull/5000), [#5036](https://github.com/leanprover/lean4/pull/5036), [#5138](https://github.com/leanprover/lean4/pull/5138), [0edf1b](https://github.com/leanprover/lean4/commit/0edf1bac392f7e2fe0266b28b51c498306363a84).
+  PRs: [#4883](https://github.com/leanprover/lean4/pull/4883), [#4814](https://github.com/leanprover/lean4/pull/4814), [#5000](https://github.com/leanprover/lean4/pull/5000), [#5036](https://github.com/leanprover/lean4/pull/5036), [#5138](https://github.com/leanprover/lean4/pull/5138), [0edf1b](https://github.com/leanprover/lean4/commit/0edf1bac392f7e2fe0266b28b51c498306363a84).
 
 * **Recursive definitions**
   * Structural recursion can now be explicitly requested using

releases_drafts/hashmap.md

@@ -1,3 +0,0 @@
-* The `Lean` module has switched from `Lean.HashMap` and `Lean.HashSet` to `Std.HashMap` and `Std.HashSet`. `Lean.HashMap` and `Lean.HashSet` are now deprecated and will be removed in a future release. Users of `Lean` APIs that interact with hash maps, for example `Lean.Environment.const2ModIdx`, might encounter minor breakage due to the following breaking changes from `Lean.HashMap` to `Std.HashMap`:
-    * query functions use the term `get` instead of `find`,
-    * the notation `map[key]` no longer returns an optional value but expects a proof that the key is present in the map instead. The previous behavior is available via the `map[key]?` notation.

releases_drafts/libuv.md

@@ -1 +0,0 @@
-* #4963 [LibUV](https://libuv.org/) is now required to build Lean. This change only affects developers who compile Lean themselves instead of obtaining toolchains via `elan`. We have updated the official build instructions with information on how to obtain LibUV on our supported platforms.