lean4-htt/RELEASES.md

Lean 4 releases

We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals. There is not yet a strong guarantee of backwards compatibility between versions, only an expectation that breaking changes will be documented in this file.

This file contains work-in-progress notes for the upcoming release, as well as previous stable releases. Please check the releases page for the current status of each version.

v4.16.0

Language

• #3696 makes all message constructors handle pretty printer errors.

• #4460 runs all linters for a single command (together) on a separate thread from further elaboration, making a first step towards parallelizing the elaborator.

• #5757 makes it harder to create "fake" theorems about definitions that are stubbed-out with sorry by ensuring that each sorry is not definitionally equal to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from the elaborator) are now unique, except for elaboration errors, since making these unique tends to cause a confusing cascade of errors. In general, however, such sorries are labeled. This enables "go to definition" on sorry in the Infoview, which brings you to its origin. The option set_option pp.sorrySource true causes the pretty printer to show source position information on sorries.

• #6123 ensures that the configuration in Simp.Config is used when reducing terms and checking definitional equality in simp.

• #6204 lets _ be used in numeric literals as a separator. For example, 1_000_000, 0xff_ff or 0b_10_11_01_00. New lexical syntax:

numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]

• #6270 fixes a bug that could cause the injectivity tactic to fail in reducible mode, which could cause unfolding lemma generation to fail (used by tactics such as unfold). In particular, Lean.Meta.isConstructorApp'? was not aware that n + 1 is equivalent to Nat.succ n.

• #6273 modifies the "foo has been deprecated: use betterFoo instead" warning so that foo and betterFoo are hoverable.

• #6278 enables simp configuration options to be passed to norm_cast.

• #6286 ensure bv_decide uses definitional equality in its reflection procedure as much as possible. Previously it would build up explicit congruence proofs for the kernel to check. This reduces the size of proof terms passed to kernel speeds up checking of large reflection proofs.

• #6288 uses Lean.RArray in bv_decide's reflection proofs. Giving speedups on problems with lots of variables.

• #6295 sets up simprocs for all the remaining operations defined in Init.Data.Fin.Basic

• #6300 adds the debug.proofAsSorry option. When enabled, the proofs of theorems are ignored and replaced with sorry.

• #6330 removes unnecessary parameters from the funcion induction principles. This is a breaking change; broken code can typically be adjusted simply by passing fewer parameters.

• #6330 removes unnecessary parameters from the funcion induction principles. This is a breaking change; broken code can typically be adjusted simply by passing fewer parameters.

• #6362 adds the --error=kind option (shorthand: -Ekind) to the lean CLI. When set, messages of kind (e.g., linter.unusedVariables) will be reported as errors. This setting does nothing in interactive contexts (e.g., the server).

• #6366 adds support for Float32 and fixes a bug in the runtime.

• #6375 fixes a bug in the simplifier. It was producing terms with loose bound variables when eliminating unused let_fun expressions.

• #6378 adds an explanation to the error message when cases and induction are applied to a term whose type is not an inductive type. For Prop, these tactics now suggest the by_cases tactic. Example:

tactic 'cases' failed, major premise type is not an inductive type
  Prop

* [#6381](https://github.com/leanprover/lean4/pull/6381) fixes a bug in `withTrackingZetaDelta` and
`withTrackingZetaDeltaSet`. The `MetaM` caches need to be reset. See new
test.

* [#6385](https://github.com/leanprover/lean4/pull/6385) fixes a bug in `simp_all?` that caused some local declarations
to be omitted from the `Try this:` suggestions.

* [#6386](https://github.com/leanprover/lean4/pull/6386) ensures that `revertAll` clears auxiliary declarations when
invoked directly by users.

* [#6387](https://github.com/leanprover/lean4/pull/6387) fixes a type error in the proof generated by the `contradiction`
tactic.

* [#6397](https://github.com/leanprover/lean4/pull/6397) ensures that `simp` and `dsimp` do not unfold definitions that
are not intended to be unfolded by the user. See issue #5755 for an
example affected by this issue.

* [#6398](https://github.com/leanprover/lean4/pull/6398) ensures `Meta.check` check projections.

* [#6412](https://github.com/leanprover/lean4/pull/6412) adds reserved names for congruence theorems used in the
simplifier and `grind` tactics. The idea is prevent the same congruence
theorems to be generated over and over again.

* [#6413](https://github.com/leanprover/lean4/pull/6413) introduces the following features to the WIP `grind` tactic:
- `Expr` internalization.
- Congruence theorem cache.
- Procedure for adding new facts
- New tracing options
- New preprocessing steps: fold projections and eliminate dangling
`Expr.mdata`

* [#6414](https://github.com/leanprover/lean4/pull/6414) fixes a bug in `Lean.Meta.Closure` that would introduce
under-applied delayed assignment metavariables, which would keep them
from ever getting instantiated. This bug affected `match` elaboration
when the expected type contained postponed elaboration problems, for
example tactic blocks.

* [#6419](https://github.com/leanprover/lean4/pull/6419) fixes multiple bugs in the WIP `grind` tactic. It also adds
support for printing the `grind` internal state.

* [#6428](https://github.com/leanprover/lean4/pull/6428) adds a new preprocessing step to the `grind` tactic:
universe-level normalization. The goal is to avoid missing equalities in
the congruence closure module.

* [#6430](https://github.com/leanprover/lean4/pull/6430) adds the predicate `Expr.fvarsSet a b`, which returns `true` if
and only if the free variables in `a` are a subset of the free variables
in `b`.

* [#6433](https://github.com/leanprover/lean4/pull/6433) adds a custom type and instance canonicalizer for the (WIP)
`grind` tactic. The `grind` tactic uses congruence closure but
disregards types, type formers, instances, and proofs. Proofs are
ignored due to proof irrelevance. Types, type formers, and instances are
considered supporting elements and are not factored into congruence
detection. Instead, `grind` only checks whether elements are
structurally equal, which, in the context of the `grind` tactic, is
equivalent to pointer equality. See new tests for examples where the
canonicalizer is important.

* [#6435](https://github.com/leanprover/lean4/pull/6435) implements the congruence table for the (WIP) `grind` tactic. It
also fixes several bugs, and adds a new preprocessing step.

* [#6437](https://github.com/leanprover/lean4/pull/6437) adds support for detecting congruent terms in the (WIP) `grind`
tactic. It also introduces the `grind.debug` option, which, when set to
`true`, checks many invariants after each equivalence class is merged.
This option is intended solely for debugging purposes.

* [#6438](https://github.com/leanprover/lean4/pull/6438) ensures `norm_cast` doesn't fail to act in the presence of
`no_index` annotations

* [#6441](https://github.com/leanprover/lean4/pull/6441) adds basic truth value propagation rules to the (WIP) `grind`
tactic.

* [#6442](https://github.com/leanprover/lean4/pull/6442) fixes the `checkParents` sanity check in `grind`.

* [#6443](https://github.com/leanprover/lean4/pull/6443) adds support for propagating the truth value of equalities in
the (WIP) `grind` tactic.

* [#6447](https://github.com/leanprover/lean4/pull/6447) refactors `grind` and adds support for invoking the simplifier
using the `GrindM` monad.

* [#6448](https://github.com/leanprover/lean4/pull/6448) declares the command `builtin_grind_propagator` for registering
equation propagator for `grind`. It also declares the auxiliary the
attribute.

* [#6449](https://github.com/leanprover/lean4/pull/6449) completes the implementation of the command
`builtin_grind_propagator`.

* [#6452](https://github.com/leanprover/lean4/pull/6452) adds support for generating (small) proofs for any two
expressions that belong to the same equivalence class in the `grind`
tactic state.

* [#6453](https://github.com/leanprover/lean4/pull/6453) improves bv_decide's performance in the presence of large
literals.

* [#6455](https://github.com/leanprover/lean4/pull/6455) fixes a bug in the equality proof generator in the (WIP) `grind`
tactic.

* [#6456](https://github.com/leanprover/lean4/pull/6456) fixes another bug in the equality proof generator in the (WIP)
`grind` tactic.

* [#6457](https://github.com/leanprover/lean4/pull/6457) adds support for generating congruence proofs for congruences
detected by the `grind` tactic.

* [#6458](https://github.com/leanprover/lean4/pull/6458) adds support for compact congruence proofs in the (WIP) `grind`
tactic. The `mkCongrProof` function now verifies whether the congruence
proof can be constructed using only `congr`, `congrFun`, and `congrArg`,
avoiding the need to generate the more complex `hcongr` auxiliary
theorems.

* [#6459](https://github.com/leanprover/lean4/pull/6459) adds the (WIP) `grind` tactic. It currently generates a warning
message to make it clear that the tactic is not ready for production.

* [#6461](https://github.com/leanprover/lean4/pull/6461) adds a new propagation rule for negation to the (WIP) `grind`
tactic.

* [#6463](https://github.com/leanprover/lean4/pull/6463) adds support for constructors to the (WIP) `grind` tactic. When
merging equivalence classes, `grind` checks for equalities between
constructors. If they are distinct, it closes the goal; if they are the
same, it applies injectivity.

* [#6464](https://github.com/leanprover/lean4/pull/6464) completes support for literal values in the (WIP) `grind`
tactic. `grind` now closes the goal whenever it merges two equivalence
classes with distinct literal values.

* [#6465](https://github.com/leanprover/lean4/pull/6465) adds support for projection functions to the (WIP) `grind`
tactic.

* [#6466](https://github.com/leanprover/lean4/pull/6466) completes the implementation of `addCongrTable` in the (WIP)
`grind` tactic. It also adds a new test to demonstrate why the extra
check is needed. It also updates the field `cgRoot` (congruence root).

* [#6468](https://github.com/leanprover/lean4/pull/6468) fixes issue #6467

* [#6469](https://github.com/leanprover/lean4/pull/6469) adds support code for implementing e-match in the (WIP) `grind`
tactic.

* [#6470](https://github.com/leanprover/lean4/pull/6470) introduces a command for specifying patterns used in the
heuristic instantiation of global theorems in the `grind` tactic. Note
that this PR only adds the parser.

* [#6472](https://github.com/leanprover/lean4/pull/6472) implements the command `grind_pattern`. The new command allows
users to associate patterns with theorems. These patterns are used for
performing heuristic instantiation with e-matching. In the future, we
will add the attributes `@[grind_eq]`, `@[grind_fwd]`, and
`@[grind_bwd]` to compute the patterns automatically for theorems.

* [#6473](https://github.com/leanprover/lean4/pull/6473) adds a deriving handler for the `ToExpr` class. It can handle
mutual and nested inductive types, however it falls back to creating
`partial` instances in such cases. This is upstreamed from the Mathlib
deriving handler written by @kmill, but has fixes to handle autoimplicit
universe level variables.

* [#6474](https://github.com/leanprover/lean4/pull/6474) adds pattern validation to the `grind_pattern` command. The new
`checkCoverage` function will also be used to implement the attributes
`@[grind_eq]`, `@[grind_fwd]`, and `@[grind_bwd]`.

* [#6475](https://github.com/leanprover/lean4/pull/6475) adds support for activating relevant theorems for the (WIP)
`grind` tactic. We say a theorem is relevant to a `grind` goal if the
symbols occurring in its patterns also occur in the goal.

* [#6478](https://github.com/leanprover/lean4/pull/6478) internalize nested ground patterns when activating ematch
theorems in the (WIP) `grind` tactic.

* [#6481](https://github.com/leanprover/lean4/pull/6481) implements E-matching for the (WIP) `grind` tactic. We still
need to finalize and internalize the new instances.

* [#6484](https://github.com/leanprover/lean4/pull/6484) addresses a few error messages where diffs weren't being
exposed.

* [#6485](https://github.com/leanprover/lean4/pull/6485) implements `Grind.EMatch.instantiateTheorem` in the (WIP)
`grind` tactic.

* [#6487](https://github.com/leanprover/lean4/pull/6487) adds source position information for `structure` parent
projections, supporting "go to definition". Closes #3063.

* [#6488](https://github.com/leanprover/lean4/pull/6488) fixes and refactors the E-matching module for the (WIP) `grind`
tactic.

* [#6490](https://github.com/leanprover/lean4/pull/6490) adds basic configuration options for the `grind` tactic.

* [#6492](https://github.com/leanprover/lean4/pull/6492) fixes a bug in the theorem instantiation procedure in the (WIP)
`grind` tactic. For example, it was missing the following instance in
one of the tests:

* [#6497](https://github.com/leanprover/lean4/pull/6497) fixes another theorem instantiation bug in the `grind` tactic.
It also moves new instances to be processed to `Goal`.

* [#6498](https://github.com/leanprover/lean4/pull/6498) adds support in the `grind` tactic for propagating dependent
forall terms `forall (h : p), q[h]` where `p` is a proposition.

* [#6499](https://github.com/leanprover/lean4/pull/6499) fixes the proof canonicalizer for `grind`.

* [#6500](https://github.com/leanprover/lean4/pull/6500) fixes a bug in the `markNestedProofs` used in `grind`. See new
test.

* [#6502](https://github.com/leanprover/lean4/pull/6502) fixes a bug in the proof assembly procedure utilized by the
`grind` tactic.

* [#6503](https://github.com/leanprover/lean4/pull/6503) adds a simple strategy to the (WIP) `grind` tactic. It just
keeps internalizing new theorem instances found by E-matching. The
simple strategy can solve examples such as:

* [#6506](https://github.com/leanprover/lean4/pull/6506) adds the `monotonicity` tactic, intended to be used inside the
`partial_fixpoint` feature.

* [#6508](https://github.com/leanprover/lean4/pull/6508) fixes a bug in the sanity checkers for the `grind` tactic. See
the new test for an example of a case where it was panicking.

* [#6509](https://github.com/leanprover/lean4/pull/6509) fixes a bug in the congruence closure data structure used in the
`grind` tactic. The new test includes an example that previously caused
a panic. A similar panic was also occurring in the test
`grind_nested_proofs.lean`.

* [#6510](https://github.com/leanprover/lean4/pull/6510) adds a custom congruence rule for equality in `grind`. The new
rule takes into account that `Eq` is a symmetric relation. In the
future, we will add support for arbitrary symmetric relations. The
current rule is important for propagating disequalities effectively in
`grind`.

* [#6512](https://github.com/leanprover/lean4/pull/6512) introduces support for user-defined fallback code in the `grind`
tactic. The fallback code can be utilized to inspect the state of
failing `grind` subgoals and/or invoke user-defined automation. Users
can now write `grind on_failure <code>`, where `<code>` should have the
type `GoalM Unit`. See the modified tests in this PR for examples.

* [#6513](https://github.com/leanprover/lean4/pull/6513) adds support for (dependent) if-then-else terms (i.e., `ite` and
`dite` applications) in the `grind` tactic.

* [#6514](https://github.com/leanprover/lean4/pull/6514) enhances the assertion of new facts in `grind` by avoiding the
creation of unnecessary metavariables.

## Library

* [#6182](https://github.com/leanprover/lean4/pull/6182) adds `BitVec.[toInt|toFin]_concat` and moves a couple of
theorems into the concat section, as `BitVec.msb_concat` is needed for
the `toInt_concat` proof.

* [#6188](https://github.com/leanprover/lean4/pull/6188) completes the `toNat` theorems for the bitwise operations
(`and`, `or`, `xor`, `shiftLeft`, `shiftRight`) of the UInt types and
adds `toBitVec` theorems as well. It also renames `and_toNat` to
`toNat_and` to fit with the current naming convention.

* [#6238](https://github.com/leanprover/lean4/pull/6238) adds theorems characterizing the value of the unsigned shift
right of a bitvector in terms of its 2s complement interpretation as an
integer.
Unsigned shift right by at least one bit makes the value of the
bitvector less than or equal to `2^(w-1)`,
makes the interpretation of the bitvector `Int` and `Nat` agree.
In the case when `n = 0`, then the shift right value equals the integer
interpretation.

* [#6244](https://github.com/leanprover/lean4/pull/6244) changes the implementation of `HashMap.toList`, so the ordering
agrees with `HashMap.toArray`.

* [#6272](https://github.com/leanprover/lean4/pull/6272) introduces the basic theory of permutations of `Array`s and
proves `Array.swap_perm`.

* [#6282](https://github.com/leanprover/lean4/pull/6282) moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and
renames them to `Std.Channel` and `Std.Mutex`.

* [#6294](https://github.com/leanprover/lean4/pull/6294) upstreams `List.length_flatMap`, `countP_flatMap` and
`count_flatMap` from Mathlib. These were not possible to state before we
upstreamed `List.sum`.

* [#6315](https://github.com/leanprover/lean4/pull/6315) adds `protected` to `Fin.cast` and `BitVec.cast`, to avoid
confusion with `_root_.cast`. These should mostly be used via
dot-notation in any case.

* [#6316](https://github.com/leanprover/lean4/pull/6316) adds lemmas simplifying `for` loops over `Option` into
`Option.pelim`, giving parity with lemmas simplifying `for` loops of
`List` into `List.fold`.

* [#6317](https://github.com/leanprover/lean4/pull/6317) completes the basic API for BitVec.ofBool.

* [#6318](https://github.com/leanprover/lean4/pull/6318) generalizes the universe level for `Array.find?`, by giving it a
separate implementation from `Array.findM?`.

* [#6324](https://github.com/leanprover/lean4/pull/6324) adds `GetElem` lemmas for the basic `Vector` operations.

* [#6333](https://github.com/leanprover/lean4/pull/6333) generalizes the panic functions to a type of `Sort u` rather
than `Type u`. This better supports universe polymorphic types and
avoids confusing errors.

* [#6334](https://github.com/leanprover/lean4/pull/6334) adds `Nat` theorems for distributing `>>>` over bitwise
operations, paralleling those of `BitVec`.

* [#6338](https://github.com/leanprover/lean4/pull/6338) adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.

* [#6341](https://github.com/leanprover/lean4/pull/6341) generalizes `DecidableRel` to allow a heterogeneous relation.

* [#6353](https://github.com/leanprover/lean4/pull/6353) reproduces the API around `List.any/all` for `Array.any/all`.

* [#6364](https://github.com/leanprover/lean4/pull/6364) makes fixes suggested by the Batteries environment linters,
particularly `simpNF`, and `unusedHavesSuffices`.

* [#6365](https://github.com/leanprover/lean4/pull/6365) expands the `Array.set` and `Array.setIfInBounds` lemmas to
match existing lemmas for `List.set`.

* [#6367](https://github.com/leanprover/lean4/pull/6367) brings Vector lemmas about membership and indexing to parity
with List and Array.

* [#6369](https://github.com/leanprover/lean4/pull/6369) adds lemmas about `Vector.set`, `anyM`, `any`, `allM`, and
`all`.

* [#6376](https://github.com/leanprover/lean4/pull/6376) adds theorems about `==` on `Vector`, reproducing those already
on `List` and `Array`.

* [#6379](https://github.com/leanprover/lean4/pull/6379) replaces the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib.
(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.)
This subtly changes the notion of ordering on `List α`.

  `List.lt` was a weaker relation: in particular if `l₁ < l₂`, then `a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable (either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`.

  When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide.

  Mathlib was already overriding the order instances for `List α`, so this change should not be noticed by anyone already using Mathlib.

  We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`, via a `==` function which is weaker than strict equality.

* [#6390](https://github.com/leanprover/lean4/pull/6390) redefines `Range.forIn'` and `Range.forM`, in preparation for
writing lemmas about them.

* [#6391](https://github.com/leanprover/lean4/pull/6391) requires that the step size in `Std.Range` is positive, to avoid
ill-specified behaviour.

* [#6396](https://github.com/leanprover/lean4/pull/6396) adds lemmas reducing for loops over `Std.Range` to for loops
over `List.range'`.

* [#6399](https://github.com/leanprover/lean4/pull/6399) adds basic lemmas about lexicographic order on Array and Vector,
achieving parity with List.

* [#6423](https://github.com/leanprover/lean4/pull/6423) adds missing lemmas about lexicographic order on
List/Array/Vector.

* [#6477](https://github.com/leanprover/lean4/pull/6477) adds the necessary domain theory that backs the
`partial_fixpoint` feature.

## Compiler

* [#6311](https://github.com/leanprover/lean4/pull/6311) adds support for `HEq` to the new code generator.

* [#6348](https://github.com/leanprover/lean4/pull/6348) adds support for `Float32` to the Lean runtime.

* [#6350](https://github.com/leanprover/lean4/pull/6350) adds missing features and fixes bugs in the `Float32` support

* [#6383](https://github.com/leanprover/lean4/pull/6383) ensures the new code generator produces code for `opaque`
definitions that are not tagged as `@[extern]`.
Remark: This is the behavior of the old code generator.

* [#6405](https://github.com/leanprover/lean4/pull/6405) adds support for erasure of `Decidable.decide` to the new code
generator. It also adds a new `Probe.runOnDeclsNamed` function, which is
helpful for writing targeted single-file tests of compiler internals.

* [#6415](https://github.com/leanprover/lean4/pull/6415) fixes a bug in the `sharecommon` module, which was returning
incorrect results for objects that had already been processed by
`sharecommon`. See the new test for an example that triggered the bug.

* [#6429](https://github.com/leanprover/lean4/pull/6429) adds support for extern LCNF decls, which is required for parity
with the existing code generator.

## Pretty Printing

* [#5689](https://github.com/leanprover/lean4/pull/5689) adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.

* [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from the elaborator) are now unique, except for elaboration errors, since making these unique tends to cause a confusing cascade of errors. In general, however, such sorries are labeled. This enables "go to definition" on sorry in the Infoview, which brings you to its origin. The option set_option pp.sorrySource true causes the pretty printer to show source position information on sorries.

Documentation

• #6450 adds a docstring to the @[app_delab] attribute.

Server

• #6279 fixes a bug in structure instance field completion that caused it to not function correctly for bracketed structure instances written in Mathlib style.

• #6408 fixes a regression where goals that don't exist were being displayed. The regression was triggered by #5835 and originally caused by #4926.

Lake

• #6176 changes Lake's build process to no longer use leanc for compiling C files or linking shared libraries and executables. Instead, it directly invokes the bundled compiler (or the native compiler if none) using the necessary flags.

• #6289 adapts Lake modules to use prelude and includes them in the check-prelude CI.

• #6291 ensures the the log error position is properly preserved when prepending stray log entries to the job log. It also adds comparison support for Log.Pos.

• #6388 merges BuildJob and Job, deprecating the former. Job now contains a trace as part of its state which can be interacted with monadically. also simplifies the implementation of OpaqueJob.

• #6411 adds the ability to override package entries in a Lake manifest via a separate JSON file. This file can be specified on the command line with --packages or applied persistently by placing it at .lake/package-overrides.json.

• #6422 fixes a bug in #6388 where the Package.afterBuildCahe* functions would produce different traces depending on whether the cache was fetched.

Other

• #6285 upstreams the ToLevel typeclass from mathlib and uses it to fix the existing ToExpr instances so that they are truly universe polymorphic (previously it generated malformed expressions when the universe level was nonzero). We improve on the mathlib definition of ToLevel to ensure the class always lives in Type, irrespective of the universe parameter.

• #6363 fixes errors at load time in the comparison mode of the Firefox profiler.

v4.15.0

Language

• #4595 implements Simp.Config.implicitDefEqsProofs. When true (default: true), simp will not create a proof term for a rewriting rule associated with an rfl-theorem. Rewriting rules are provided by users by annotating theorems with the attribute @[simp]. If the proof of the theorem is just rfl (reflexivity), and implicitDefEqProofs := true, simp will not create a proof term which is an application of the annotated theorem.

• #5429 avoid negative environment lookup

• #5501 ensure instantiateMVarsProfiling adds a trace node

• #5856 adds a feature to the the mutual def elaborator where the instance command yields theorems instead of definitions when the class is a Prop.

• #5907 unset trailing for simpa? "try this" suggestion

• #5920 changes the rule for which projections become instances. Before, all parents along with all indirect ancestors that were represented as subobject fields would have their projections become instances. Now only projections for direct parents become instances.

• #5934 make all_goals admit goals on failure

• #5942 introduce synthetic atoms in bv_decide

• #5945 adds a new definition Message.kind which returns the top-level tag of a message. This is serialized as the new field kind in SerialMessaege so that i can be used by external consumers (e.g., Lake) to identify messages via lean --json.

• #5968 arg conv tactic misreported number of arguments on error

• #5979 BitVec.twoPow in bv_decide

• #5991 simplifies the implementation of omega.

• #5992 fix style in bv_decide normalizer

• #5999 adds configuration options for decide/decide!/native_decide and refactors the tactics to be frontends to the same backend. Adds a +revert option that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makes native_decide fail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once). Now native_decide supports universe polymorphism.

• #6010 changes bv_decide's configuration from lots of set_option to an elaborated config like simp or omega. The notable exception is sat.solver which is still a set_option such that users can configure a custom SAT solver globally for an entire project or file. Additionally it introduces the ability to set maxSteps for the simp preprocessing run through the new config.

• #6012 improves the validation of new syntactic tokens. Previously, the validation code had inconsistencies: some atoms would be accepted only if they had a leading space as a pretty printer hint. Additionally, atoms with internal whitespace are no longer allowed.

• #6016 removes the decide! tactic in favor of decide +kernel (breaking change).

• #6019 removes @[specilize] from MkBinding.mkBinding, which is a function that cannot be specialized (as none of its arguments are functions). As a result, the specializable function Nat.foldRevM.loop doesn't get specialized, which leads to worse performing code.

• #6022 makes the change tactic and conv tactic use the same elaboration strategy. It works uniformly for both the target and local hypotheses. Now change can assign metavariables, for example:

example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`

• #6024 fixes a bug where the monad lift coercion elaborator would partially unify expressions even if they were not monads. This could be taken advantage of to propagate information that could help elaboration make progress, for example the first change worked because the monad lift coercion elaborator was unifying @Eq _ _ with @Eq (Nat × Nat) p:

example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked

As such, this is a breaking change; you may need to adjust expressions to include additional implicit arguments.

• #6029 adds a normalization rule to bv_normalize (which is used by bv_decide) that converts x / 2^k into x >>> k under suitable conditions. This allows us to simplify the expensive division circuits that are used for bitblasting into much cheaper shifting circuits. Concretely, it allows for the following canonicalization:

• #6030 fixes simp only [· ∈ ·] after #5020.

• #6035 introduces the and flattening pre processing pass from Bitwuzla to bv_decide. It splits hypotheses of the form (a && b) = true into a = true and b = true which has synergy potential with the already existing embedded constraint substitution pass.

• #6037 fixes bv_decide's embedded constraint substitution to generate correct counter examples in the corner case where duplicate theorems are in the local context.

• #6045 add LEAN_ALWAYS_INLINE to some functions

• #6048 fixes simp? suggesting output with invalid indentation

• #6051 mark Meta.Context.config as private

• #6053 fixes the caching infrastructure for whnf and isDefEq, ensuring the cache accounts for all relevant configuration flags. It also cleans up the WHNF.lean module and improves the configuration of whnf.

• #6061 adds a simp_arith benchmark.

• #6062 optimize Nat.Linear.Expr.toPoly

• #6064 optimize Nat.Linear.Poly.norm

• #6068 improves the asymptotic performance of simp_arith when there are many variables to consider.

• #6077 adds options to bv_decide's configuration structure such that all non mandatory preprocessing passes can be disabled.

• #6082 changes how the canonicalizer handles forall and lambda, replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth on zulip.

• #6093 use mkFreshUserName in ArgsPacker

• #6096 improves the #print command for structures to show all fields and which parents the fields were inherited from, hiding internal details such as which parents are represented as subobjects. This information is still present in the constructor if needed. The pretty printer for private constants is also improved, and it now handles private names from the current module like any other name; private names from other modules are made hygienic.

• #6098 modifies Lean.MVarId.replaceTargetDefEq and Lean.MVarId.replaceLocalDeclDefEq to use Expr.equal instead of Expr.eqv when determining whether the expression has changed. This is justified on the grounds that binder names and binder infos are user-visible and affect elaboration.

• #6105 fixes a stack overflow caused by a cyclic assignment in the metavariable context. The cycle is unintentionally introduced by the structure instance elaborator.

• #6108 turn off pp.mvars in apply? results

• #6109 fixes an issue in the injection tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment. This issue was causing the error: "mvarId is already assigned" in issue #6066. The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.

• #6112 makes stricter requirements for the @[deprecated] attribute, requiring either a replacement identifier as @[deprecated bar] or suggestion text @[deprecated "Past its use by date"], and also requires a since := "..." field.

• #6114 liberalizes atom rules by allowing '' to be a prefix of an atom, after #6012 only added an exception for '' alone, and also adds some unit tests for atom validation.

• #6116 fixes a bug where structural recursion did not work when indices of the recursive argument appeared as function parameters in a different order than in the argument's type's definition.

• #6125 adds support for structure in mutual blocks, allowing inductive types defined by inductive and structure to be mutually recursive. The limitations are (1) that the parents in the extends clause must be defined before the mutual block and (2) mutually recursive classes are not allowed (a limitation shared by class inductive). There are also improvements to universe level inference for inductive types and structures. Breaking change: structure parents now elaborate with the structure in scope (fix: use qualified names or rename the structure to avoid shadowing), and structure parents no longer elaborate with autoimplicits enabled.

• #6128 does the same fix as #6104, but such that it doesn't break the test/the file in Plausible. This is done by not creating unused let binders in metavariable types that are made by elimMVar. (This is also a positive thing for users looking at metavariable types, for example in error messages)

• #6129 fixes a bug at isDefEq when zetaDelta := false. See new test for a small example that exposes the issue.

• #6131 fixes a bug at the definitional equality test (isDefEq). At unification constraints of the form c.{u} =?= c.{v}, it was not trying to unfold c. This bug did not affect the kernel.

• #6141 make use of recursive structures in snapshot types

• #6145 fixes the revert tactic so that it creates a syntheticOpaque metavariable as the new goal, instead of a natural metavariable

• #6146 fixes a non-termination bug that occurred when generating the match-expression splitter theorem. The bug was triggered when the proof automation for the splitter theorem repeatedly applied injection to the same local declaration, as it could not be removed due to forward dependencies. See issue #6065 for an example that reproduces this issue.

• #6165 modifies structure instance notation and where notation to use the same notation for fields. Structure instance notation now admits binders, type ascriptions, and equations, and where notation admits full structure lvals. Examples of these for structure instance notation:

structure PosFun where
  f : Nat → Nat
  pos : ∀ n, 0 < f n

- [#6168](https://github.com/leanprover/lean4/pull/6168) extends the "motive is not type correct" error message for the
rewrite tactic to explain what it means. It also pretty prints the
type-incorrect motive and reports the type error.

- [#6170](https://github.com/leanprover/lean4/pull/6170) adds core metaprogramming functions for forking off background
tasks from elaboration such that their results are visible to reporting
and the language server

- [#6175](https://github.com/leanprover/lean4/pull/6175) fixes a bug with the `structure`/`class` command where if there
are parents that are not represented as subobjects but which used other
parents as instances, then there would be a kernel error. Closes #2611.

- [#6180](https://github.com/leanprover/lean4/pull/6180) fixes a non-termination bug that occurred when generating the
match-expression equation theorems. The bug was triggered when the proof
automation for the equation theorem repeatedly applied `injection(` to
the same local declaration, as it could not be removed due to forward
dependencies. See issue #6067 for an example that reproduces this issue.

- [#6189](https://github.com/leanprover/lean4/pull/6189) changes how generalized field notation ("dot notation") resolves
the function. The new resolution rule is that if `x : S`, then `x.f`
resolves the name `S.f` relative to the root namespace (hence it now
affected by `export` and `open`). Breaking change: aliases now resolve
differently. Before, if `x : S`, and if `S.f` is an alias for `S'.f`,
then `x.f` would use `S'.f` and look for an argument of type `S'`. Now,
it looks for an argument of type `S`, which is more generally useful
behavior. Code making use of the old behavior should consider defining
`S` or `S'` in terms of the other, since dot notation can unfold
definitions during resolution.

- [#6206](https://github.com/leanprover/lean4/pull/6206) makes it possible to write `rw (occs := [1,2]) ...` instead of
`rw (occs := .pos [1,2]) ...` by adding a coercion from `List.Nat` to
`Lean.Meta.Occurrences`.

- [#6220](https://github.com/leanprover/lean4/pull/6220) adds proper support for `let_fun` in `simp`.

- [#6236](https://github.com/leanprover/lean4/pull/6236) fixes an issue where edits to a command containing a nested
docstring fail to reparse the entire command.

## Library

- [#4904](https://github.com/leanprover/lean4/pull/4904) introduces date and time functionality to the Lean 4 Std.

- [#5616](https://github.com/leanprover/lean4/pull/5616) is a follow-up to https://github.com/leanprover/lean4/pull/5609,
where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior
when the denominator is zero.

- [#5866](https://github.com/leanprover/lean4/pull/5866) verifies the `keys` function on `Std.HashMap`.

- [#5885](https://github.com/leanprover/lean4/pull/5885) add Int16/Int32/Int64

- [#5926](https://github.com/leanprover/lean4/pull/5926) add `Option.or_some'`

- [#5927](https://github.com/leanprover/lean4/pull/5927) `List.pmap_eq_self`

- [#5937](https://github.com/leanprover/lean4/pull/5937) upstream lemmas about Fin.foldX

- [#5938](https://github.com/leanprover/lean4/pull/5938) upstream List.ofFn and relate to Array.ofFn

- [#5941](https://github.com/leanprover/lean4/pull/5941) List.mapFinIdx, lemmas, relate to Array version

- [#5949](https://github.com/leanprover/lean4/pull/5949) consolidate `decide_True` and `decide_true_eq_true`

- [#5950](https://github.com/leanprover/lean4/pull/5950) relate Array.takeWhile with List.takeWhile

- [#5951](https://github.com/leanprover/lean4/pull/5951) remove @[simp] from BitVec.ofFin_sub and sub_ofFin

- [#5952](https://github.com/leanprover/lean4/pull/5952) relate Array.eraseIdx with List.eraseIdx

- [#5961](https://github.com/leanprover/lean4/pull/5961) define ISize and basic operations on it

- [#5969](https://github.com/leanprover/lean4/pull/5969) upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas

- [#5970](https://github.com/leanprover/lean4/pull/5970) deprecate Array.split in favour of identical Array.partition

- [#5971](https://github.com/leanprover/lean4/pull/5971) relate Array.isPrefixOf with List.isPrefixOf

- [#5972](https://github.com/leanprover/lean4/pull/5972) relate Array.zipWith/zip/unzip with List versions

- [#5974](https://github.com/leanprover/lean4/pull/5974) add another List.find?_eq_some lemma

- [#5981](https://github.com/leanprover/lean4/pull/5981) names the default SizeOf instance `instSizeOfDefault`

- [#5982](https://github.com/leanprover/lean4/pull/5982) minor lemmas about List.ofFn

- [#5984](https://github.com/leanprover/lean4/pull/5984) adds lemmas for `List` for the interactions between {`foldl`,
`foldr`, `foldlM`, `foldlrM`} and {`filter`, `filterMap`}.

- [#5985](https://github.com/leanprover/lean4/pull/5985) relates the operations `findSomeM?`, `findM?`, `findSome?`, and
`find?` on `Array` with the corresponding operations on `List`, and also
provides simp lemmas for the `Array` operations `findSomeRevM?`,
`findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the
usual forward find operations).

- [#5987](https://github.com/leanprover/lean4/pull/5987) BitVec.getMsbD in bv_decide

- [#5988](https://github.com/leanprover/lean4/pull/5988) changes the signature of `Array.set` to take a `Nat`, and a
tactic-provided bound, rather than a `Fin`.

- [#5995](https://github.com/leanprover/lean4/pull/5995) BitVec.sshiftRight' in bv_decide

- [#6007](https://github.com/leanprover/lean4/pull/6007) List.modifyTailIdx naming fix

- [#6008](https://github.com/leanprover/lean4/pull/6008) missing @[ext] attribute on monad transformer ext lemmas

- [#6023](https://github.com/leanprover/lean4/pull/6023) variants of List.forIn_eq_foldlM

- [#6025](https://github.com/leanprover/lean4/pull/6025) deprecate duplicated Fin.size_pos

- [#6032](https://github.com/leanprover/lean4/pull/6032) changes the signature of `Array.get` to take a Nat and a proof,
rather than a `Fin`, for consistency with the rest of the (planned)
Array API. Note that because of bootstrapping issues we can't provide
`get_elem_tactic` as an autoparameter for the proof. As users will
mostly use the `xs[i]` notation provided by `GetElem`, this hopefully
isn't a problem.

- [#6041](https://github.com/leanprover/lean4/pull/6041) modifies the order of arguments for higher-order `Array`
functions, preferring to put the `Array` last (besides positional
arguments with defaults). This is more consistent with the `List` API,
and is more flexible, as dot notation allows two different partially
applied versions.

- [#6049](https://github.com/leanprover/lean4/pull/6049) adds a primitive for accessing the current thread ID

- [#6052](https://github.com/leanprover/lean4/pull/6052) adds `Array.pmap`, as well as a `@[csimp]` lemma in terms of the
no-copy `Array.attachWith`.

- [#6055](https://github.com/leanprover/lean4/pull/6055) adds lemmas about for loops over `Array`, following the existing
lemmas for `List`.

- [#6056](https://github.com/leanprover/lean4/pull/6056) upstream some NameMap functions

- [#6060](https://github.com/leanprover/lean4/pull/6060) implements conversion functions from `Bool` to all `UIntX` and
`IntX` types.

- [#6070](https://github.com/leanprover/lean4/pull/6070) adds the Lean.RArray data structure.

- [#6074](https://github.com/leanprover/lean4/pull/6074) allow `Sort u` in `Squash`

- [#6094](https://github.com/leanprover/lean4/pull/6094) adds raw transmutation of floating-point numbers to and from
`UInt64`. Floats and UInts share the same endianness across all
supported platforms. The IEEE 754 standard precisely specifies the bit
layout of floats. Note that `Float.toBits` is distinct from
`Float.toUInt64`, which attempts to preserve the numeric value rather
than the bitwise value.

- [#6095](https://github.com/leanprover/lean4/pull/6095) generalize `List.get_mem`

- [#6097](https://github.com/leanprover/lean4/pull/6097) naming convention and `NaN` normalization

- [#6102](https://github.com/leanprover/lean4/pull/6102) moves `IO.rand` and `IO.setRandSeed` to be in the `BaseIO`
monad.

- [#6106](https://github.com/leanprover/lean4/pull/6106) fix naming of left/right injectivity lemmas

- [#6111](https://github.com/leanprover/lean4/pull/6111) fills in the API for `Array.findSome?` and `Array.find?`,
transferring proofs from the corresponding List statements.

- [#6120](https://github.com/leanprover/lean4/pull/6120) adds theorems `BitVec.(getMsbD, msb)_(rotateLeft, rotateRight)`.

- [#6126](https://github.com/leanprover/lean4/pull/6126) adds lemmas for extracting a given bit of a `BitVec` obtained
via `sub`/`neg`/`sshiftRight'`/`abs`.

- [#6130](https://github.com/leanprover/lean4/pull/6130) adds `Lean.loadPlugin` which exposes functionality similar to
the `lean` executable's `--plugin` option to Lean code.

- [#6132](https://github.com/leanprover/lean4/pull/6132) duplicates the verification API for
`List.attach`/`attachWith`/`pmap` over to `Array`.

- [#6133](https://github.com/leanprover/lean4/pull/6133) replaces `Array.feraseIdx` and `Array.insertAt` with
`Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat`
argument and a tactic-provided proof that it is in bounds. We also have
`eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the
index is out of bounds. We also provide a `Fin` valued version of
`Array.findIdx?`. Together, these quite ergonomically improve the array
indexing safety at a number of places in the compiler/elaborator.

- [#6136](https://github.com/leanprover/lean4/pull/6136) fixes the run-time evaluation of `(default : Float)`.

- [#6139](https://github.com/leanprover/lean4/pull/6139) modifies the signature of the functions `Nat.fold`,
`Nat.foldRev`, `Nat.any`, `Nat.all`, so that the function is passed the
upper bound. This allows us to change runtime array bounds checks to
compile time checks in many places.

- [#6148](https://github.com/leanprover/lean4/pull/6148) adds a primitive for creating temporary directories, akin to the
existing functionality for creating temporary files.

- [#6149](https://github.com/leanprover/lean4/pull/6149) completes the elementwise accessors for `ofNatLt`, `allOnes`,
and `not` by adding their implementations of `getMsbD`.

- [#6151](https://github.com/leanprover/lean4/pull/6151) completes the `toInt` interface for `BitVec` bitwise operations.

- [#6154](https://github.com/leanprover/lean4/pull/6154) implements `BitVec.toInt_abs`.

- [#6155](https://github.com/leanprover/lean4/pull/6155) adds `toNat` theorems for `BitVec.signExtend.`

- [#6157](https://github.com/leanprover/lean4/pull/6157) adds toInt theorems for BitVec.signExtend.

- [#6160](https://github.com/leanprover/lean4/pull/6160) adds theorem `mod_eq_sub`, makes theorem
`sub_mul_eq_mod_of_lt_of_le` not private anymore and moves its location
within the `rotate*` section to use it in other proofs.

- [#6184](https://github.com/leanprover/lean4/pull/6184) uses `Array.findFinIdx?` in preference to `Array.findIdx?` where
it allows converting a runtime bounds check to a compile time bounds
check.

- [#6188](https://github.com/leanprover/lean4/pull/6188) completes the `toNat` theorems for the bitwise operations
(`and`, `or`, `xor`, `shiftLeft`, `shiftRight`) of the UInt types and
adds `toBitVec` theorems as well. It also renames `and_toNat` to
`toNat_and` to fit with the current naming convention.

- [#6190](https://github.com/leanprover/lean4/pull/6190) adds the builtin simproc `USize.reduceToNat` which reduces the
`USize.toNat` operation on literals less than `UInt32.size` (i.e.,
`4294967296`).

- [#6191](https://github.com/leanprover/lean4/pull/6191) adds `Array.zipWithAll`, and the basic lemmas relating it to
`List.zipWithAll`.

- [#6192](https://github.com/leanprover/lean4/pull/6192) adds deprecations for `Lean.HashMap` functions which did not
receive deprecation attributes initially.

- [#6193](https://github.com/leanprover/lean4/pull/6193) completes the TODO in `Init.Data.Array.BinSearch`, removing the
`partial` keyword and converting runtime bounds checks to compile time
bounds checks.

- [#6194](https://github.com/leanprover/lean4/pull/6194) changes the signature of `Array.swap`, so it takes `Nat`
arguments with tactic provided bounds checking. It also renames
`Array.swap!` to `Array.swapIfInBounds`.

- [#6195](https://github.com/leanprover/lean4/pull/6195) renames `Array.setD` to `Array.setIfInBounds`.

- [#6197](https://github.com/leanprover/lean4/pull/6197) upstreams the definition of `Vector` from Batteries, along with
the basic functions.

- [#6200](https://github.com/leanprover/lean4/pull/6200) upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib
and uses them to prove the simp theorem `Nat.mod_two_pow`.

- [#6202](https://github.com/leanprover/lean4/pull/6202) makes `USize.toUInt64` a regular non-opaque definition.

- [#6203](https://github.com/leanprover/lean4/pull/6203) adds the theorems `le_usize_size` and `usize_size_le`, which
make proving inequalities about `USize.size` easier.

- [#6205](https://github.com/leanprover/lean4/pull/6205) upstreams some UInt theorems from Batteries and adds more
`toNat`-related theorems. It also adds the missing `UInt8` and `UInt16`
to/from `USize` conversions so that the the interface is uniform across
the UInt types.

- [#6207](https://github.com/leanprover/lean4/pull/6207) ensures the `Fin.foldl` and `Fin.foldr` are semireducible.
Without this the defeq `example (f : Fin 3 → ℕ) : List.ofFn f = [f 0, f
1, f 2] := rfl` was failing.

- [#6208](https://github.com/leanprover/lean4/pull/6208) fix Vector.indexOf?

- [#6217](https://github.com/leanprover/lean4/pull/6217) adds `simp` lemmas about `List`'s `==` operation.

- [#6221](https://github.com/leanprover/lean4/pull/6221) fixes:
- Problems in other linux distributions that the default `tzdata`
directory is not the same as previously defined by ensuring it with a
fallback behavior when directory is missing.
- Trim unnecessary characters from local time identifier.

- [#6222](https://github.com/leanprover/lean4/pull/6222) changes the definition of `HashSet.insertMany` and
`HashSet.Raw.insertMany` so that it is equivalent to repeatedly calling
`HashSet.insert`/`HashSet.Raw.insert`. It also clarifies the docstrings
of all the `insert` and `insertMany` functions.

- [#6230](https://github.com/leanprover/lean4/pull/6230) copies some lemmas about `List.foldX` to `Array`.

- [#6233](https://github.com/leanprover/lean4/pull/6233) upstreams lemmas about `Vector` from Batteries.

- [#6234](https://github.com/leanprover/lean4/pull/6234) upstreams the definition and basic lemmas about `List.finRange`
from Batteries.

- [#6235](https://github.com/leanprover/lean4/pull/6235) relates that operations `Nat.fold`/`foldRev`/`any`/`all` to the
corresponding List operations over `List.finRange`.

- [#6241](https://github.com/leanprover/lean4/pull/6241) refactors `Array.qsort` to remove runtime array bounds checks,
and avoids the use of `partial`. We use the `Vector` API, along with
auto_params, to avoid having to write any proofs. The new code
benchmarks indistinguishably from the old.

- [#6242](https://github.com/leanprover/lean4/pull/6242) deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an
`[NeZero]` instance, rather than returning an element of `Fin (n+1)`).

- [#6247](https://github.com/leanprover/lean4/pull/6247) adds the theorems `numBits_pos`, `le_numBits`, `numBits_le` ,
which make proving inequalities about `System.Platform.numBits` easier.

## Compiler

- [#5840](https://github.com/leanprover/lean4/pull/5840) changes `lean_sharecommon_{eq,hash}` to only consider the
salient bytes of an object, and not any bytes of any
unspecified/uninitialized unused capacity.

- [#6087](https://github.com/leanprover/lean4/pull/6087) fixes a bug in the constant folding for the `Nat.ble` and
`Nat.blt` function in the old code generator, leading to a
miscompilation.

- [#6143](https://github.com/leanprover/lean4/pull/6143) should make lean better-behaved around sanitizers, per
https://github.com/google/sanitizers/issues/1688.
As far as I can tell,
https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn#algorithm
replaces local variables with heap allocations, and so taking the
address of a local is not effective at producing a monotonic measure of
stack usage.

- [#6209](https://github.com/leanprover/lean4/pull/6209) documents under which conditions `Runtime.markPersistent` is
unsafe and adjusts the elaborator accordingly

- [#6257](https://github.com/leanprover/lean4/pull/6257) harden `markPersistent` uses

## Pretty Printing

- [#2934](https://github.com/leanprover/lean4/pull/2934) adds the option `pp.parens` (default: false) that causes the
pretty printer to eagerly insert parentheses, which can be useful for
teaching and for understanding the structure of expressions. For
example, it causes `p → q → r` to pretty print as `p → (q → r)`.

- [#6014](https://github.com/leanprover/lean4/pull/6014) prevents `Nat.succ ?_` from pretty printing as `?_.succ`, which
should make `apply?` be more usable.

- [#6085](https://github.com/leanprover/lean4/pull/6085) improves the term info for coercions marked with
`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to
definition" on the function name work. Hovering over such a coerced
function will show the coercee rather than the coercion expression. The
coercion expression can still be seen by hovering over the whitespace in
the function application.

- [#6096](https://github.com/leanprover/lean4/pull/6096) improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.

- [#6119](https://github.com/leanprover/lean4/pull/6119) adds a new delab option `pp.coercions.types` which, when
enabled, will display all coercions with an explicit type ascription.

- [#6161](https://github.com/leanprover/lean4/pull/6161) ensures whitespace is printed before `+opt` and `-opt`
configuration options when pretty printing, improving the experience of
tactics such as `simp?`.

- [#6181](https://github.com/leanprover/lean4/pull/6181) fixes a bug where the signature pretty printer would ignore the
current setting of `pp.raw`. This fixes an issue where `#check ident`
would not heed `pp.raw`. Closes #6090.

- [#6213](https://github.com/leanprover/lean4/pull/6213) exposes the difference in "synthesized type class instance is
not definitionally equal" errors.

## Documentation

- [#6009](https://github.com/leanprover/lean4/pull/6009) fixes a typo in the docstring for prec and makes the text
slightly more precise.

- [#6040](https://github.com/leanprover/lean4/pull/6040) join → flatten in docstring

- [#6110](https://github.com/leanprover/lean4/pull/6110) does some mild refactoring of the `Lean.Elab.StructInst` module
while adding documentation.

- [#6144](https://github.com/leanprover/lean4/pull/6144) converts 3 doc-string to module docs since it seems that this is
what they were intended to be!

- [#6150](https://github.com/leanprover/lean4/pull/6150) refine kernel code comments

- [#6158](https://github.com/leanprover/lean4/pull/6158) adjust file reference in Data.Sum

- [#6239](https://github.com/leanprover/lean4/pull/6239) explains the order in which `Expr.abstract` introduces de Bruijn
indices.

## Server

- [#5835](https://github.com/leanprover/lean4/pull/5835) adds auto-completion for the fields of structure instance notation. Specifically, querying the completions via `Ctrl+Space` in the whitespace of a structure instance notation will now bring up the full list of fields. Whitespace structure completion can be enabled for custom syntax by wrapping the parser for the list of fields in a `structInstFields` parser.

- [#5837](https://github.com/leanprover/lean4/pull/5837) fixes an old auto-completion bug where `x.` would issue
nonsensical completions when `x.` could not be elaborated as a dot
completion.

- [#5996](https://github.com/leanprover/lean4/pull/5996) avoid max heartbeat error in completion

- [#6031](https://github.com/leanprover/lean4/pull/6031) fixes a regression with go-to-definition and document highlight
misbehaving on tactic blocks.

- [#6246](https://github.com/leanprover/lean4/pull/6246) fixes a performance issue where the Lean language server would
walk the full project file tree every time a file was saved, blocking
the processing of all other requests and notifications and significantly
increasing overall language server latency after saving.

## Lake

- [#5684](https://github.com/leanprover/lean4/pull/5684) update toolchain on `lake update`

- [#6026](https://github.com/leanprover/lean4/pull/6026) adds a newline at end of each Lean file generated by `lake new`
templates.

- [#6218](https://github.com/leanprover/lean4/pull/6218) makes Lake no longer automatically fetch GitHub cloud releases
if the package build directory is already present (mirroring the
behavior of the Reservoir cache). This prevents the cache from
clobbering existing prebuilt artifacts. Users can still manually fetch
the cache and clobber the build directory by running `lake build
<pkg>:release`.

- [#6225](https://github.com/leanprover/lean4/pull/6225) makes `lake build` also eagerly print package materialization
log lines. Previously, only a `lake update` performed eager logging.

- [#6231](https://github.com/leanprover/lean4/pull/6231) improves the errors Lake produces when it fails to fetch a
dependency from Reservoir. If the package is not indexed, it will
produce a suggestion about how to require it from GitHub.

## Other

- [#6137](https://github.com/leanprover/lean4/pull/6137) adds support for displaying multiple threads in the trace
profiler output.

- [#6138](https://github.com/leanprover/lean4/pull/6138) fixes `trace.profiler.pp` not using the term pretty printer.

- [#6259](https://github.com/leanprover/lean4/pull/6259) ensures that nesting trace nodes are annotated with timing
information iff `trace.profiler` is active.

v4.14.0
----------

**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.13.0...v4.14.0

### Language features, tactics, and metaprograms

* `structure` and `inductive` commands
  * [#5517](https://github.com/leanprover/lean4/pull/5517) improves universe level inference for the resulting type of an `inductive` or `structure.` Recall that a `Prop`-valued inductive type is a syntactic subsingleton if it has at most one constructor and all the arguments to the constructor are in `Prop`. Such types have large elimination, so they could be defined in `Type` or `Prop` without any trouble. The way inference has changed is that if a type is a syntactic subsingleton with exactly one constructor, and the constructor has at least one parameter/field, then the `inductive`/`structure` command will prefer creating a `Prop` instead of a `Type`. The upshot is that the `: Prop` in `structure S : Prop` is often no longer needed. (With @arthur-adjedj).
  * [#5842](https://github.com/leanprover/lean4/pull/5842) and [#5783](https://github.com/leanprover/lean4/pull/5783) implement a feature where the `structure` command can now define recursive inductive types:
    ```lean
    structure Tree where
      n : Nat
      children : Fin n → Tree

    def Tree.size : Tree → Nat
      | {n, children} => Id.run do
        let mut s := 0
        for h : i in [0 : n] do
          s := s + (children ⟨i, h.2⟩).size
        pure s
    ```
  * [#5814](https://github.com/leanprover/lean4/pull/5814) fixes a bug where Mathlib's `Type*` elaborator could lead to incorrect universe parameters with the `inductive` command.
  * [#3152](https://github.com/leanprover/lean4/pull/3152) and [#5844](https://github.com/leanprover/lean4/pull/5844) fix bugs in default value processing for structure instance notation (with @arthur-adjedj).
  * [#5399](https://github.com/leanprover/lean4/pull/5399) promotes instance synthesis order calculation failure from a soft error to a hard error.
  * [#5542](https://github.com/leanprover/lean4/pull/5542) deprecates `:=` variants of `inductive` and `structure` (see breaking changes).

* **Application elaboration improvements**
  * [#5671](https://github.com/leanprover/lean4/pull/5671) makes `@[elab_as_elim]` require at least one discriminant, since otherwise there is no advantage to this alternative elaborator.
  * [#5528](https://github.com/leanprover/lean4/pull/5528) enables field notation in explicit mode. The syntax `@x.f` elaborates as `@S.f` with `x` supplied to the appropriate parameter.
  * [#5692](https://github.com/leanprover/lean4/pull/5692) modifies the dot notation resolution algorithm so that it can apply `CoeFun` instances. For example, Mathlib has `Multiset.card : Multiset α →+ Nat`, and now with `m : Multiset α`, the notation `m.card` resolves to `⇑Multiset.card m`.
  * [#5658](https://github.com/leanprover/lean4/pull/5658) fixes a bug where 'don't know how to synthesize implicit argument' errors might have the incorrect local context when the eta arguments feature is activated.
  * [#5933](https://github.com/leanprover/lean4/pull/5933) fixes a bug where `..` ellipses in patterns made use of optparams and autoparams.
  * [#5770](https://github.com/leanprover/lean4/pull/5770) makes dot notation for structures resolve using *all* ancestors. Adds a *resolution order* for generalized field notation. This is the order of namespaces visited during resolution when trying to resolve names. The algorithm to compute a resolution order is the commonly used C3 linearization (used for example by Python), which when successful ensures that immediate parents' namespaces are considered before more distant ancestors' namespaces. By default we use a relaxed version of the algorithm that tolerates inconsistencies, but using `set_option structure.strictResolutionOrder true` makes inconsistent parent orderings into warnings.

* **Recursion and induction principles**
  * [#5619](https://github.com/leanprover/lean4/pull/5619) fixes functional induction principle generation to avoid over-eta-expanding in the preprocessing step.
  * [#5766](https://github.com/leanprover/lean4/pull/5766) fixes structural nested recursion so that it is not confused when a nested type appears first.
  * [#5803](https://github.com/leanprover/lean4/pull/5803) fixes a bug in functional induction principle generation when there are `let` bindings.
  * [#5904](https://github.com/leanprover/lean4/pull/5904) improves functional induction principle generation to unfold aux definitions more carefully.
  * [#5850](https://github.com/leanprover/lean4/pull/5850) refactors code for `Predefinition.Structural`.

* **Error messages**
  * [#5276](https://github.com/leanprover/lean4/pull/5276) fixes a bug in "type mismatch" errors that would structurally assign metavariables during the algorithm to expose differences.
  * [#5919](https://github.com/leanprover/lean4/pull/5919) makes "type mismatch" errors add type ascriptions to expose differences for numeric literals.
  * [#5922](https://github.com/leanprover/lean4/pull/5922) makes "type mismatch" errors expose differences in the bodies of functions and pi types.
  * [#5888](https://github.com/leanprover/lean4/pull/5888) improves the error message for invalid induction alternative names in `match` expressions (@josojo).
  * [#5719](https://github.com/leanprover/lean4/pull/5719) improves `calc` error messages.

* [#5627](https://github.com/leanprover/lean4/pull/5627) and [#5663](https://github.com/leanprover/lean4/pull/5663) improve the **`#eval` command** and introduce some new features.
  * Now results can be pretty printed if there is a `ToExpr` instance, which means **hoverable output**. If `ToExpr` fails, it then tries looking for a `Repr` or `ToString` instance like before. Setting `set_option eval.pp false` disables making use of `ToExpr` instances.
  * There is now **auto-derivation** of `Repr` instances, enabled with the `pp.derive.repr` option (default to **true**). For example:
    ```lean
    inductive Baz
    | a | b

    #eval Baz.a
    -- Baz.a
    ```
    It simply does `deriving instance Repr for Baz` when there's no way to represent `Baz`.
  * The option `eval.type` controls whether or not to include the type in the output. For now the default is false.
  * Now expressions such as `#eval do return 2`, where monad is unknown, work. It tries unifying the monad with `CommandElabM`, `TermElabM`, or `IO`.
  * The classes `Lean.Eval` and `Lean.MetaEval` have been removed. These each used to be responsible for adapting monads and printing results. Now the `MonadEval` class is responsible for adapting monads for evaluation (it is similar to `MonadLift`, but instances are allowed to use default data when initializing state), and representing results is handled through a separate process.
  * Error messages about failed instance synthesis are now more precise. Once it detects that a `MonadEval` class applies, then the error message will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
  * Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log messages.
  * Fixes a bug where `let rec` could not be used in `#eval`.

* `partial` definitions
  * [#5780](https://github.com/leanprover/lean4/pull/5780) improves the error message when `partial` fails to prove a type is inhabited. Add delta deriving.
  * [#5821](https://github.com/leanprover/lean4/pull/5821) gives `partial` inhabitation the ability to create local `Inhabited` instances from parameters.

* **New tactic configuration syntax.** The configuration syntax for all core tactics has been given an upgrade. Rather than `simp (config := { contextual := true, maxSteps := 22})`, one can now write `simp +contextual (maxSteps := 22)`. Tactic authors can migrate by switching from `(config)?` to `optConfig` in tactic syntaxes and potentially deleting `mkOptionalNode` in elaborators. [#5883](https://github.com/leanprover/lean4/pull/5883), [#5898](https://github.com/leanprover/lean4/pull/5898),  [#5928](https://github.com/leanprover/lean4/pull/5928), and [#5932](https://github.com/leanprover/lean4/pull/5932). (Tactic authors, see breaking changes.)

* `simp` tactic
  * [#5632](https://github.com/leanprover/lean4/pull/5632) fixes the simpproc for `Fin` literals to reduce more consistently.
  * [#5648](https://github.com/leanprover/lean4/pull/5648) fixes a bug in `simpa ... using t` where metavariables in `t` were not properly accounted for, and also improves the type mismatch error.
  * [#5838](https://github.com/leanprover/lean4/pull/5838) fixes the docstring of `simp!` to actually talk about `simp!`.
  * [#5870](https://github.com/leanprover/lean4/pull/5870) adds support for `attribute [simp ←]` (note the reverse direction). This adds the reverse of a theorem as a global simp theorem.

* `decide` tactic
  * [#5665](https://github.com/leanprover/lean4/pull/5665) adds `decide!` tactic for using kernel reduction (warning: this is renamed to `decide +kernel` in a future release).

* `bv_decide` tactic
  * [#5714](https://github.com/leanprover/lean4/pull/5714) adds inequality regression tests (@alexkeizer).
  * [#5608](https://github.com/leanprover/lean4/pull/5608) adds `bv_toNat` tag for `toNat_ofInt` (@bollu).
  * [#5618](https://github.com/leanprover/lean4/pull/5618) adds support for `at` in `ac_nf` and uses it in `bv_normalize` (@tobiasgrosser).
  * [#5628](https://github.com/leanprover/lean4/pull/5628) adds udiv support.
  * [#5635](https://github.com/leanprover/lean4/pull/5635) adds auxiliary bitblasters for negation and subtraction.
  * [#5637](https://github.com/leanprover/lean4/pull/5637) adds more `getLsbD` bitblaster theory.
  * [#5652](https://github.com/leanprover/lean4/pull/5652) adds umod support.
  * [#5653](https://github.com/leanprover/lean4/pull/5653) adds performance benchmark for modulo.
  * [#5655](https://github.com/leanprover/lean4/pull/5655) reduces error on `bv_check` to warning.
  * [#5670](https://github.com/leanprover/lean4/pull/5670) adds `~~~(-x)` support.
  * [#5673](https://github.com/leanprover/lean4/pull/5673) disables `ac_nf` by default.
  * [#5675](https://github.com/leanprover/lean4/pull/5675) fixes context tracking in `bv_decide` counter example.
  * [#5676](https://github.com/leanprover/lean4/pull/5676) adds an error when the LRAT proof is invalid.
  * [#5781](https://github.com/leanprover/lean4/pull/5781) introduces uninterpreted symbols everywhere.
  * [#5823](https://github.com/leanprover/lean4/pull/5823) adds `BitVec.sdiv` support.
  * [#5852](https://github.com/leanprover/lean4/pull/5852) adds `BitVec.ofBool` support.
  * [#5855](https://github.com/leanprover/lean4/pull/5855) adds `if` support.
  * [#5869](https://github.com/leanprover/lean4/pull/5869) adds support for all the SMTLIB BitVec divison/remainder operations.
  * [#5886](https://github.com/leanprover/lean4/pull/5886) adds embedded constraint substitution.
  * [#5918](https://github.com/leanprover/lean4/pull/5918) fixes loose mvars bug in `bv_normalize`.
  * Documentation:
    * [#5636](https://github.com/leanprover/lean4/pull/5636) adds remarks about multiplication.

* `conv` mode
  * [#5861](https://github.com/leanprover/lean4/pull/5861) improves the `congr` conv tactic to handle "over-applied" functions.
  * [#5894](https://github.com/leanprover/lean4/pull/5894) improves the `arg` conv tactic so that it can access more arguments and so that it can handle "over-applied" functions (it generates a specialized congruence lemma for the specific argument in question). Makes `arg 1` and `arg 2` apply to pi types in more situations. Adds negative indexing, for example `arg -2` is equivalent to the `lhs` tactic. Makes the `enter [...]` tactic show intermediate states like `rw`.

* **Other tactics**
  * [#4846](https://github.com/leanprover/lean4/pull/4846) fixes a bug where `generalize ... at *` would apply to implementation details (@ymherklotz).
  * [#5730](https://github.com/leanprover/lean4/pull/5730) upstreams the `classical` tactic combinator.
  * [#5815](https://github.com/leanprover/lean4/pull/5815) improves the error message when trying to unfold a local hypothesis that is not a local definition.
  * [#5862](https://github.com/leanprover/lean4/pull/5862) and [#5863](https://github.com/leanprover/lean4/pull/5863) change how `apply` and `simp` elaborate, making them not disable error recovery. This improves hovers and completions when the term has elaboration errors.

* `deriving` clauses
  * [#5899](https://github.com/leanprover/lean4/pull/5899) adds declaration ranges for delta-derived instances.
  * [#5265](https://github.com/leanprover/lean4/pull/5265) removes unused syntax in `deriving` clauses for providing arguments to deriving handlers (see breaking changes).

* [#5065](https://github.com/leanprover/lean4/pull/5065) upstreams and updates `#where`, a command that reports the current scope information.

* **Linters**
  * [#5338](https://github.com/leanprover/lean4/pull/5338) makes the unused variables linter ignore variables defined in tactics by default now, avoiding performance bottlenecks.
  * [#5644](https://github.com/leanprover/lean4/pull/5644) ensures that linters in general do not run on `#guard_msgs` itself.

* **Metaprogramming interface**
  * [#5720](https://github.com/leanprover/lean4/pull/5720) adds `pushGoal`/`pushGoals` and `popGoal` for manipulating the goal state. These are an alternative to `replaceMainGoal` and `getMainGoal`, and with them you don't need to worry about making sure nothing clears assigned metavariables from the goal list between assigning the main goal and using `replaceMainGoal`. Modifies `closeMainGoalUsing`, which is like a `TacticM` version of `liftMetaTactic`. Now the callback is run in a context where the main goal is removed from the goal list, and the callback is free to modify the goal list. Furthermore, the `checkUnassigned` argument has been replaced with `checkNewUnassigned`, which checks whether the value assigned to the goal has any *new* metavariables, relative to the start of execution of the callback. Modifies `withCollectingNewGoalsFrom` to take the `parentTag` argument explicitly rather than indirectly via `getMainTag`. Modifies `elabTermWithHoles` to optionally take `parentTag?`.
  * [#5563](https://github.com/leanprover/lean4/pull/5563) fixes `getFunInfo` and `inferType` to use `withAtLeastTransparency` rather than `withTransparency`.
  * [#5679](https://github.com/leanprover/lean4/pull/5679) fixes `RecursorVal.getInduct` to return the name of major argument’s type. This makes "structure eta" work for nested inductives.
  * [#5681](https://github.com/leanprover/lean4/pull/5681) removes unused `mkRecursorInfoForKernelRec`.
  * [#5686](https://github.com/leanprover/lean4/pull/5686) makes discrimination trees index the domains of foralls, for better performance of the simplify and type class search.
  * [#5760](https://github.com/leanprover/lean4/pull/5760) adds `Lean.Expr.name?` recognizer for `Name` expressions.
  * [#5800](https://github.com/leanprover/lean4/pull/5800) modifies `liftCommandElabM` to preserve more state, fixing an issue where using it would drop messages.
  * [#5857](https://github.com/leanprover/lean4/pull/5857) makes it possible to use dot notation in `m!` strings, for example `m!"{.ofConstName n}"`.
  * [#5841](https://github.com/leanprover/lean4/pull/5841) and [#5853](https://github.com/leanprover/lean4/pull/5853) record the complete list of `structure` parents in the `StructureInfo` environment extension.

* **Other fixes or improvements**
  * [#5566](https://github.com/leanprover/lean4/pull/5566) fixes a bug introduced in [#4781](https://github.com/leanprover/lean4/pull/4781) where heartbeat exceptions were no longer being handled properly. Now such exceptions are tagged with `runtime.maxHeartbeats` (@eric-wieser).
  * [#5708](https://github.com/leanprover/lean4/pull/5708) modifies the proof objects produced by the proof-by-reflection tactics `ac_nf0` and `simp_arith` so that the kernel is less prone to reducing expensive atoms.
  * [#5768](https://github.com/leanprover/lean4/pull/5768) adds a `#version` command that prints Lean's version information.
  * [#5822](https://github.com/leanprover/lean4/pull/5822) fixes elaborator algorithms to match kernel algorithms for primitive projections (`Expr.proj`).
  * [#5811](https://github.com/leanprover/lean4/pull/5811) improves the docstring for the `rwa` tactic.


### Language server, widgets, and IDE extensions

* [#5224](https://github.com/leanprover/lean4/pull/5224) fixes `WorkspaceClientCapabilities` to make `applyEdit` optional, in accordance with the LSP specification (@pzread).
* [#5340](https://github.com/leanprover/lean4/pull/5340) fixes a server deadlock when shutting down the language server and a desync between client and language server after a file worker crash.
* [#5560](https://github.com/leanprover/lean4/pull/5560) makes `initialize` and `builtin_initialize` participate in the call hierarchy and other requests.
* [#5650](https://github.com/leanprover/lean4/pull/5650) makes references in attributes participate in the call hierarchy and other requests.
* [#5666](https://github.com/leanprover/lean4/pull/5666) add auto-completion in tactic blocks without having to type the first character of the tactic, and adds tactic completion docs to tactic auto-completion items.
* [#5677](https://github.com/leanprover/lean4/pull/5677) fixes several cases where goal states were not displayed in certain text cursor positions.
* [#5707](https://github.com/leanprover/lean4/pull/5707) indicates deprecations in auto-completion items.
* [#5736](https://github.com/leanprover/lean4/pull/5736), [#5752](https://github.com/leanprover/lean4/pull/5752), [#5763](https://github.com/leanprover/lean4/pull/5763), [#5802](https://github.com/leanprover/lean4/pull/5802), and [#5805](https://github.com/leanprover/lean4/pull/5805) fix various performance issues in the language server.
* [#5801](https://github.com/leanprover/lean4/pull/5801) distinguishes theorem auto-completions from non-theorem auto-completions.

### Pretty printing

* [#5640](https://github.com/leanprover/lean4/pull/5640) fixes a bug where goal states in messages might print newlines as spaces.
* [#5643](https://github.com/leanprover/lean4/pull/5643) adds option `pp.mvars.delayed` (default false), which when false causes delayed assignment metavariables to pretty print with what they are assigned to. Now `fun x : Nat => ?a` pretty prints as `fun x : Nat => ?a` rather than `fun x ↦ ?m.7 x`.
* [#5711](https://github.com/leanprover/lean4/pull/5711) adds options `pp.mvars.anonymous` and `pp.mvars.levels`, which when false respectively cause expression metavariables and level metavariables to pretty print as `?_`.
* [#5710](https://github.com/leanprover/lean4/pull/5710) adjusts the `⋯` elaboration warning to mention `pp.maxSteps`.

* [#5759](https://github.com/leanprover/lean4/pull/5759) fixes the app unexpander for `sorryAx`.
* [#5827](https://github.com/leanprover/lean4/pull/5827) improves accuracy of binder names in the signature pretty printer (like in output of `#check`). Also fixes the issue where consecutive hygienic names pretty print without a space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝ : Nat)`.
* [#5830](https://github.com/leanprover/lean4/pull/5830) makes sure all the core delaborators respond to `pp.explicit` when appropriate.
* [#5639](https://github.com/leanprover/lean4/pull/5639) makes sure name literals use escaping when pretty printing.
* [#5854](https://github.com/leanprover/lean4/pull/5854) adds delaborators for `<|>`, `<*>`, `>>`, `<*`, and `*>`.

### Library

* `Array`
  * [#5687](https://github.com/leanprover/lean4/pull/5687) deprecates `Array.data`.
  * [#5705](https://github.com/leanprover/lean4/pull/5705) uses a better default value for `Array.swapAt!`.
  * [#5748](https://github.com/leanprover/lean4/pull/5748) moves `Array.mapIdx` lemmas to a new file.
  * [#5749](https://github.com/leanprover/lean4/pull/5749) simplifies signature of `Array.mapIdx`.
  * [#5758](https://github.com/leanprover/lean4/pull/5758) upstreams `Array.reduceOption`.
  * [#5786](https://github.com/leanprover/lean4/pull/5786) adds simp lemmas for `Array.isEqv` and `BEq`.
  * [#5796](https://github.com/leanprover/lean4/pull/5796) renames `Array.shrink` to `Array.take`, and relates it to `List.take`.
  * [#5798](https://github.com/leanprover/lean4/pull/5798) upstreams `List.modify`, adds lemmas, relates to `Array.modify`.
  * [#5799](https://github.com/leanprover/lean4/pull/5799) relates `Array.forIn` and `List.forIn`.
  * [#5833](https://github.com/leanprover/lean4/pull/5833) adds `Array.forIn'`, and relates to `List`.
  * [#5848](https://github.com/leanprover/lean4/pull/5848) fixes deprecations in `Init.Data.Array.Basic` to not recommend the deprecated constant.
  * [#5895](https://github.com/leanprover/lean4/pull/5895) adds `LawfulBEq (Array α) ↔ LawfulBEq α`.
  * [#5896](https://github.com/leanprover/lean4/pull/5896) moves `@[simp]` from `back_eq_back?` to `back_push`.
  * [#5897](https://github.com/leanprover/lean4/pull/5897) renames `Array.back` to `back!`.

* `List`
  * [#5605](https://github.com/leanprover/lean4/pull/5605) removes `List.redLength`.
  * [#5696](https://github.com/leanprover/lean4/pull/5696) upstreams `List.mapIdx` and adds lemmas.
  * [#5697](https://github.com/leanprover/lean4/pull/5697) upstreams `List.foldxM_map`.
  * [#5701](https://github.com/leanprover/lean4/pull/5701) renames `List.join` to `List.flatten`.
  * [#5703](https://github.com/leanprover/lean4/pull/5703) upstreams `List.sum`.
  * [#5706](https://github.com/leanprover/lean4/pull/5706) marks `prefix_append_right_inj` as a simp lemma.
  * [#5716](https://github.com/leanprover/lean4/pull/5716) fixes `List.drop_drop` addition order.
  * [#5731](https://github.com/leanprover/lean4/pull/5731) renames `List.bind` and `Array.concatMap` to `flatMap`.
  * [#5732](https://github.com/leanprover/lean4/pull/5732) renames `List.pure` to `List.singleton`.
  * [#5742](https://github.com/leanprover/lean4/pull/5742) upstreams `ne_of_mem_of_not_mem`.
  * [#5743](https://github.com/leanprover/lean4/pull/5743) upstreams `ne_of_apply_ne`.
  * [#5816](https://github.com/leanprover/lean4/pull/5816) adds more `List.modify` lemmas.
  * [#5879](https://github.com/leanprover/lean4/pull/5879) renames `List.groupBy` to `splitBy`.
  * [#5913](https://github.com/leanprover/lean4/pull/5913) relates `for` loops over `List` with `foldlM`.

* `Nat`
  * [#5694](https://github.com/leanprover/lean4/pull/5694) removes `instBEqNat`, which is redundant with `instBEqOfDecidableEq` but not defeq.
  * [#5746](https://github.com/leanprover/lean4/pull/5746) deprecates `Nat.sum`.
  * [#5785](https://github.com/leanprover/lean4/pull/5785) adds `Nat.forall_lt_succ` and variants.

* Fixed width integers
  * [#5323](https://github.com/leanprover/lean4/pull/5323) redefine unsigned fixed width integers in terms of `BitVec`.
  * [#5735](https://github.com/leanprover/lean4/pull/5735) adds `UIntX.[val_ofNat, toBitVec_ofNat]`.
  * [#5790](https://github.com/leanprover/lean4/pull/5790) defines `Int8`.
  * [#5901](https://github.com/leanprover/lean4/pull/5901) removes native code for `UInt8.modn`.

* `BitVec`
  * [#5604](https://github.com/leanprover/lean4/pull/5604) completes `BitVec.[getMsbD|getLsbD|msb]` for shifts (@luisacicolini).
  * [#5609](https://github.com/leanprover/lean4/pull/5609) adds lemmas for division when denominator is zero (@bollu).
  * [#5620](https://github.com/leanprover/lean4/pull/5620) documents Bitblasting (@bollu)
  * [#5623](https://github.com/leanprover/lean4/pull/5623) moves `BitVec.udiv/umod/sdiv/smod` after `add/sub/mul/lt` (@tobiasgrosser).
  * [#5645](https://github.com/leanprover/lean4/pull/5645) defines `udiv` normal form to be `/`, resp. `umod` and `%` (@bollu).
  * [#5646](https://github.com/leanprover/lean4/pull/5646) adds lemmas about arithmetic inequalities (@bollu).
  * [#5680](https://github.com/leanprover/lean4/pull/5680) expands relationship with `toFin` (@tobiasgrosser).
  * [#5691](https://github.com/leanprover/lean4/pull/5691) adds `BitVec.(getMSbD, msb)_(add, sub)` and `BitVec.getLsbD_sub` (@luisacicolini).
  * [#5712](https://github.com/leanprover/lean4/pull/5712) adds `BitVec.[udiv|umod]_[zero|one|self]` (@tobiasgrosser).
  * [#5718](https://github.com/leanprover/lean4/pull/5718) adds `BitVec.sdiv_[zero|one|self]` (@tobiasgrosser).
  * [#5721](https://github.com/leanprover/lean4/pull/5721) adds `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` (@luisacicolini).
  * [#5772](https://github.com/leanprover/lean4/pull/5772) adds `BitVec.toInt_sub`, simplifies `BitVec.toInt_neg` (@tobiasgrosser).
  * [#5778](https://github.com/leanprover/lean4/pull/5778) prove that `intMin` the smallest signed bitvector (@alexkeizer).
  * [#5851](https://github.com/leanprover/lean4/pull/5851) adds `(msb, getMsbD)_twoPow` (@luisacicolini).
  * [#5858](https://github.com/leanprover/lean4/pull/5858) adds `BitVec.[zero_ushiftRight|zero_sshiftRight|zero_mul]` and cleans up BVDecide (@tobiasgrosser).
  * [#5865](https://github.com/leanprover/lean4/pull/5865) adds `BitVec.(msb, getMsbD)_concat` (@luisacicolini).
  * [#5881](https://github.com/leanprover/lean4/pull/5881) adds `Hashable (BitVec n)`

* `String`/`Char`
  * [#5728](https://github.com/leanprover/lean4/pull/5728) upstreams `String.dropPrefix?`.
  * [#5745](https://github.com/leanprover/lean4/pull/5745) changes `String.dropPrefix?` signature.
  * [#5747](https://github.com/leanprover/lean4/pull/5747) adds `Hashable Char` instance

* `HashMap`
  * [#5880](https://github.com/leanprover/lean4/pull/5880) adds interim implementation of `HashMap.modify`/`alter`

* **Other**
  * [#5704](https://github.com/leanprover/lean4/pull/5704) removes `@[simp]` from `Option.isSome_eq_isSome`.
  * [#5739](https://github.com/leanprover/lean4/pull/5739) upstreams material on `Prod`.
  * [#5740](https://github.com/leanprover/lean4/pull/5740) moves `Antisymm` to `Std.Antisymm`.
  * [#5741](https://github.com/leanprover/lean4/pull/5741) upstreams basic material on `Sum`.
  * [#5756](https://github.com/leanprover/lean4/pull/5756) adds `Nat.log2_two_pow` (@spinylobster).
  * [#5892](https://github.com/leanprover/lean4/pull/5892) removes duplicated `ForIn` instances.
  * [#5900](https://github.com/leanprover/lean4/pull/5900) removes `@[simp]` from `Sum.forall` and `Sum.exists`.
  * [#5812](https://github.com/leanprover/lean4/pull/5812) removes redundant `Decidable` assumptions (@FR-vdash-bot).

### Compiler, runtime, and FFI

* [#5685](https://github.com/leanprover/lean4/pull/5685) fixes help message flags, removes the `-f` flag and adds the `-g` flag (@James-Oswald).
* [#5930](https://github.com/leanprover/lean4/pull/5930) adds `--short-version` (`-V`) option to display short version (@juhp).
* [#5144](https://github.com/leanprover/lean4/pull/5144) switches all 64-bit platforms over to consistently using GMP for bignum arithmetic.
* [#5753](https://github.com/leanprover/lean4/pull/5753) raises the minimum supported Windows version to Windows 10 1903 (released May 2019).

### Lake

* [#5715](https://github.com/leanprover/lean4/pull/5715) changes `lake new math` to use `autoImplicit false` (@eric-wieser).
* [#5688](https://github.com/leanprover/lean4/pull/5688) makes `Lake` not create core aliases in the `Lake` namespace.
* [#5924](https://github.com/leanprover/lean4/pull/5924) adds a `text` option for `buildFile*` utilities.
* [#5789](https://github.com/leanprover/lean4/pull/5789) makes `lake init` not `git init` when inside git work tree (@haoxins).
* [#5684](https://github.com/leanprover/lean4/pull/5684) has Lake update a package's `lean-toolchain` file on `lake update` if it finds the package's direct dependencies use a newer compatible toolchain. To skip this step, use the `--keep-toolchain` CLI option. (See breaking changes.)
* [#6218](https://github.com/leanprover/lean4/pull/6218) makes Lake no longer automatically fetch GitHub cloud releases if the package build directory is already present (mirroring the behavior of the Reservoir cache). This prevents the cache from clobbering existing prebuilt artifacts. Users can still manually fetch the cache and clobber the build directory by running `lake build <pkg>:release`.
* [#6231](https://github.com/leanprover/lean4/pull/6231) improves the errors Lake produces when it fails to fetch a dependency from Reservoir. If the package is not indexed, it will produce a suggestion about how to require it from GitHub.

### Documentation

* [#5617](https://github.com/leanprover/lean4/pull/5617) fixes MSYS2 build instructions.
* [#5725](https://github.com/leanprover/lean4/pull/5725) points out that `OfScientific` is called with raw literals (@eric-wieser).
* [#5794](https://github.com/leanprover/lean4/pull/5794) adds a stub for application ellipsis notation (@eric-wieser).

### Breaking changes

* The syntax for providing arguments to deriving handlers has been removed, which was not used by any major Lean projects in the ecosystem. As a result, the  `applyDerivingHandlers` now takes one fewer argument, `registerDerivingHandlerWithArgs` is now simply `registerDerivingHandler`, `DerivingHandler` no longer includes the unused parameter, and `DerivingHandlerNoArgs` has been deprecated. To migrate code, delete the unused `none` argument and use `registerDerivingHandler` and `DerivingHandler`. ([#5265](https://github.com/leanprover/lean4/pull/5265))
* The minimum supported Windows version has been raised to Windows 10 1903, released May 2019. ([#5753](https://github.com/leanprover/lean4/pull/5753))
* The `--lean` CLI option for `lake` was removed. Use the `LEAN` environment variable instead. ([#5684](https://github.com/leanprover/lean4/pull/5684))
* The `inductive ... :=`, `structure ... :=`, and `class ... :=` syntaxes have been deprecated in favor of the `... where` variants. The old syntax produces a warning, controlled by the `linter.deprecated` option. ([#5542](https://github.com/leanprover/lean4/pull/5542))
* The generated tactic configuration elaborators now land in `TacticM` to make use of the current recovery state. Commands that wish to elaborate configurations should now use `declare_command_config_elab` instead of `declare_config_elab` to get an elaborator landing in `CommandElabM`. Syntaxes should migrate to `optConfig` instead of `(config)?`, but the elaborators are reverse compatible. ([#5883](https://github.com/leanprover/lean4/pull/5883))


v4.13.0
----------

**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.12.0...v4.13.0

### Language features, tactics, and metaprograms

* `structure` command
  * [#5511](https://github.com/leanprover/lean4/pull/5511) allows structure parents to be type synonyms.
  * [#5531](https://github.com/leanprover/lean4/pull/5531) allows default values for structure fields to be noncomputable.

* `rfl` and `apply_rfl` tactics
  * [#3714](https://github.com/leanprover/lean4/pull/3714), [#3718](https://github.com/leanprover/lean4/pull/3718) improve the `rfl` tactic and give better error messages.
  * [#3772](https://github.com/leanprover/lean4/pull/3772) makes `rfl` no longer use kernel defeq for ground terms.
  * [#5329](https://github.com/leanprover/lean4/pull/5329) tags `Iff.refl` with `@[refl]` (@Parcly-Taxel)
  * [#5359](https://github.com/leanprover/lean4/pull/5359) ensures that the `rfl` tactic tries `Iff.rfl` (@Parcly-Taxel)

* `unfold` tactic
  * [#4834](https://github.com/leanprover/lean4/pull/4834) let `unfold` do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib `unfold_let` tactic.

* `omega` tactic
  * [#5382](https://github.com/leanprover/lean4/pull/5382) fixes spurious error in [#5315](https://github.com/leanprover/lean4/issues/5315)
  * [#5523](https://github.com/leanprover/lean4/pull/5523) supports `Int.toNat`

* `simp` tactic
  * [#5479](https://github.com/leanprover/lean4/pull/5479) lets `simp` apply rules with higher-order patterns.

* `induction` tactic
  * [#5494](https://github.com/leanprover/lean4/pull/5494) fixes `induction`’s "pre-tactic" block to always be indented, avoiding unintended uses of it.

* `ac_nf` tactic
  * [#5524](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/5211) makes `extractLsb'` the primitive `bv_decide` understands, rather than `extractLsb` (@alexkeizer)
  * [#5365](https://github.com/leanprover/lean4/pull/5365) adds `bv_decide` diagnoses.
  * [#5375](https://github.com/leanprover/lean4/pull/5375) adds `bv_decide` normalization rules for `ofBool (a.getLsbD i)` and `ofBool a[i]` (@alexkeizer)
  * [#5423](https://github.com/leanprover/lean4/pull/5423) enhances the rewriting rules of `bv_decide`
  * [#5433](https://github.com/leanprover/lean4/pull/5433) presents the `bv_decide` counterexample at the API
  * [#5484](https://github.com/leanprover/lean4/pull/5484) handles `BitVec.ofNat` with `Nat` fvars in `bv_decide`
  * [#5506](https://github.com/leanprover/lean4/pull/5506), [#5507](https://github.com/leanprover/lean4/pull/5507) add `bv_normalize` rules.
  * [#5568](https://github.com/leanprover/lean4/pull/5568) generalize the `bv_normalize` pipeline to support more general preprocessing passes
  * [#5573](https://github.com/leanprover/lean4/pull/5573) gets `bv_normalize` up-to-date with the current `BitVec` rewrites
  * Cleanups: [#5408](https://github.com/leanprover/lean4/pull/5408), [#5493](https://github.com/leanprover/lean4/pull/5493), [#5578](https://github.com/leanprover/lean4/pull/5578)


* Elaboration improvements
  * [#5266](https://github.com/leanprover/lean4/pull/5266) preserve order of overapplied arguments in `elab_as_elim` procedure.
  * [#5510](https://github.com/leanprover/lean4/pull/5510) generalizes `elab_as_elim` to allow arbitrary motive applications.
  * [#5283](https://github.com/leanprover/lean4/pull/5283), [#5512](https://github.com/leanprover/lean4/pull/5512) refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit `_` arguments now.
  * [#5376](https://github.com/leanprover/lean4/pull/5376) modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.
  * [#5402](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/5419) must not reduce `ite` in the discriminant of `match`-expression when reducibility setting is `.reducible`
  * [#5474](https://github.com/leanprover/lean4/pull/5474) have autoparams report parameter/field on failure
  * [#5530](https://github.com/leanprover/lean4/pull/5530) makes automatic instance names about types with hygienic names be hygienic.

* Deriving handlers
  * [#5432](https://github.com/leanprover/lean4/pull/5432) makes `Repr` deriving instance handle explicit type parameters

* Functional induction
  * [#5364](https://github.com/leanprover/lean4/pull/5364) adds more equalities in context, more careful cleanup.

* Linters
  * [#5335](https://github.com/leanprover/lean4/pull/5335) fixes the unused variables linter complaining about match/tactic combinations
  * [#5337](https://github.com/leanprover/lean4/pull/5337) fixes the unused variables linter complaining about some wildcard patterns

* Other fixes
  * [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line

* Metaprogramming
  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
  * [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
  * [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
  * [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.
  * [#5587](https://github.com/leanprover/lean4/pull/5587) allows `MVarId.assertHypotheses` to set `BinderInfo` and `LocalDeclKind`.
  * [#5588](https://github.com/leanprover/lean4/pull/5588) adds `MVarId.tryClearMany'`, a variant of `MVarId.tryClearMany`.



### Language server, widgets, and IDE extensions

* [#5205](https://github.com/leanprover/lean4/pull/5205) decreases the latency of auto-completion in tactic blocks.
* [#5237](https://github.com/leanprover/lean4/pull/5237) fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.
* [#5257](https://github.com/leanprover/lean4/pull/5257) fixes several instances of incorrect auto-completions being reported.
* [#5299](https://github.com/leanprover/lean4/pull/5299) allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.
* [#5312](https://github.com/leanprover/lean4/pull/5312) fixes the server breaking when changing whitespace after the module header.
* [#5322](https://github.com/leanprover/lean4/pull/5322) fixes several instances of auto-completion reporting non-existent namespaces.
* [#5428](https://github.com/leanprover/lean4/pull/5428) makes sure to always report some recent file range as progress when waiting for elaboration.


### Pretty printing

* [#4979](https://github.com/leanprover/lean4/pull/4979) make pretty printer escape identifiers that are tokens.
* [#5389](https://github.com/leanprover/lean4/pull/5389) makes formatter use the current token table.
* [#5513](https://github.com/leanprover/lean4/pull/5513) use breakable instead of unbreakable whitespace when formatting tokens.


### Library

* [#5222](https://github.com/leanprover/lean4/pull/5222) reduces allocations in `Json.compress`.
* [#5231](https://github.com/leanprover/lean4/pull/5231) upstreams `Zero` and `NeZero`
* [#5292](https://github.com/leanprover/lean4/pull/5292) refactors `Lean.Elab.Deriving.FromToJson` (@arthur-adjedj)
* [#5415](https://github.com/leanprover/lean4/pull/5415) implements `Repr Empty` (@TomasPuverle)
* [#5421](https://github.com/leanprover/lean4/pull/5421) implements `To/FromJSON Empty` (@TomasPuverle)

* Logic
  * [#5263](https://github.com/leanprover/lean4/pull/5263) allows simplifying `dite_not`/`decide_not` with only `Decidable (¬p)`.
  * [#5268](https://github.com/leanprover/lean4/pull/5268) fixes binders on `ite_eq_left_iff`
  * [#5284](https://github.com/leanprover/lean4/pull/5284) turns off `Inhabited (Sum α β)` instances
  * [#5355](https://github.com/leanprover/lean4/pull/5355) adds simp lemmas for `LawfulBEq`
  * [#5374](https://github.com/leanprover/lean4/pull/5374) add `Nonempty` instances for products, allowing more `partial` functions to elaborate successfully
  * [#5447](https://github.com/leanprover/lean4/pull/5447) updates Pi instance names
  * [#5454](https://github.com/leanprover/lean4/pull/5454) makes some instance arguments implicit
  * [#5456](https://github.com/leanprover/lean4/pull/5456) adds `heq_comm`
  * [#5529](https://github.com/leanprover/lean4/pull/5529) moves `@[simp]` from `exists_prop'` to `exists_prop`

* `Bool`
  * [#5228](https://github.com/leanprover/lean4/pull/5228) fills gaps in Bool lemmas
  * [#5332](https://github.com/leanprover/lean4/pull/5332) adds notation `^^` for Bool.xor
  * [#5351](https://github.com/leanprover/lean4/pull/5351) removes `_root_.and` (and or/not/xor) and instead exports/uses `Bool.and` (etc.).

* `BitVec`
  * [#5240](https://github.com/leanprover/lean4/pull/5240) removes BitVec simps with complicated RHS
  * [#5247](https://github.com/leanprover/lean4/pull/5247) `BitVec.getElem_zeroExtend`
  * [#5248](https://github.com/leanprover/lean4/pull/5248) simp lemmas for BitVec, improving confluence
  * [#5249](https://github.com/leanprover/lean4/pull/5249) removes `@[simp]` from some BitVec lemmas
  * [#5252](https://github.com/leanprover/lean4/pull/5252) changes `BitVec.intMin/Max` from abbrev to def
  * [#5278](https://github.com/leanprover/lean4/pull/5278) adds `BitVec.getElem_truncate` (@tobiasgrosser)
  * [#5281](https://github.com/leanprover/lean4/pull/5281) adds udiv/umod bitblasting for `bv_decide` (@bollu)
  * [#5297](https://github.com/leanprover/lean4/pull/5297) `BitVec` unsigned order theoretic results
  * [#5313](https://github.com/leanprover/lean4/pull/5313) adds more basic BitVec ordering theory for UInt
  * [#5314](https://github.com/leanprover/lean4/pull/5314) adds `toNat_sub_of_le` (@bollu)
  * [#5357](https://github.com/leanprover/lean4/pull/5357) adds `BitVec.truncate` lemmas
  * [#5358](https://github.com/leanprover/lean4/pull/5358) introduces `BitVec.setWidth` to unify zeroExtend and truncate (@tobiasgrosser)
  * [#5361](https://github.com/leanprover/lean4/pull/5361) some BitVec GetElem lemmas
  * [#5385](https://github.com/leanprover/lean4/pull/5385) adds `BitVec.ofBool_[and|or|xor]_ofBool` theorems (@tobiasgrosser)
  * [#5404](https://github.com/leanprover/lean4/pull/5404) more of `BitVec.getElem_*` (@tobiasgrosser)
  * [#5410](https://github.com/leanprover/lean4/pull/5410) BitVec analogues of `Nat.{mul_two, two_mul, mul_succ, succ_mul}` (@bollu)
  * [#5411](https://github.com/leanprover/lean4/pull/5411) `BitVec.toNat_{add,sub,mul_of_lt}` for BitVector non-overflow reasoning (@bollu)
  * [#5413](https://github.com/leanprover/lean4/pull/5413) adds `_self`, `_zero`, and `_allOnes` for `BitVec.[and|or|xor]` (@tobiasgrosser)
  * [#5416](https://github.com/leanprover/lean4/pull/5416) adds LawCommIdentity + IdempotentOp for `BitVec.[and|or|xor]` (@tobiasgrosser)
  * [#5418](https://github.com/leanprover/lean4/pull/5418) decidable quantifers for BitVec
  * [#5450](https://github.com/leanprover/lean4/pull/5450) adds `BitVec.toInt_[intMin|neg|neg_of_ne_intMin]` (@tobiasgrosser)
  * [#5459](https://github.com/leanprover/lean4/pull/5459) missing BitVec lemmas
  * [#5469](https://github.com/leanprover/lean4/pull/5469) adds `BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft]` (@luisacicolini)
  * [#5478](https://github.com/leanprover/lean4/pull/5478) adds `BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight)` (@luisacicolini)
  * [#5487](https://github.com/leanprover/lean4/pull/5487) adds `sdiv_eq`, `smod_eq` to allow `sdiv`/`smod` bitblasting (@bollu)
  * [#5491](https://github.com/leanprover/lean4/pull/5491) adds `BitVec.toNat_[abs|sdiv|smod]` (@tobiasgrosser)
  * [#5492](https://github.com/leanprover/lean4/pull/5492) `BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not)` (@luisacicolini)
  * [#5499](https://github.com/leanprover/lean4/pull/5499) `BitVec.Lemmas` - drop non-terminal simps (@tobiasgrosser)
  * [#5505](https://github.com/leanprover/lean4/pull/5505) unsimps `BitVec.divRec_succ'`
  * [#5508](https://github.com/leanprover/lean4/pull/5508) adds `BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…` (@tobiasgrosser)
  * [#5554](https://github.com/leanprover/lean4/pull/5554) adds `Bitvec.[add, sub, mul]_eq_xor` and `width_one_cases` (@luisacicolini)

* `List`
  * [#5242](https://github.com/leanprover/lean4/pull/5242) improve naming for `List.mergeSort` lemmas
  * [#5302](https://github.com/leanprover/lean4/pull/5302) provide `mergeSort` comparator autoParam
  * [#5373](https://github.com/leanprover/lean4/pull/5373) fix name of `List.length_mergeSort`
  * [#5377](https://github.com/leanprover/lean4/pull/5377) upstream `map_mergeSort`
  * [#5378](https://github.com/leanprover/lean4/pull/5378) modify signature of lemmas about `mergeSort`
  * [#5245](https://github.com/leanprover/lean4/pull/5245) avoid importing `List.Basic` without List.Impl
  * [#5260](https://github.com/leanprover/lean4/pull/5260) review of List API
  * [#5264](https://github.com/leanprover/lean4/pull/5264) review of List API
  * [#5269](https://github.com/leanprover/lean4/pull/5269) remove HashMap's duplicated Pairwise and Sublist
  * [#5271](https://github.com/leanprover/lean4/pull/5271) remove @[simp] from `List.head_mem` and similar
  * [#5273](https://github.com/leanprover/lean4/pull/5273) lemmas about `List.attach`
  * [#5275](https://github.com/leanprover/lean4/pull/5275) reverse direction of `List.tail_map`
  * [#5277](https://github.com/leanprover/lean4/pull/5277) more `List.attach` lemmas
  * [#5285](https://github.com/leanprover/lean4/pull/5285) `List.count` lemmas
  * [#5287](https://github.com/leanprover/lean4/pull/5287) use boolean predicates in `List.filter`
  * [#5289](https://github.com/leanprover/lean4/pull/5289) `List.mem_ite_nil_left` and analogues
  * [#5293](https://github.com/leanprover/lean4/pull/5293) cleanup of `List.findIdx` / `List.take` lemmas
  * [#5294](https://github.com/leanprover/lean4/pull/5294) switch primes on `List.getElem_take`
  * [#5300](https://github.com/leanprover/lean4/pull/5300) more `List.findIdx` theorems
  * [#5310](https://github.com/leanprover/lean4/pull/5310) fix `List.all/any` lemmas
  * [#5311](https://github.com/leanprover/lean4/pull/5311) fix `List.countP` lemmas
  * [#5316](https://github.com/leanprover/lean4/pull/5316) `List.tail` lemma
  * [#5331](https://github.com/leanprover/lean4/pull/5331) fix implicitness of `List.getElem_mem`
  * [#5350](https://github.com/leanprover/lean4/pull/5350) `List.replicate` lemmas
  * [#5352](https://github.com/leanprover/lean4/pull/5352) `List.attachWith` lemmas
  * [#5353](https://github.com/leanprover/lean4/pull/5353) `List.head_mem_head?`
  * [#5360](https://github.com/leanprover/lean4/pull/5360) lemmas about `List.tail`
  * [#5391](https://github.com/leanprover/lean4/pull/5391) review of `List.erase` / `List.find` lemmas
  * [#5392](https://github.com/leanprover/lean4/pull/5392) `List.fold` / `attach` lemmas
  * [#5393](https://github.com/leanprover/lean4/pull/5393) `List.fold` relators
  * [#5394](https://github.com/leanprover/lean4/pull/5394) lemmas about `List.maximum?`
  * [#5403](https://github.com/leanprover/lean4/pull/5403) theorems about `List.toArray`
  * [#5405](https://github.com/leanprover/lean4/pull/5405) reverse direction of `List.set_map`
  * [#5448](https://github.com/leanprover/lean4/pull/5448) add lemmas about `List.IsPrefix` (@Command-Master)
  * [#5460](https://github.com/leanprover/lean4/pull/5460) missing `List.set_replicate_self`
  * [#5518](https://github.com/leanprover/lean4/pull/5518) rename `List.maximum?` to `max?`
  * [#5519](https://github.com/leanprover/lean4/pull/5519) upstream `List.fold` lemmas
  * [#5520](https://github.com/leanprover/lean4/pull/5520) restore `@[simp]` on `List.getElem_mem` etc.
  * [#5521](https://github.com/leanprover/lean4/pull/5521) List simp fixes
  * [#5550](https://github.com/leanprover/lean4/pull/5550) `List.unattach` and simp lemmas
  * [#5594](https://github.com/leanprover/lean4/pull/5594) induction-friendly `List.min?_cons`

* `Array`
  * [#5246](https://github.com/leanprover/lean4/pull/5246) cleanup imports of Array.Lemmas
  * [#5255](https://github.com/leanprover/lean4/pull/5255) split Init.Data.Array.Lemmas for better bootstrapping
  * [#5288](https://github.com/leanprover/lean4/pull/5288) rename `Array.data` to `Array.toList`
  * [#5303](https://github.com/leanprover/lean4/pull/5303) cleanup of `List.getElem_append` variants
  * [#5304](https://github.com/leanprover/lean4/pull/5304) `Array.not_mem_empty`
  * [#5400](https://github.com/leanprover/lean4/pull/5400) reorganization in Array/Basic
  * [#5420](https://github.com/leanprover/lean4/pull/5420) make `Array` functions either semireducible or use structural recursion
  * [#5422](https://github.com/leanprover/lean4/pull/5422) refactor `DecidableEq (Array α)`
  * [#5452](https://github.com/leanprover/lean4/pull/5452) refactor of Array
  * [#5458](https://github.com/leanprover/lean4/pull/5458) cleanup of Array docstrings after refactor
  * [#5461](https://github.com/leanprover/lean4/pull/5461) restore `@[simp]` on `Array.swapAt!_def`
  * [#5465](https://github.com/leanprover/lean4/pull/5465) improve Array GetElem lemmas
  * [#5466](https://github.com/leanprover/lean4/pull/5466) `Array.foldX` lemmas
  * [#5472](https://github.com/leanprover/lean4/pull/5472) @[simp] lemmas about `List.toArray`
  * [#5485](https://github.com/leanprover/lean4/pull/5485) reverse simp direction for `toArray_concat`
  * [#5514](https://github.com/leanprover/lean4/pull/5514) `Array.eraseReps`
  * [#5515](https://github.com/leanprover/lean4/pull/5515) upstream `Array.qsortOrd`
  * [#5516](https://github.com/leanprover/lean4/pull/5516) upstream `Subarray.empty`
  * [#5526](https://github.com/leanprover/lean4/pull/5526) fix name of `Array.length_toList`
  * [#5527](https://github.com/leanprover/lean4/pull/5527) reduce use of deprecated lemmas in Array
  * [#5534](https://github.com/leanprover/lean4/pull/5534) cleanup of Array GetElem lemmas
  * [#5536](https://github.com/leanprover/lean4/pull/5536) fix `Array.modify` lemmas
  * [#5551](https://github.com/leanprover/lean4/pull/5551) upstream `Array.flatten` lemmas
  * [#5552](https://github.com/leanprover/lean4/pull/5552) switch obvious cases of array "bang"`[]!` indexing to rely on hypothesis (@TomasPuverle)
  * [#5577](https://github.com/leanprover/lean4/pull/5577) add missing simp to `Array.size_feraseIdx`
  * [#5586](https://github.com/leanprover/lean4/pull/5586) `Array/Option.unattach`

* `Option`
  * [#5272](https://github.com/leanprover/lean4/pull/5272) remove @[simp] from `Option.pmap/pbind` and add simp lemmas
  * [#5307](https://github.com/leanprover/lean4/pull/5307) restoring Option simp confluence
  * [#5354](https://github.com/leanprover/lean4/pull/5354) remove @[simp] from `Option.bind_map`
  * [#5532](https://github.com/leanprover/lean4/pull/5532) `Option.attach`
  * [#5539](https://github.com/leanprover/lean4/pull/5539) fix explicitness of `Option.mem_toList`

* `Nat`
  * [#5241](https://github.com/leanprover/lean4/pull/5241) add @[simp] to `Nat.add_eq_zero_iff`
  * [#5261](https://github.com/leanprover/lean4/pull/5261) Nat bitwise lemmas
  * [#5262](https://github.com/leanprover/lean4/pull/5262) `Nat.testBit_add_one` should not be a global simp lemma
  * [#5267](https://github.com/leanprover/lean4/pull/5267) protect some Nat bitwise theorems
  * [#5305](https://github.com/leanprover/lean4/pull/5305) rename Nat bitwise lemmas
  * [#5306](https://github.com/leanprover/lean4/pull/5306) add `Nat.self_sub_mod` lemma
  * [#5503](https://github.com/leanprover/lean4/pull/5503) restore @[simp] to upstreamed `Nat.lt_off_iff`

* `Int`
  * [#5301](https://github.com/leanprover/lean4/pull/5301) rename `Int.div/mod` to `Int.tdiv/tmod`
  * [#5320](https://github.com/leanprover/lean4/pull/5320) add `ediv_nonneg_of_nonpos_of_nonpos` to DivModLemmas (@sakehl)

* `Fin`
  * [#5250](https://github.com/leanprover/lean4/pull/5250) missing lemma about `Fin.ofNat'`
  * [#5356](https://github.com/leanprover/lean4/pull/5356) `Fin.ofNat'` uses `NeZero`
  * [#5379](https://github.com/leanprover/lean4/pull/5379) remove some @[simp]s from Fin lemmas
  * [#5380](https://github.com/leanprover/lean4/pull/5380) missing Fin @[simp] lemmas

* `HashMap`
  * [#5244](https://github.com/leanprover/lean4/pull/5244) (`DHashMap`|`HashMap`|`HashSet`).(`getKey?`|`getKey`|`getKey!`|`getKeyD`)
  * [#5362](https://github.com/leanprover/lean4/pull/5362) remove the last use of `Lean.(HashSet|HashMap)`
  * [#5369](https://github.com/leanprover/lean4/pull/5369) `HashSet.ofArray`
  * [#5370](https://github.com/leanprover/lean4/pull/5370) `HashSet.partition`
  * [#5581](https://github.com/leanprover/lean4/pull/5581) `Singleton`/`Insert`/`Union` instances for `HashMap`/`Set`
  * [#5582](https://github.com/leanprover/lean4/pull/5582) `HashSet.all`/`any`
  * [#5590](https://github.com/leanprover/lean4/pull/5590) adding `Insert`/`Singleton`/`Union` instances for `HashMap`/`Set.Raw`
  * [#5591](https://github.com/leanprover/lean4/pull/5591) `HashSet.Raw.all/any`

* `Monads`
  * [#5463](https://github.com/leanprover/lean4/pull/5463) upstream some monad lemmas
  * [#5464](https://github.com/leanprover/lean4/pull/5464) adjust simp attributes on monad lemmas
  * [#5522](https://github.com/leanprover/lean4/pull/5522) more monadic simp lemmas

* Simp lemma cleanup
  * [#5251](https://github.com/leanprover/lean4/pull/5251) remove redundant simp annotations
  * [#5253](https://github.com/leanprover/lean4/pull/5253) remove Int simp lemmas that can't fire
  * [#5254](https://github.com/leanprover/lean4/pull/5254) variables appearing on both sides of an iff should be implicit
  * [#5381](https://github.com/leanprover/lean4/pull/5381) cleaning up redundant simp lemmas


### Compiler, runtime, and FFI

* [#4685](https://github.com/leanprover/lean4/pull/4685) fixes a typo in the C `run_new_frontend` signature
* [#4729](https://github.com/leanprover/lean4/pull/4729) has IR checker suggest using `noncomputable`
* [#5143](https://github.com/leanprover/lean4/pull/5143) adds a shared library for Lake
* [#5437](https://github.com/leanprover/lean4/pull/5437) removes (syntactically) duplicate imports (@euprunin)
* [#5462](https://github.com/leanprover/lean4/pull/5462) updates `src/lake/lakefile.toml` to the adjusted Lake build process
* [#5541](https://github.com/leanprover/lean4/pull/5541) removes new shared libs before build to better support Windows
* [#5558](https://github.com/leanprover/lean4/pull/5558) make `lean.h` compile with MSVC (@kant2002)
* [#5564](https://github.com/leanprover/lean4/pull/5564) removes non-conforming size-0 arrays (@eric-wieser)


### Lake
  * 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](https://github.com/leanprover/lean4/pull/5486), [#5572](https://github.com/leanprover/lean4/pull/5572), [#5583](https://github.com/leanprover/lean4/pull/5583), [#5600](https://github.com/leanprover/lean4/pull/5600), [#5641](https://github.com/leanprover/lean4/pull/5641), [#5642](https://github.com/leanprover/lean4/pull/5642).
  * [#5504](https://github.com/leanprover/lean4/pull/5504) lake new and lake init now produce TOML configurations by default.
  * [#5878](https://github.com/leanprover/lean4/pull/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](https://github.com/leanprover/lean4/pull/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).

### Documentation fixes

* [#3918](https://github.com/leanprover/lean4/pull/3918) `@[builtin_doc]` attribute (@digama0)
* [#4305](https://github.com/leanprover/lean4/pull/4305) explains the borrow syntax (@eric-wieser)
* [#5349](https://github.com/leanprover/lean4/pull/5349) adds documentation for `groupBy.loop` (@vihdzp)
* [#5473](https://github.com/leanprover/lean4/pull/5473) fixes typo in `BitVec.mul` docstring (@llllvvuu)
* [#5476](https://github.com/leanprover/lean4/pull/5476) fixes typos in `Lean.MetavarContext`
* [#5481](https://github.com/leanprover/lean4/pull/5481) removes mention of `Lean.withSeconds` (@alexkeizer)
* [#5497](https://github.com/leanprover/lean4/pull/5497) updates documentation and tests for `toUIntX` functions (@TomasPuverle)
* [#5087](https://github.com/leanprover/lean4/pull/5087) mentions that `inferType` does not ensure type correctness
* Many fixes to spelling across the doc-strings, (@euprunin): [#5425](https://github.com/leanprover/lean4/pull/5425) [#5426](https://github.com/leanprover/lean4/pull/5426) [#5427](https://github.com/leanprover/lean4/pull/5427) [#5430](https://github.com/leanprover/lean4/pull/5430)  [#5431](https://github.com/leanprover/lean4/pull/5431) [#5434](https://github.com/leanprover/lean4/pull/5434) [#5435](https://github.com/leanprover/lean4/pull/5435) [#5436](https://github.com/leanprover/lean4/pull/5436) [#5438](https://github.com/leanprover/lean4/pull/5438) [#5439](https://github.com/leanprover/lean4/pull/5439) [#5440](https://github.com/leanprover/lean4/pull/5440) [#5599](https://github.com/leanprover/lean4/pull/5599)

### Changes to CI

* [#5343](https://github.com/leanprover/lean4/pull/5343) allows addition of `release-ci` label via comment (@thorimur)
* [#5344](https://github.com/leanprover/lean4/pull/5344) sets check level correctly during workflow (@thorimur)
* [#5444](https://github.com/leanprover/lean4/pull/5444) Mathlib's `lean-pr-testing-NNNN` branches should use Batteries' `lean-pr-testing-NNNN` branches
* [#5489](https://github.com/leanprover/lean4/pull/5489) commit `lake-manifest.json` when updating `lean-pr-testing` branches
* [#5490](https://github.com/leanprover/lean4/pull/5490) use separate secrets for commenting and branching in `pr-release.yml`

v4.12.0
----------

### 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:

/--
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, #5074, #5100, #5113, #5137, #5203, #5212, #5220.

• simp tactic

  • #4988 fixes a panic in the reducePow simproc.
  • #5071 exposes the index option to the dsimp tactic, introduced to simp in #4202.
  • #5159 fixes a panic at Fin.isValue simproc.
  • #5167 and #5175 rename the simpCtorEq simproc to reduceCtorEq and makes it optional. (See breaking changes.)
  • #5187 ensures reduceCtorEq is enabled in the norm_cast tactic.
  • #5073 modifies the simp debug trace messages to tag with "dpre" and "dpost" instead of "pre" and "post" when in definitional rewrite mode. #5054 explains the reduce steps for trace.Debug.Meta.Tactic.simp trace messages.

• ext tactic

  • #4996 reduces default maximum iteration depth from 1000000 to 100.

• induction tactic

  • #5117 fixes a bug where let bindings in minor premises wouldn't be counted correctly.

• omega tactic

  • #5157 fixes a panic.

• conv tactic

  • #5149 improves arg n to handle subsingleton instance arguments.

• #5044 upstreams the #time command.

• #5079 makes #check and #reduce typecheck the elaborated terms.

• Incrementality

  • #4974 fixes regression where we would not interrupt elaboration of previous document versions.
  • #5004 fixes a performance regression.
  • #5001 disables incremental body elaboration in presence of where clauses in declarations.
  • #5018 enables infotrees on the command line for ilean generation.
  • #5040 and #5056 improve performance of info trees.
  • #5090 disables incrementality in the case .. | .. tactic.
  • #5312 fixes a bug where changing whitespace after the module header could break subsequent commands.

• Definitions

  • #5016 and #5066 add clean_wf tactic to clean up tactic state in decreasing_by. This can be disabled with set_option debug.rawDecreasingByGoal false.
  • #5055 unifies equational theorems between structural and well-founded recursion.
  • #5041 allows mutually recursive functions to use different parameter names among the “fixed parameter prefix”
  • #4154 and #5109 add fine-grained equational lemmas for non-recursive functions. See breaking changes.
  • #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 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 fixes bugs in recursion over predicates.

• Variable inclusion

  • #5206 documents that include currently only applies to theorems.

• Elaboration

  • #4926 fixes a bug where autoparam errors were associated to an incorrect source position.
  • #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 improves strength of the tactic that proves array indexing is in bounds.
  • #5119 fixes a bug in the tactic that proves indexing is in bounds where it could loop in the presence of mvars.
  • #5072 makes the structure type clickable in "not a field of structure" errors for structure instance notation.
  • #4717 fixes a bug where mutual inductive commands could create terms that the kernel rejects.
  • #5142 fixes a bug where variable could fail when mixing binder updates and declarations.

• Other fixes or improvements

  • #5118 changes the definition of the syntheticHole parser so that hovering over _ in ?_ gives the docstring for synthetic holes.
  • #5173 uses the emoji variant selector for ✅️,❌️,💥️ in messages, improving fonts selection.
  • #5183 fixes a bug in rename_i where implementation detail hypotheses could be renamed.

Language server, widgets, and IDE extensions

• #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 updates the user widget manual.
• #5193 updates the quickstart guide with the new display name for the Lean 4 extension ("Lean 4").
• #5185 fixes a bug where over time "import out of date" messages would accumulate.
• #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 localizes an instance in Lsp.Diagnostics.

Pretty printing

• #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 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 and #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 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 adds @[ext] attribute to Array.ext.
  • #4957 deprecates Array.get_modify.

• List

  • #4995 upstreams List.findIdx lemmas.
  • #5029, #5048 and #5132 add List.Sublist lemmas, some upstreamed. #5077 fixes implicitness in refl/rfl lemma binders. add List.Sublist theorems.
  • #5047 upstreams List.Pairwise lemmas.
  • #5053, #5124, and #5161 add List.find?/findSome?/findIdx? theorems.
  • #5039 adds List.foldlRecOn and List.foldrRecOn recursion principles to prove things about List.foldl and List.foldr.
  • #5069 upstreams List.Perm.
  • #5092 and #5107 add List.mergeSort and a fast @[csimp] implementation.
  • #5103 makes the simp lemmas for List.subset more aggressive.
  • #5106 changes the statement of List.getLast?_cons.
  • #5123 and #5158 add List.range and List.iota lemmas.
  • #5130 adds List.join lemmas.
  • #5131 adds List.append lemmas.
  • #5152 adds List.erase(|P|Idx) lemmas.
  • #5127 makes miscellaneous lemma updates.
  • #5153 and #5160 add lemmas about List.attach and List.pmap.
  • #5164, #5177, and #5215 add List.find? and List.range'/range/iota lemmas.
  • #5196 adds List.Pairwise_erase and related lemmas.
  • #5151 and #5163 improve confluence of List simp lemmas. #5105 and #5102 adjust List simp lemmas.
  • #5178 removes List.getLast_eq_iff_getLast_eq_some as a simp lemma.
  • #5210 reverses the meaning of List.getElem_drop and List.getElem_drop'.
  • #5214 moves @[csimp] lemmas earlier where possible.

• Nat and Int

  • #5104 adds Nat.add_left_eq_self and relatives.
  • #5146 adds missing Nat.and_xor_distrib_(left|right).
  • #5148 and #5190 improve Nat and Int simp lemma confluence.
  • #5165 adjusts Int simp lemmas.
  • #5166 adds Int lemmas relating neg and emod/mod.
  • #5208 reverses the direction of the Int.toNat_sub simp lemma.
  • #5209 adds Nat.bitwise lemmas.
  • #5230 corrects the docstrings for integer division and modulus.

• Option

  • #5128 and #5154 add Option lemmas.

• BitVec

  • #4889 adds sshiftRight bitblasting.
  • #4981 adds Std.Associative and Std.Commutative instances for BitVec.[and|or|xor].
  • #4913 enables missingDocs error for BitVec modules.
  • #4930 makes parameter names for BitVec more consistent.
  • #5098 adds BitVec.intMin. Introduces boolToPropSimps simp set for converting from boolean to propositional expressions.
  • #5200 and #5217 rename BitVec.getLsb to BitVec.getLsbD, etc., to bring naming in line with List/Array/etc.
  • Theorems: #4977, #4951, #4667, #5007, #4997, #5083, #5081, #4392

• UInt

  • #4514 fixes naming convention for UInt lemmas.

• Std.HashMap and Std.HashSet

  • #4943 deprecates variants of hash map query methods. (See breaking changes.)
  • #4917 switches the library and Lean to Std.HashMap and Std.HashSet almost everywhere.
  • #4954 deprecates Lean.HashMap and Lean.HashSet.
  • #5023 cleans up lemma parameters.

• Std.Sat (for bv_decide)

  • #4933 adds definitions of SAT and CNF.
  • #4953 defines "and-inverter graphs" (AIGs) as described in section 3 of Davis-Swords 2013.

• Parsec

  • #4774 generalizes the Parsec library, allowing parsing of iterable data beyond String such as ByteArray. (See breaking changes.)
  • #5115 moves Lean.Data.Parsec to Std.Internal.Parsec for bootstrappng reasons.

• Thunk

  • #4969 upstreams Thunk.ext.

• IO

  • #4973 modifies IO.FS.lines to handle \r\n on all operating systems instead of just on Windows.
  • #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 adds Array, Bool and Prod utilities from LeanSAT.
  • #4960 adds Relation.TransGen.trans.
  • #5012 states WellFoundedRelation Nat using <, not Nat.lt.
  • #5011 uses ≠ instead of Not (Eq ...) in Fin.ne_of_val_ne.
  • #5197 upstreams Fin.le_antisymm.
  • #5042 reduces usage of refine'.
  • #5101 adds about if-then-else and Option.
  • #5112 adds basic instances for ULift and PLift.
  • #5133 and #5168 make fixes from running the simpNF linter over Lean.
  • #5156 removes a bad simp lemma in omega theory.
  • #5155 improves confluence of Bool simp lemmas.
  • #5162 improves confluence of Function.comp simp lemmas.
  • #5191 improves confluence of if-then-else simp lemmas.
  • #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).
  • #5180 disables some simp lemmas with bad discrimination tree keys.
  • #5189 cleans up internal simp lemmas that had leaked.
  • #5198 cleans up allowUnsafeReducibility.
  • #5229 removes unused lemmas from some simp tactics.
  • #5199 removes >6 month deprecations.

Lean internals

• Performance
  • Some core algorithms have been rewritten in C++ for performance.
    • #4910 and #4912 reimplement instantiateLevelMVars.
    • #4915, #4922, and #4931 reimplement instantiateExprMVars, 30% faster on a benchmark.
  • #4934 has optimizations for the kernel's Expr equality test.
  • #4990 fixes bug in hashing for the kernel's Expr equality test.
  • #4935 and #4936 skip some PreDefinition transformations if they are not needed.
  • #5225 adds caching for visited exprs at CheckAssignmentQuick in ExprDefEq.
  • #5226 maximizes term sharing at instantiateMVarDeclMVars, used by runTactic.
• Diagnostics and profiling
  • #4923 adds profiling for instantiateMVars in Lean.Elab.MutualDef, which can be a bottleneck there.
  • #4924 adds diagnostics for large theorems, controlled by the diagnostics.threshold.proofSize option.
  • #4897 improves display of diagnostic results.
• Other fixes or improvements
  • #4921 cleans up Expr.betaRev.
  • #4940 fixes tests by not writing directly to stdout, which is unreliable now that elaboration and reporting are executed in separate threads.
  • #4955 documents that stderrAsMessages is now the default on the command line as well.
  • #4647 adjusts documentation for building on macOS.
  • #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 adds linter name to errors when a linter crashes.
  • #5043 cleans up command line snapshots logic.
  • #5067 minimizes some imports.
  • #5068 generalizes the monad for addMatcherInfo.
  • f71a1f adds missing test for #5126.
  • #5201 restores a test.
  • #3698 fixes a bug where label attributes did not pass on the attribute kind.
  • Typos: #5080, #5150, #5202

Compiler, runtime, and FFI

• #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 adds missing include in runtime for AUTO_THREAD_FINALIZATION feature on Windows.
• #4941 adds more LEAN_EXPORTs for Windows.
• #4911 improves formatting of CLI help text for the frontend.
• #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 handles the SIGBUS signal when detecting stack overflows.
• #5062 avoids overwriting existing signal handlers, like in rust-lang/rust#69685.
• #4860 improves workarounds for building on Windows. Splits libleanshared on Windows to avoid symbol limit, removes the LEAN_EXPORT denylist workaround, adds missing LEAN_EXPORTs.
• #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 links LibUV.

Lake

• #5030 removes dead code.
• #4770 adds additional fields to the package configuration which will be used by Reservoir. See the PR description for details.

DevOps/CI

• #4914 and #4937 improve the release checklist.
• #4925 ignores stale leanpkg tests.
• #5003 upgrades actions/cache in CI.
• #5010 sets save-always in cache actions in CI.
• #5008 adds more libuv search patterns for the speedcenter.
• #5009 reduce number of runs in the speedcenter for "fast" benchmarks from 10 to 3.
• #5014 adjusts lakefile editing to use new git syntax in pr-release workflow.
• #5025 has pr-release workflow pass --retry to curl.
• #5022 builds MacOS Aarch64 release for PRs by default.
• #5045 adds libuv to the required packages heading in macos docs.
• #5034 fixes the install name of libleanshared_1 on macOS.
• #5051 fixes Windows stage 0.
• #5052 fixes 32bit stage 0 builds in CI.
• #5057 avoids rebuilding leanmanifest in each build.
• #5099 makes restart-on-label workflow also filter by commit SHA.
• #4325 adds CaDiCaL.

Breaking changes

• LibUV 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)

• Recursive definitions with a decreasing_by clause that begins with simp_wf may break. Try removing simp_wf or replacing it with simp. (#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)

• 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, #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)

• Nat.strongInductionOn is now Nat.strongRecOn and Nat.caseStrongInductionOn to Nat.caseStrongRecOn. (#5147)

• The parameters to Membership.mem have been swapped, which affects all Membership instances. (#5020)

• The meanings of List.getElem_drop and List.getElem_drop' have been reversed and the first is now a simp lemma. (#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)

• The Lean module has switched from Lean.HashMap and Lean.HashSet to Std.HashMap and Std.HashSet (#4943). Lean.HashMap and Lean.HashSet are now deprecated (#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)
  • 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

Language features, tactics, and metaprograms

• The variable inclusion mechanism has been changed. Like before, when a definition mentions a variable, Lean will add it as an argument of the definition, but now in theorem bodies, variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an include command or are instance implicit and depend only on such variables. The omit command can be used to omit included variables.

  See breaking changes below.

  PRs: #4883, #4814, #5000, #5036, #5138, 0edf1b.

• Recursive definitions

  • Structural recursion can now be explicitly requested using

    termination_by structural x
    

    in analogy to the existing termination_by x syntax that causes well-founded recursion to be used. #4542

  • #4672 fixes a bug that could lead to ill-typed terms.

  • The termination_by? syntax no longer forces the use of well-founded recursion, and when structural recursion is inferred, it will print the result using the termination_by structural syntax.

  • Mutual structural recursion is now supported. This feature supports both mutual recursion over a non-mutual data type, as well as recursion over mutual or nested data types:

    mutual
    def Even : Nat → Prop
      | 0 => True
      | n+1 => Odd n
    
    def Odd : Nat → Prop
      | 0 => False
      | n+1 => Even n
    end
    
    mutual
    inductive A
    | other : B → A
    | empty
    inductive B
    | other : A → B
    | empty
    end
    
    mutual
    def A.size : A → Nat
    | .other b => b.size + 1
    | .empty => 0
    
    def B.size : B → Nat
    | .other a => a.size + 1
    | .empty => 0
    end
    
    inductive Tree where | node : List Tree → Tree
    
    mutual
    def Tree.size : Tree → Nat
    | node ts => Tree.list_size ts
    
    def Tree.list_size : List Tree → Nat
    | [] => 0
    | t::ts => Tree.size t + Tree.list_size ts
    end
    

    Functional induction principles are generated for these functions as well (A.size.induct, A.size.mutual_induct).

    Nested structural recursion is still not supported.

    PRs: #4639, #4715, #4642, #4656, #4684, #4715, #4728, #4575, #4731, #4658, #4734, #4738, #4718, #4733, #4787, #4788, #4789, #4807, #4772

  • #4809 makes unnecessary termination_by clauses cause warnings, not errors.

  • #4831 improves handling of nested structural recursion through non-recursive types.

  • #4839 improves support for structural recursive over inductive predicates when there are reflexive arguments.

• simp tactic

  • #4784 sets configuration Simp.Config.implicitDefEqProofs to true by default.

• omega tactic

  • #4612 normalizes the order that constraints appear in error messages.
  • #4695 prevents pushing casts into multiplications unless it produces a non-trivial linear combination.
  • #4989 fixes a regression.

• decide tactic

  • #4711 switches from using default transparency to at least default transparency when reducing the Decidable instance.
  • #4674 adds detailed feedback on decide tactic failure. It tells you which Decidable instances it unfolded, if it get stuck on Eq.rec it gives a hint about avoiding tactics when defining Decidable instances, and if it gets stuck on Classical.choice it gives hints about classical instances being in scope. During this process, it processes Decidable.recs and matches to pin blame on a non-reducing instance.

• @[ext] attribute

  • #4543 and #4762 make @[ext] realize ext_iff theorems from user ext theorems. Fixes the attribute so that @[local ext] and @[scoped ext] are usable. The @[ext (iff := false)] option can be used to turn off ext_iff realization.
  • #4694 makes "go to definition" work for the generated lemmas. Also adjusts the core library to make use of ext_iff generation.
  • #4710 makes ext_iff theorem preserve inst implicit binder types, rather than making all binder types implicit.

• #eval command

  • #4810 introduces a safer #eval command that prevents evaluation of terms that contain sorry. The motivation is that failing tactics, in conjunction with operations such as array accesses, can lead to the Lean process crashing. Users can use the new #eval! command to use the previous unsafe behavior. (#4829 adjusts a test.)

• #4447 adds #discr_tree_key and #discr_tree_simp_key commands, for helping debug discrimination tree failures. The #discr_tree_key t command prints the discrimination tree keys for a term t (or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys. The #discr_tree_simp_key command is similar to #discr_tree_key, but treats the underlying type as one of a simp lemma, that is it transforms it into an equality and produces the key of the left-hand side.

  For example,

  #discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
  -- bar _ (@OfNat.ofNat Nat _ _)
  
  #discr_tree_simp_key Nat.add_assoc
  -- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
  

• #4741 changes option parsing to allow user-defined options from the command line. Initial options are now re-parsed and validated after importing. Command line option assignments prefixed with weak. are silently discarded if the option name without the prefix does not exist.

• Deriving handlers

  • 7253ef and a04f3c improve the construction of the BEq deriving handler.
  • 86af04 makes BEq deriving handler work when there are dependently typed fields.
  • #4826 refactors the DecidableEq deriving handle to use termination_by structural.

• Metaprogramming

  • #4593 adds unresolveNameGlobalAvoidingLocals.
  • #4618 deletes deprecated functions from 2022.
  • #4642 adds Meta.lambdaBoundedTelescope.
  • #4731 adds Meta.withErasedFVars, to enter a context with some fvars erased from the local context.
  • #4777 adds assignment validation at closeMainGoal, preventing users from circumventing the occurs check for tactics such as exact.
  • #4807 introduces Lean.Meta.PProdN module for packing and projecting nested PProds.
  • #5170 fixes Syntax.unsetTrailing. A consequence of this is that "go to definition" now works on the last module name in an import block (issue #4958).

Language server, widgets, and IDE extensions

• #4727 makes it so that responses to info view requests come as soon as the relevant tactic has finished execution.
• #4580 makes it so that whitespace changes do not invalidate imports, and so starting to type the first declaration after imports should no longer cause them to reload.
• #4780 fixes an issue where hovering over unimported builtin names could result in a panic.

Pretty printing

• #4558 fixes the pp.instantiateMVars setting and changes the default value to true.
• #4631 makes sure syntax nodes always run their formatters. Fixes an issue where if ppSpace appears in a macro or elab command then it does not format with a space.
• #4665 fixes a bug where pretty printed signatures (for example in #check) were overly hoverable due to pp.tagAppFns being set.
• #4724 makes match pretty printer be sensitive to pp.explicit, which makes hovering over a match in the Infoview show the underlying term.
• #4764 documents why anonymous constructor notation isn't pretty printed with flattening.
• #4786 adjusts the parenthesizer so that only the parentheses are hoverable, implemented by having the parentheses "steal" the term info from the parenthesized expression.
• #4854 allows arbitrarily long sequences of optional arguments to be omitted from the end of applications, versus the previous conservative behavior of omitting up to one optional argument.

Library

• Nat
  • #4597 adds bitwise lemmas Nat.and_le_(left|right).
  • #4874 adds simprocs for simplifying bit expressions.
• Int
  • #4903 fixes performance of HPow Int Nat Int synthesis by rewriting it as a NatPow Int instance.
• UInt* and Fin
  • #4605 adds lemmas.
  • #4629 adds *.and_toNat.
• Option
  • #4599 adds get lemmas.
  • #4600 adds Option.or, a version of Option.orElse that is strict in the second argument.
• GetElem
  • #4603 adds getElem_congr to help with rewriting indices.
• List and Array
  • Upstreamed from Batteries: #4586 upstreams List.attach and Array.attach, #4697 upstreams List.Subset and List.Sublist and API, #4706 upstreams basic material on List.Pairwise and List.Nodup, #4720 upstreams more List.erase API, #4836 and #4837 upstream List.IsPrefix/List.IsSuffix/List.IsInfix and add Decidable instances, #4855 upstreams List.tail, List.findIdx, List.indexOf, List.countP, List.count, and List.range', #4856 upstreams more List lemmas, #4866 upstreams List.pairwise_iff_getElem, #4865 upstreams List.eraseIdx lemmas.
  • #4687 adjusts List.replicate simp lemmas and simprocs.
  • #4704 adds characterizations of List.Sublist.
  • #4707 adds simp normal form tests for List.Pairwise and List.Nodup.
  • #4708 and #4815 reorganize lemmas on list getters.
  • #4765 adds simprocs for literal array accesses such as #[1,2,3,4,5][2].
  • #4790 removes typeclass assumptions for List.Nodup.eraseP.
  • #4801 adds efficient usize functions for array types.
  • #4820 changes List.filterMapM to run left-to-right.
  • #4835 fills in and cleans up gaps in List API.
  • #4843, #4868, and #4877 correct List.Subset lemmas.
  • #4863 splits Init.Data.List.Lemmas into function-specific files.
  • #4875 fixes statement of List.take_takeWhile.
  • Lemmas: #4602, #4627, #4678 for List.head and list.getLast, #4723 for List.erase, #4742
• ByteArray
  • #4582 eliminates partial from ByteArray.toList and ByteArray.findIdx?.
• BitVec
  • #4568 adds recurrence theorems for bitblasting multiplication.
  • #4571 adds shiftLeftRec lemmas.
  • #4872 adds ushiftRightRec and lemmas.
  • #4873 adds getLsb_replicate.
• Std.HashMap added:
  • #4583 adds Std.HashMap as a verified replacement for Lean.HashMap. See the PR for naming differences, but #4725 renames HashMap.remove to HashMap.erase.
  • #4682 adds Inhabited instances.
  • #4732 improves BEq argument order in hash map lemmas.
  • #4759 makes lemmas resolve instances via unification.
  • #4771 documents that hash maps should be used linearly to avoid expensive copies.
  • #4791 removes bif from hash map lemmas, which is inconvenient to work with in practice.
  • #4803 adds more lemmas.
• SMap
  • #4690 upstreams SMap.foldM.
• BEq
  • #4607 adds PartialEquivBEq, ReflBEq, EquivBEq, and LawfulHashable classes.
• IO
  • #4660 adds IO.Process.Child.tryWait.
• #4747, #4730, and #4756 add ×' syntax for PProd. Adds a delaborator for PProd and MProd values to pretty print as flattened angle bracket tuples.
• Other fixes or improvements
  • #4604 adds lemmas for cond.
  • #4619 changes some definitions into theorems.
  • #4616 fixes some names with duplicated namespaces.
  • #4620 fixes simp lemmas flagged by the simpNF linter.
  • #4666 makes the Antisymm class be a Prop.
  • #4621 cleans up unused arguments flagged by linter.
  • #4680 adds imports for orphaned Init modules.
  • #4679 adds imports for orphaned Std.Data modules.
  • #4688 adds forward and backward directions of not_exists.
  • #4689 upstreams eq_iff_true_of_subsingleton.
  • #4709 fixes precedence handling for Repr instances for negative numbers for Int and Float.
  • #4760 renames TC ("transitive closure") to Relation.TransGen.
  • #4842 fixes List deprecations.
  • #4852 upstreams some Mathlib attributes applied to lemmas.
  • 93ac63 improves proof.
  • #4862 and #4878 generalize the universe for PSigma.exists and rename it to Exists.of_psigma_prop.
  • Typos: #4737, 7d2155
  • Docs: #4782, #4869, #4648

Lean internals

• Elaboration
  • #4596 enforces isDefEqStuckEx at unstuckMVar procedure, causing isDefEq to throw a stuck defeq exception if the metavariable was created in a previous level. This results in some better error messages, and it helps rw succeed in synthesizing instances (see issue #2736).
  • #4713 fixes deprecation warnings when there are overloaded symbols.
  • elab_as_elim algorithm:
    • #4722 adds check that inferred motive is type-correct.
    • #4800 elaborates arguments for parameters appearing in the types of targets.
    • #4817 makes the algorithm correctly handle eliminators with explicit motive arguments.
  • #4792 adds term elaborator for Lean.Parser.Term.namedPattern (e.g. n@(n' + 1)) to report errors when used in non-pattern-matching contexts.
  • #4818 makes anonymous dot notation work when the expected type is a pi-type-valued type synonym.
• Typeclass inference
  • #4646 improves synthAppInstances, the function responsible for synthesizing instances for the rw and apply tactics. Adds a synthesis loop to handle functions whose instances need to be synthesized in a complex order.
• Inductive types
  • #4684 (backported as 98ee78) refactors InductiveVal to have a numNested : Nat field instead of isNested : Bool. This modifies the kernel.
• Definitions
  • #4776 improves performance of Replacement.apply.
  • #4712 fixes .eq_def theorem generation with messy universes.
  • #4841 improves success of finding T.below x hypothesis when transforming match statements for IndPredBelow.
• Diagnostics and profiling
  • #4611 makes kernel diagnostics appear when diagnostics is enabled even if it is the only section.
  • #4753 adds missing profileitM functions.
  • #4754 adds Lean.Expr.numObjs to compute the number of allocated sub-expressions in a given expression, primarily for diagnosing performance issues.
  • #4769 adds missing withTraceNodes to improve trace.profiler output.
  • #4781 and #4882 make the "use set_option diagnostics true" message be conditional on current setting of diagnostics.
• Performance
  • #4767, #4775, and #4887 add ShareCommon.shareCommon' for sharing common terms. In an example with 16 million subterms, it is 20 times faster than the old shareCommon procedure.
  • #4779 ensures Expr.replaceExpr preserves DAG structure in Exprs.
  • #4783 documents performance issue in Expr.replaceExpr.
  • #4794, #4797, #4798 make for_each use precise cache.
  • #4795 makes Expr.find? and Expr.findExt? use the kernel implementations.
  • #4799 makes Expr.replace use the kernel implementation.
  • #4871 makes Expr.foldConsts use a precise cache.
  • #4890 makes expr_eq_fn use a precise cache.
• Utilities
  • #4453 upstreams ToExpr FilePath and compile_time_search_path%.
• Module system
  • #4652 fixes handling of const2ModIdx in finalizeImport, making it prefer the original module for a declaration when a declaration is re-declared.
• Kernel
  • #4637 adds a check to prevent large Nat exponentiations from evaluating. Elaborator reduction is controlled by the option exponentiation.threshold.
  • #4683 updates comments in kernel/declaration.h, making sure they reflect the current Lean 4 types.
  • #4796 improves performance by using replace with a precise cache.
  • #4700 improves performance by fixing the implementation of move constructors and move assignment operators. Expression copying was taking 10% of total runtime in some workloads. See issue #4698.
  • #4702 improves performance in replace_rec_fn::apply by avoiding expression copies. These copies represented about 13% of time spent in save_result in some workloads. See the same issue.
• Other fixes or improvements
  • #4590 fixes a typo in some constants and trace.profiler.useHeartbeats.
  • #4617 add 'since' dates to deprecated attributes.
  • #4625 improves the robustness of the constructor-as-variable test.
  • #4740 extends test with nice example reported on Zulip.
  • #4766 moves Syntax.hasIdent to be available earlier and shakes dependencies.
  • #4881 splits out Lean.Language.Lean.Types.
  • #4893 adds LEAN_EXPORT for sharecommon functions.
  • Typos: #4635, #4719, af40e6
  • Docs: #4748 (Command.Scope)

Compiler, runtime, and FFI

• #4661 moves Std from libleanshared to much smaller libInit_shared. This fixes the Windows build.
• #4668 fixes initialization, explicitly initializing Std in lean_initialize.
• #4746 adjusts shouldExport to exclude more symbols to get below Windows symbol limit. Some exceptions are added by #4884 and #4956 to support Verso.
• #4778 adds lean_is_exclusive_obj (Lean.isExclusiveUnsafe) and lean_set_external_data.
• #4515 fixes calling programs with spaces on Windows.

Lake

• #4735 improves a number of elements related to Git checkouts, cloud releases, and related error handling.

  • On error, Lake now prints all top-level logs. Top-level logs are those produced by Lake outside of the job monitor (e.g., when cloning dependencies).
  • When fetching a remote for a dependency, Lake now forcibly fetches tags. This prevents potential errors caused by a repository recreating tags already fetched.
  • Git error handling is now more informative.
  • The builtin package facets release, optRelease, extraDep are now captions in the same manner as other facets.
  • afterReleaseSync and afterReleaseAsync now fetch optRelease rather than release.
  • Added support for optional jobs, whose failure does not cause the whole build to failure. Now optRelease is such a job.

• #4608 adds draft CI workflow when creating new projects.

• #4847 adds CLI options to control log levels. The --log-level=<lv> controls the minimum log level Lake should output. For instance, --log-level=error will only print errors (not warnings or info). Also, adds an analogous --fail-level option to control the minimum log level for build failures. The existing --iofail and --wfail options are respectively equivalent to --fail-level=info and --fail-level=warning.

• Docs: #4853

DevOps/CI

• Workflows
  • #4531 makes release trigger an update of release.lean-lang.org.
  • #4598 adjusts pr-release to the new lakefile.lean syntax.
  • #4632 makes pr-release use the correct tag name.
  • #4638 adds ability to manually trigger nightly release.
  • #4640 adds more debugging output for restart-on-label CI.
  • #4663 bumps up waiting for 10s to 30s for restart-on-label.
  • #4664 bumps versions for actions/checkout and actions/upload-artifacts.
  • 582d6e bumps version for actions/download-artifact.
  • 6d9718 adds back dropped check-stage3.
  • 0768ad adds Jira sync (for FRO).
  • #4830 adds support to report CI errors on FRO Zulip.
  • #4838 adds trigger for nightly_bump_toolchain on mathlib4 upon nightly release.
  • abf420 fixes msys2.
  • #4895 deprecates Nix-based builds and removes interactive components. Users who prefer the flake build should maintain it externally.
• #4693, #4458, and #4876 update the release checklist.
• #4669 fixes the "max dynamic symbols" metric per static library.
• #4691 improves compatibility of tests/list_simp for retesting simp normal forms with Mathlib.
• #4806 updates the quickstart guide.
• c02aa9 documents the triage team in the contribution guide.

Breaking changes

• For @[ext]-generated ext and ext_iff lemmas, the x and y term arguments are now implicit. Furthermore these two lemmas are now protected (#4543).

• Now trace.profiler.useHearbeats is trace.profiler.useHeartbeats (#4590).

• A bugfix in the structural recursion code may in some cases break existing code, when a parameter of the type of the recursive argument is bound behind indices of that type. This can usually be fixed by reordering the parameters of the function (#4672).

• Now List.filterMapM sequences monadic actions left-to-right (#4820).

• The effect of the variable command on proofs of theorems has been changed. Whether such section variables are accessible in the proof now depends only on the theorem signature and other top-level commands, not on the proof itself. This change ensures that

  • the statement of a theorem is independent of its proof. In other words, changes in the proof cannot change the theorem statement.
  • tactics such as induction cannot accidentally include a section variable.
  • the proof can be elaborated in parallel to subsequent declarations in a future version of Lean.

  The effect of variables on the theorem header as well as on other kinds of declarations is unchanged.

  Specifically, section variables are included if they

  • are directly referenced by the theorem header,
  • are included via the new include command in the current section and not subsequently mentioned in an omit statement,
  • are directly referenced by any variable included by these rules, OR
  • are instance-implicit variables that reference only variables included by these rules.

  For porting, a new option deprecated.oldSectionVars is included to locally switch back to the old behavior.

v4.10.0

Language features, tactics, and metaprograms

• split tactic:

  • #4401 improves the strategy split uses to generalize discriminants of matches and adds trace.split.failure trace class for diagnosing issues.

• rw tactic:

  • #4385 prevents the tactic from claiming pre-existing goals are new subgoals.
  • dac1da adds configuration for ordering new goals, like for apply.

• simp tactic:

  • #4430 adds dsimprocs for if expressions (ite and dite).
  • #4434 improves heuristics for unfolding. Equational lemmas now have priorities where more-specific equationals lemmas are tried first before a possible catch-all.
  • #4481 fixes an issue where function-valued OfNat numeric literals would become denormalized.
  • #4467 fixes an issue where dsimp theorems might not apply to literals.
  • #4484 fixes the source position for the warning for deprecated simp arguments.
  • #4258 adds docstrings for dsimp configuration.
  • #4567 improves the accuracy of used simp lemmas reported by simp?.
  • fb9727 adds (but does not implement) the simp configuration option implicitDefEqProofs, which will enable including rfl-theorems in proof terms.

• omega tactic:

  • #4360 makes the tactic generate error messages lazily, improving its performance when used in tactic combinators.

• bv_omega tactic:

  • #4579 works around changes to the definition of Fin.sub in this release.

• #4490 sets up groundwork for a tactic index in generated documentation, as there was in Lean 3. See PR description for details.

• Commands

  • #4370 makes the variable command fully elaborate binders during validation, fixing an issue where some errors would be reported only at the next declaration.
  • #4408 fixes a discrepancy in universe parameter order between theorem and def declarations.
  • #4493 and #4482 fix a discrepancy in the elaborators for theorem, def, and example, making Prop-valued examples and other definition commands elaborate like theorems.
  • 8f023b, 3c4d6b and 0783d0 change the #reduce command to be able to control what gets reduced. For example, #reduce (proofs := true) (types := false) e reduces both proofs and types in the expression e. By default, neither proofs or types are reduced.
  • #4489 fixes an elaboration bug in #check_tactic.
  • #4505 adds support for open _root_.<namespace>.

• Options

  • #4576 adds the debug.byAsSorry option. Setting set_option debug.byAsSorry true causes all by ... terms to elaborate as sorry.
  • 7b56eb and d8e719 add the debug.skipKernelTC option. Setting set_option debug.skipKernelTC true turns off kernel typechecking. This is meant for temporarily working around kernel performance issues, and it compromises soundness since buggy tactics may produce invalid proofs, which will not be caught if this option is set to true.

• #4301 adds a linter to flag situations where a local variable's name is one of the argumentless constructors of its type. This can arise when a user either doesn't open a namespace or doesn't add a dot or leading qualifier, as in the following:

  inductive Tree (α : Type) where
    | leaf
    | branch (left : Tree α) (val : α) (right : Tree α)
  
  def depth : Tree α → Nat
    | leaf => 0
  

  With this linter, the leaf pattern is highlighted as a local variable whose name overlaps with the constructor Tree.leaf.

  The linter can be disabled with set_option linter.constructorNameAsVariable false.

  Additionally, the error message that occurs when a name in a pattern that takes arguments isn't valid now suggests similar names that would be valid. This means that the following definition:

  def length (list : List α) : Nat :=
    match list with
    | nil => 0
    | cons x xs => length xs + 1
  

  now results in the following warning:

  warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
  note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
  

  and error:

  invalid pattern, constructor or constant marked with '[match_pattern]' expected
  
  Suggestion: 'List.cons' is similar
  

• Metaprogramming

  • #4454 adds public Name.isInternalDetail function for filtering declarations using naming conventions for internal names.

• Other fixes or improvements

  • #4416 sorts the output of #print axioms for determinism.
  • #4528 fixes error message range for the cdot focusing tactic.

Language server, widgets, and IDE extensions

• #4443 makes the watchdog be more resilient against badly behaving clients.

Pretty printing

• #4433 restores fallback pretty printers when context is not available, and documents addMessageContext.
• #4556 introduces pp.maxSteps option and sets the default value of pp.deepTerms to false. Together, these keep excessively large or deep terms from overwhelming the Infoview.

Library

• #4560 splits GetElem class into GetElem and GetElem?. This enables removing Decidable instance arguments from GetElem.getElem? and GetElem.getElem!, improving their rewritability. See the docstrings for these classes for more information.
• Array
  • #4389 makes Array.toArrayAux_eq be a simp lemma.
  • #4399 improves robustness of the proof for Array.reverse_data.
• List
  • #4469 and #4475 improve the organization of the List API.
  • #4470 improves the List.set and List.concat API.
  • #4472 upstreams lemmas about List.filter from Batteries.
  • #4473 adjusts @[simp] attributes.
  • #4488 makes List.getElem?_eq_getElem be a simp lemma.
  • #4487 adds missing List.replicate API.
  • #4521 adds lemmas about List.map.
  • #4500 changes List.length_cons to use as.length + 1 instead of as.length.succ.
  • #4524 fixes the statement of List.filter_congr.
  • #4525 changes binder explicitness in List.bind_map.
  • #4550 adds maximum?_eq_some_iff' and minimum?_eq_some_iff?.
• #4400 switches the normal forms for indexing List and Array to xs[n] and xs[n]?.
• HashMap
  • #4372 fixes linearity in HashMap.insert and HashMap.erase, leading to a 40% speedup in a replace-heavy workload.
• Option
  • #4403 generalizes type of Option.forM from Unit to PUnit.
  • #4504 remove simp attribute from Option.elim and instead adds it to individual reduction lemmas, making unfolding less aggressive.
• Nat
  • #4242 adds missing theorems for n + 1 and n - 1 normal forms.
  • #4486 makes Nat.min_assoc be a simp lemma.
  • #4522 moves @[simp] from Nat.pred_le to Nat.sub_one_le.
  • #4532 changes various Nat.succ n to n + 1.
• Int
  • #3850 adds complete div/mod simprocs for Int.
• String/Char
  • #4357 make the byte size interface be Nat-valued with functions Char.utf8Size and String.utf8ByteSize.
  • #4438 upstreams Char.ext from Batteries and adds some Char documentation to the manual.
• Fin
  • #4421 adjusts Fin.sub to be more performant in definitional equality checks.
• Prod
  • #4526 adds missing Prod.map lemmas.
  • #4533 fixes binder explicitness in lemmas.
• BitVec
  • #4428 adds missing simproc for BitVec equality.
  • #4417 adds BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT.
• Std library
  • #4499 introduces Std, a library situated between Init and Lean, providing functionality not in the prelude both to Lean's implementation and to external users.
• Other fixes or improvements
  • #3056 standardizes on using (· == a) over (a == ·).
  • #4502 fixes errors reported by running the library through the the Batteries linters.

Lean internals

• #4391 makes getBitVecValue? recognize BitVec.ofNatLt.
• #4410 adjusts instantiateMVars algorithm to zeta reduce let expressions while beta reducing instantiated metavariables.
• #4420 fixes occurs check for metavariable assignments to also take metavariable types into account.
• #4425 fixes forEachModuleInDir to iterate over each Lean file exactly once.
• #3886 adds support to build Lean core oleans using Lake.
• Defeq and WHNF algorithms
  • #4387 improves performance of isDefEq by eta reducing lambda-abstracted terms during metavariable assignments, since these are beta reduced during metavariable instantiation anyway.
  • #4388 removes redundant code in isDefEqQuickOther.
• Typeclass inference
  • #4530 fixes handling of metavariables when caching results at synthInstance?.
• Elaboration
  • #4426 makes feature where the "don't know how to synthesize implicit argument" error reports the name of the argument more reliable.
  • #4497 fixes a name resolution bug for generalized field notation (dot notation).
  • #4536 blocks the implicit lambda feature for (e :) notation.
  • #4562 makes it be an error for there to be two functions with the same name in a where/let rec block.
• Recursion principles
  • #4549 refactors findRecArg, extracting withRecArgInfo. Errors are now reported in parameter order rather than the order they are tried (non-indices are tried first). For every argument, it will say why it wasn't tried, even if the reason is obvious (e.g. a fixed prefix or is Prop-typed, etc.).
• Porting core C++ to Lean
  • #4474 takes a step to refactor constructions toward a future port to Lean.
  • #4498 ports mk_definition_inferring_unsafe to Lean.
  • #4516 ports recOn construction to Lean.
  • #4517, #4653, and #4651 port below and brecOn construction to Lean.
• Documentation
  • #4501 adds a more-detailed docstring for PersistentEnvExtension.
• Other fixes or improvements
  • #4382 removes @[inline] attribute from NameMap.find?, which caused respecialization at each call site.
  • 5f9ded improves output of trace.Elab.snapshotTree.
  • #4424 removes "you might need to open '{dir}' in your editor" message that is now handled by Lake and the VS Code extension.
  • #4451 improves the performance of CollectMVars and FindMVar.
  • #4479 adds missing DecidableEq and Repr instances for intermediate structures used by the BitVec and Fin simprocs.
  • #4492 adds tests for a previous isDefEq issue.
  • 9096d6 removes PersistentHashMap.size.
  • #4508 fixes @[implemented_by] for functions defined by well-founded recursion.
  • #4509 adds additional tests for apply? tactic.
  • d6eab3 fixes a benchmark.
  • #4563 adds a workaround for a bug in IndPredBelow.mkBelowMatcher.
• Cleanup: #4380, #4431, #4494, e8f768, de2690, d3a756, #4404, #4537.

Compiler, runtime, and FFI

• d85d3d fixes criterion for tail-calls in ownership calculation.
• #3963 adds validation of UTF-8 at the C++-to-Lean boundary in the runtime.
• #4512 fixes missing unboxing in interpreter when loading initialized value.
• #4477 exposes the compiler flags for the bundled C compiler (clang).

Lake

• #4384 deprecates inputFile and replaces it with inputBinFile and inputTextFile. Unlike inputBinFile (and inputFile), inputTextFile normalizes line endings, which helps ensure text file traces are platform-independent.

• #4371 simplifies dependency resolution code.

• #4439 touches up the Lake configuration DSL and makes other improvements: string literals can now be used instead of identifiers for names, avoids using French quotes in lake new and lake init templates, changes the exe template to use Main for the main module, improves the math template error if lean-toolchain fails to download, and downgrades unknown configuration fields from an error to a warning to improve cross-version compatibility.

• #4496 tweaks require syntax and updates docs. Now require in TOML for a package name such as doc-gen4 does not need French quotes.

• #4485 fixes a bug where package versions in indirect dependencies would take precedence over direct dependencies.

• #4478 fixes a bug where Lake incorrectly included the module dynamic library in a platform-independent trace.

• #4529 fixes some issues with bad import errors. A bad import in an executable no longer prevents the executable's root module from being built. This also fixes a problem where the location of a transitive bad import would not been shown. The root module of the executable now respects nativeFacets.

• #4564 fixes a bug where non-identifier script names could not be entered on the CLI without French quotes.

• #4566 addresses a few issues with precompiled libraries.

  • Fixes a bug where Lake would always precompile the package of a module.
  • If a module is precompiled, it now precompiles its imports. Previously, it would only do this if imported.

• #4495, #4692, #4849 add a new type of require that fetches package metadata from a registry API endpoint (e.g. Reservoir) and then clones a Git package using the information provided. To require such a dependency, the new syntax is:

  require <scope> / <pkg-name> [@ git <rev>]
  -- Examples:
  require "leanprover" / "doc-gen4"
  require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
  

  Or in TOML:

  [[require]]
  name = "<pkg-name>"
  scope = "<scope>"
  rev = "<rev>"
  

  Unlike with Git dependencies, Lake can make use of the richer information provided by the registry to determine the default branch of the package. This means for repositories of packages like doc-gen4 which have a default branch that is not master, Lake will now use said default branch (e.g., in doc-gen4's case, main).

  Lake also supports configuring the registry endpoint via an environment variable: RESERVIOR_API_URL. Thus, any server providing a similar interface to Reservoir can be used as the registry. Further configuration options paralleling those of Cargo's Alternative Registries and Source Replacement will come in the future.

DevOps/CI

• #4427 uses Namespace runners for CI for leanprover/lean4.
• #4440 fixes speedcenter tests in CI.
• #4441 fixes that workflow change would break CI for unrebased PRs.
• #4442 fixes Wasm release-ci.
• 6d265b fixes for github.event.pull_request.merge_commit_sha sometimes not being available.
• 16cad2 adds optimization for CI to not fetch complete history.
• #4544 causes releases to be marked as prerelease on GitHub.
• #4446 switches Lake to using src/lake/lakefile.toml to avoid needing to load a version of Lake to build Lake.
• Nix
  • 5eb5fa fixes update-stage0-commit for Nix.
  • #4476 adds gdb to Nix shell.
  • e665a0 fixes update-stage0 for Nix.
  • 4808eb fixes cacheRoots for Nix.
  • #3811 adds platform-dependent flag to lib target.
  • #4587 adds linking of -lStd back into nix build flags on darwin.

Breaking changes

• Char.csize is replaced by Char.utf8Size (#4357).
• Library lemmas now are in terms of (· == a) over (a == ·) (#3056).
• Now the normal forms for indexing into List and Array is xs[n] and xs[n]? rather than using functions like List.get (#4400).
• Sometimes terms created via a sequence of unifications will be more eta reduced than before and proofs will require adaptation (#4387).
• The GetElem class has been split into two; see the docstrings for GetElem and GetElem? for more information (#4560).

v4.9.0

Language features, tactics, and metaprograms

• Definition transparency
  • #4053 adds the seal and unseal commands, which make definitions locally be irreducible or semireducible.
  • #4061 marks functions defined by well-founded recursion with @[irreducible] by default, which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
• Incrementality
  • #3940 extends incremental elaboration into various steps inside of declarations: definition headers, bodies, and tactics. .
  • 250994 and 67338b add @[incremental] attribute to mark an elaborator as supporting incremental elaboration.
  • #4259 improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
  • #4268 adds special handling for := by so that stray tokens in tactic blocks do not inhibit incrementality.
  • #4308 adds incremental have tactic.
  • #4340 fixes incorrect info tree reuse.
  • #4364 adds incrementality for careful command macros such as set_option in theorem, theorem foo.bar, and lemma.
  • #4395 adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
  • #4407 fixes non-incremental commands in macros blocking further incremental reporting.
  • #4436 fixes incremental reporting when there are nested tactics in terms.
  • #4459 adds incrementality support for next and if tactics.
  • #4554 disables incrementality for tactics in terms in tactics.
• Functional induction
  • #4135 ensures that the names used for functional induction are reserved.
  • #4327 adds support for structural recursion on reflexive types. For example,

    inductive Many (α : Type u) where
      | none : Many α
      | more : α → (Unit → Many α) → Many α
    
    def Many.map {α β : Type u} (f : α → β) : Many α → Many β
      | .none => .none
      | .more x xs => .more (f x) (fun _ => (xs ()).map f)
    
    #check Many.map.induct
    /-
    Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop)
      (case1 : motive Many.none)
      (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) :
      ∀ (a : Many α), motive a
    -/
    

• #3903 makes the Lean frontend normalize all line endings to LF before processing. This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
• #4130 makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
• split tactic
  • #4211 fixes split at h when h has forward dependencies.
  • #4349 allows split for if-expressions to work on non-propositional goals.
• apply tactic
  • #3929 makes error message for apply show implicit arguments in unification errors as needed. Modifies MessageData type (see breaking changes below).
• cases tactic
  • #4224 adds support for unification of offsets such as x + 20000 = 20001 in cases tactic.
• omega tactic
  • #4073 lets omega fall back to using classical Decidable instances when setting up contradiction proofs.
  • #4141 and #4184 fix bugs.
  • #4264 improves omega error message if no facts found in local context.
  • #4358 improves expression matching in omega by using match_expr.
• simp tactic

  • #4176 makes names of erased lemmas clickable.

  • #4208 adds a pretty printer for discrimination tree keys.

  • #4202 adds Simp.Config.index configuration option, which controls whether to use the full discrimination tree when selecting candidate simp lemmas. When index := false, only the head function is taken into account, like in Lean 3. This feature can help users diagnose tricky simp failures or issues in code from libraries developed using Lean 3 and then ported to Lean 4.

    In the following example, it will report that foo is a problematic theorem.

    opaque f : Nat → Nat → Nat
    
    @[simp] theorem foo : f x (x, y).2 = y := by sorry
    
    example : f a b ≤ b := by
      set_option diagnostics true in
      simp (config := { index := false })
    /-
    [simp] theorems with bad keys
      foo, key: f _ (@Prod.mk ℕ ℕ _ _).2
    -/
    

    With the information above, users can annotate theorems such as foo using no_index for problematic subterms. Example:

    opaque f : Nat → Nat → Nat
    
    @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
    
    example : f a b ≤ b := by
      simp -- `foo` is still applied with `index := true`
    

  • #4274 prevents internal match equational theorems from appearing in simp trace.

  • #4177 and #4359 make simp continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode.

  • #4341 fixes panic when applying @[simp] to malformed theorem syntax.

  • #4345 fixes simp so that it does not use the forward version of a user-specified backward theorem.

  • #4352 adds missing dsimp simplifications for fixed parameters of generated congruence theorems.

  • #4362 improves trace messages for simp so that constants are hoverable.

• Elaboration
  • #4046 makes subst notation (he ▸ h) try rewriting in both directions even when there is no expected type available.
  • #3328 adds support for identifiers in autoparams (for example, rfl in (h : x = y := by exact rfl)).
  • #4096 changes how the type in let and have is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance.
  • #4215 ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
  • #4267 cases signature elaboration errors to show even if there are parse errors in the body.
  • #4368 improves error messages when numeric literals fail to synthesize an OfNat instance, including special messages warning when the expected type of the numeral can be a proposition.
  • #4643 fixes issue leading to nested error messages and info trees vanishing, where snapshot subtrees were not restored on reuse.
  • #4657 calculates error suppression per snapshot, letting elaboration errors appear even when there are later parse errors (RFC #3556).
• Metaprogramming
  • #4167 adds Lean.MVarId.revertAll to revert all free variables.
  • #4169 adds Lean.MVarId.ensureNoMVar to ensure the goal's target contains no expression metavariables.
  • #4180 adds cleanupAnnotations parameter to forallTelescope methods.
  • #4307 adds support for parser aliases in syntax quotations.
• Work toward implementing grind tactic
  • 0a515e and #4164 add grind_norm and grind_norm_proc attributes and @[grind_norm] theorems.
  • #4170, #4221, and #4249 create grind preprocessor and core module.
  • #4235 and d6709e add special cases tactic to grind along with @[grind_cases] attribute to mark types that this cases tactic should automatically apply to.
  • #4243 adds special injection? tactic to grind.
• Other fixes or improvements
  • #4065 fixes a bug in the Nat.reduceLeDiff simproc.
  • #3969 makes deprecation warnings activate even for generalized field notation ("dot notation").
  • #4132 fixes the sorry term so that it does not activate the implicit lambda feature
  • 9803c5 and 47c8e3 move cdot and calc parsers to Lean namespace.
  • #4252 fixes the case tactic so that it is usable in macros by having it erase macro scopes from the tag.
  • 26b671 and cc33c3 extract haveId syntax.
  • #4335 fixes bugs in partial calc tactic when there is mdata or metavariables.
  • #4329 makes termination_by? report unused each unused parameter as _.
• Docs: #4238, #4294, #4338.

Language server, widgets, and IDE extensions

• #4066 fixes features like "Find References" when browsing core Lean sources.
• #4254 allows embedding user widgets in structured messages. Companion PR is vscode-lean4#449.
• #4445 makes watchdog more resilient against badly behaving clients.

Library

• #4059 upstreams many List and Array operations and theorems from Batteries.
• #4055 removes the unused Inhabited instance for Subtype.
• #3967 adds dates in existing @[deprecated] attributes.
• #4231 adds boilerplate Char, UInt, and Fin theorems.
• #4205 fixes the MonadStore type classes to use semiOutParam.
• #4350 renames IsLawfulSingleton to LawfulSingleton.
• Nat
  • #4094 swaps Nat.zero_or and Nat.or_zero.
  • #4098 and #4145 change the definition of Nat.mod so that n % (m + n) reduces when n is literal without relying on well-founded recursion, which becomes irreducible by default in #4061.
  • #4188 redefines Nat.testBit to be more performant.
  • Theorems: #4199.
• Array
  • #4074 improves the functional induction principle Array.feraseIdx.induct.
• List
  • #4172 removes @[simp] from List.length_pos.
• Option
  • #4037 adds theorems to simplify Option-valued dependent if-then-else.
  • #4314 removes @[simp] from Option.bind_eq_some.
• BitVec
  • Theorems: #3920, #4095, #4075, #4148, #4165, #4178, #4200, #4201, #4298, #4299, #4257, #4179, #4321, #4187.
  • #4193 adds simprocs for reducing x >>> i and x <<< i where i is a bitvector literal.
  • #4194 adds simprocs for reducing (x <<< i) <<< j and (x >>> i) >>> j where i and j are natural number literals.
  • #4229 redefines rotateLeft/rotateRight to use modulo reduction of shift offset.
  • 0d3051 makes <num>#<term> bitvector literal notation global.
• Char/String
  • #4143 modifies String.substrEq to avoid linter warnings in downstream code.
  • #4233 adds simprocs for Char and String inequalities.
  • #4348 upstreams Mathlib lemmas.
  • #4354 upstreams basic String lemmas.
• HashMap
  • #4248 fixes implicitness of typeclass arguments in HashMap.ofList.
• IO
  • #4036 adds IO.Process.getCurrentDir and IO.Process.setCurrentDir for adjusting the current process's working directory.
• Cleanup: #4077, #4189, #4304.
• Docs: #4001, #4166, #4332.

Lean internals

• Defeq and WHNF algorithms
  • #4029 remove unnecessary checkpointDefEq
  • #4206 fixes isReadOnlyOrSyntheticOpaque to respect metavariable depth.
  • #4217 fixes missing occurs check for delayed assignments.
• Definition transparency
  • #4052 adds validation to application of @[reducible]/@[semireducible]/@[irreducible] attributes (with local/scoped modifiers as well). Setting set_option allowUnsafeReductibility true turns this validation off.
• Inductive types
  • #3591 fixes a bug where indices could be incorrectly promoted to parameters.
  • #3398 fixes a bug in the injectivity theorem generator.
  • #4342 fixes elaboration of mutual inductives with instance parameters.
• Diagnostics and profiling
  • #3986 adds option trace.profiler.useHeartbeats to switch trace.profiler.threshold to being in terms of heartbeats instead of milliseconds.
  • #4082 makes set_option diagnostics true report kernel diagnostic information.
• Typeclass resolution
  • #4119 fixes multiple issues with TC caching interacting with synthPendingDepth, adds maxSynthPendingDepth option with default value 1.
  • #4210 ensures local instance cache does not contain multiple copies of the same instance.
  • #4216 fix handling of metavariables, to avoid needing to set the option backward.synthInstance.canonInstances to false.
• Other fixes or improvements
  • #4080 fixes propagation of state for Lean.Elab.Command.liftCoreM and Lean.Elab.Command.liftTermElabM.
  • #3944 makes the Repr deriving handler be consistent between structure and inductive for how types and proofs are erased.
  • #4113 propagates maxHeartbeats to kernel to control "(kernel) deterministic timeout" error.
  • #4125 reverts #3970 (monadic generalization of FindExpr).
  • #4128 catches stack overflow in auto-bound implicits feature.
  • #4129 adds tryCatchRuntimeEx combinator to replace catchRuntimeEx reader state.
  • #4155 simplifies the expression canonicalizer.
  • #4151 and #4369 add many missing trace classes.
  • #4185 makes congruence theorem generators clean up type annotations of argument types.
  • #4192 fixes restoration of infotrees when auto-bound implicit feature is activated, fixing a pretty printing error in hovers and strengthening the unused variable linter.
  • dfb496 fixes declareBuiltin to allow it to be called multiple times per declaration.
  • #4569 fixes an issue introduced in a merge conflict, where the interrupt exception was swallowed by some tryCatchRuntimeEx uses.
  • #4584 (backported as b056a0) adapts kernel interruption to the new cancellation system.
  • Cleanup: #4112, #4126, #4091, #4139, #4153.
  • Tests: 030406, #4133.

Compiler, runtime, and FFI

• #4100 improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
• #2903 fixes segfault in old compiler from mishandling noConfusion applications.
• #4311 fixes bug in constant folding.
• #3915 documents the runtime memory layout for inductive types.

Lake

• #4518 makes trace reading more robust. Lake now rebuilds if trace files are invalid or unreadable and is backwards compatible with previous pure numeric traces.
• #4057 adds support for docstrings on require commands.
• #4088 improves hovers for family_def and library_data commands.
• #4147 adds default README.md to package templates
• #4261 extends lake test help page, adds help page for lake check-test, adds lake lint and tag @[lint_driver], adds support for specifying test and lint drivers from dependencies, adds testDriverArgs and lintDriverArgs options, adds support for library test drivers, makes lake check-test and lake check-lint only load the package without dependencies.
• #4270 adds lake pack and lake unpack for packing and unpacking Lake build artifacts from an archive.
• #4083 Switches the manifest format to use major.minor.patch semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after 0.x) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifests with numeric versions. It will treat the numeric version N as semantic version 0.N.0. Lake will also accept manifest versions with - suffixes (e.g., x.y.z-foo) and then ignore the suffix.
• #4273 adds a lift from JobM to FetchM for backwards compatibility reasons.
• #4351 fixes LogIO-to-CliM-lifting performance issues.
• #4343 make Lake store the dependency trace for a build in the cached build long and then verifies that it matches the trace of the current build before replaying the log.
• #4402 moves the cached log into the trace file (no more .log.json). This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace. Separately, .hash file generation was changed to be more reliable as well. The .hash files are deleted as part of the build and always regenerate with --rehash.
• Other fixes or improvements
  • #4056 cleans up tests
  • #4244 fixes noRelease test when Lean repo is tagged
  • #4346 improves tests/serve
  • #4356 adds build log path to the warning for a missing or invalid build log.

DevOps

• #3984 adds a script (script/rebase-stage0.sh) for git rebase -i that automatically updates each stage0.
• #4108 finishes renamings from transition to Std to Batteries.
• #4109 adjusts the Github bug template to mention testing using live.lean-lang.org.
• #4136 makes CI rerun only when full-ci label is added or removed.
• #4175 and 72b345 switch to using #guard_msgs to run tests as much as possible.
• #3125 explains the Lean4 pygments lexer.
• #4247 sets up a procedure for preparing release notes.
• #4032 modernizes build instructions and workflows.
• #4255 moves some expensive checks from merge queue to releases.
• #4265 adds aarch64 macOS as native compilation target for CI.
• f05a82 restores macOS aarch64 install suffix in CI
• #4317 updates build instructions for macOS.
• #4333 adjusts workflow to update Batteries in manifest when creating lean-pr-testing-NNNN Mathlib branches.
• #4355 simplifies lean4checker step of release checklist.
• #4361 adds installing elan to pr-release CI step.
• #4628 fixes the Windows build, which was missing an exported symbol.

Breaking changes

While most changes could be considered to be a breaking change, this section makes special note of API changes.

• Nat.zero_or and Nat.or_zero have been swapped (#4094).
• IsLawfulSingleton is now LawfulSingleton (#4350).
• The BitVec literal notation is now <num>#<term> rather than <term>#<term>, and it is global rather than scoped. Use BitVec.ofNat w x rather than x#w when x is a not a numeric literal (0d3051).
• BitVec.rotateLeft and BitVec.rotateRight now take the shift modulo the bitwidth (#4229).
• These are no longer simp lemmas: List.length_pos (#4172), Option.bind_eq_some (#4314).
• Types in let and have (both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed (#4096). In particular, tactics embedded in the type will no longer make use of the type of value in expressions such as let x : type := value; body.
• Now functions defined by well-founded recursion are marked with @[irreducible] by default (#4061). Existing proofs that hold by definitional equality (e.g. rfl) can be rewritten to explicitly unfold the function definition (using simp, unfold, rw), or the recursive function can be temporarily made semireducible (using unseal f in before the command), or the function definition itself can be marked as @[semireducible] to get the previous behavior.
• Due to #3929:

  • The MessageData.ofPPFormat constructor has been removed. Its functionality has been split into two:

    • for lazy structured messages, please use MessageData.lazy;
    • for embedding Format or FormatWithInfos, use MessageData.ofFormatWithInfos.

    An example migration can be found in #3929.

  • The MessageData.ofFormat constructor has been turned into a function. If you need to inspect MessageData, you can pattern-match on MessageData.ofFormatWithInfos.

v4.8.0

Language features, tactics, and metaprograms

• Functional induction principles. #3432, #3620, #3754, #3762, #3738, #3776, #3898.

  Derived from the definition of a (possibly mutually) recursive function, a functional induction principle is created that is tailored to proofs about that function.

  For example from:

  def ackermann : Nat → Nat → Nat
    | 0, m => m + 1
    | n+1, 0 => ackermann n 1
    | n+1, m+1 => ackermann n (ackermann (n + 1) m)
  

  we get

  ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
    (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
    (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
    (x x : Nat) : motive x x
  

  It can be used in the induction tactic using the using syntax:

  induction n, m using ackermann.induct
  

• The termination checker now recognizes more recursion patterns without an explicit termination_by. In particular the idiom of counting up to an upper bound, as in

  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
    if _ : i < arr.size then
      Array.sum arr (i+1) (acc + arr[i])
    else
      acc
  

  is recognized without having to say termination_by arr.size - i.

  • #3630 makes termination_by? not use sizeOf when not needed
  • #3652 improves the termination_by syntax.
  • #3658 changes how termination arguments are elaborated.
  • #3665 refactors GuessLex to allow inferring more complex termination arguments
  • #3666 infers termination arguments such as xs.size - i

• #3629, #3655, #3747: Adds @[induction_eliminator] and @[cases_eliminator] attributes to be able to define custom eliminators for the induction and cases tactics, replacing the @[eliminator] attribute. Gives custom eliminators for Nat so that induction and cases put goal states into terms of 0 and n + 1 rather than Nat.zero and Nat.succ n. Added option tactic.customEliminators to control whether to use custom eliminators. Added a hack for rcases/rintro/obtain to use the custom eliminator for Nat.

• Shorter instances names. There is a new algorithm for generating names for anonymous instances. Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%. With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters. The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm. While the new algorithm produces names that are 1.2% less unique, it avoids cross-project collisions by adding a module-based suffix when it does not refer to declarations from the same "project" (modules that share the same root). #3089 and #3934.

• 8d2adf Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).

• 84b091 Lean now generates an error if the type of a theorem is not a proposition.

• Definition transparency. 47a343. @[reducible], @[semireducible], and @[irreducible] are now scoped and able to be set for imported declarations.

• simp/dsimp

  • #3607 enables kernel projection reduction in dsimp
  • b24fbf and acdb00: dsimproc command to define defeq-preserving simplification procedures.
  • #3624 makes dsimp normalize raw nat literals as OfNat.ofNat applications.
  • #3628 makes simp correctly handle OfScientific.ofScientific literals.
  • #3654 makes dsimp? report used simprocs.
  • dee074 fixes equation theorem handling in simp for non-recursive definitions.
  • #3819 improved performance when simp encounters a loop.
  • #3821 fixes discharger/cache interaction.
  • #3824 keeps simp from breaking Char literals.
  • #3838 allows Nat instances matching to be more lenient.
  • #3870 documentation for simp configuration options.
  • #3972 fixes simp caching.
  • #4044 improves cache behavior for "well-behaved" dischargers.

• omega

  • #3639, #3766, #3853, #3875: introduces a term canonicalizer.
  • #3736 improves handling of positivity for the modulo operator for Int.
  • #3828 makes it work as a simp discharger.
  • #3847 adds helpful error messages.

• rfl

  • #3671, #3708: upstreams the @[refl] attribute and the rfl tactic.
  • #3751 makes apply_rfl not operate on Eq itself.
  • #4067 improves error message when there are no goals.

• #3719 upstreams the rw? tactic, with fixes and improvements in #3783, #3794, #3911.

• conv

  • #3659 adds a conv version of the calc tactic.
  • #3763 makes conv clean up using try with_reducible rfl instead of try rfl.

• #guard_msgs

  • #3617 introduces whitespace protection using the ⏎ character.
  • #3883: The #guard_msgs command now has options to change whitespace normalization and sensitivity to message ordering. For example, #guard_msgs (whitespace := lax) in cmd collapses whitespace before checking messages, and #guard_msgs (ordering := sorted) in cmd sorts the messages in lexicographic order before checking.
  • #3931 adds an unused variables ignore function for #guard_msgs.
  • #3912 adds a diff between the expected and actual outputs. This feature is currently disabled by default, but can be enabled with set_option guard_msgs.diff true. Depending on user feedback, this option may default to true in a future version of Lean.

• do notation

  • #3820 makes it an error to lift (<- ...) out of a pure if ... then ... else ...

• Lazy discrimination trees

  • #3610 fixes a name collision for LazyDiscrTree that could lead to cache poisoning.
  • #3677 simplifies and fixes LazyDiscrTree handling for exact?/apply?.
  • #3685 moves general exact?/apply? functionality into LazyDiscrTree.
  • #3769 has lemma selection improvements for rw? and LazyDiscrTree.
  • #3818 improves ordering of matches.

• #3590 adds inductive.autoPromoteIndices option to be able to disable auto promotion of indices in the inductive command.

• Miscellaneous bug fixes and improvements

  • #3606 preserves cache and dischargeDepth fields in Lean.Meta.Simp.Result.mkEqSymm.
  • #3633 makes elabTermEnsuringType respect errToSorry, improving error recovery of the have tactic.
  • #3647 enables noncomputable unsafe definitions, for deferring implementations until later.
  • #3672 adjust namespaces of tactics.
  • #3725 fixes Ord derive handler for indexed inductive types with unused alternatives.
  • #3893 improves performance of derived Ord instances.
  • #3771 changes error reporting for failing tactic macros. Improves rfl error message.
  • #3745 fixes elaboration of generalized field notation if the object of the notation is an optional parameter.
  • #3799 makes commands such as universe, variable, namespace, etc. require that their argument appear in a later column. Commands that can optionally parse an ident or parse any number of idents generally should require that the ident use colGt. This keeps typos in commands from being interpreted as identifiers.
  • #3815 lets the split tactic be used for writing code.
  • #3822 adds missing info in induction tactic for with clauses of the form | cstr a b c => ?_.
  • #3806 fixes withSetOptionIn combinator.
  • #3844 removes unused trace.Elab.syntax option.
  • #3896 improves hover and go-to-def for attribute command.
  • #3989 makes linter options more discoverable.
  • #3916 fixes go-to-def for syntax defined with @[builtin_term_parser].
  • #3962 fixes how solveByElim handles symm lemmas, making exact?/apply? usable again.
  • #3968 improves the @[deprecated] attribute, adding (since := "<date>") field.
  • #3768 makes #print command show structure fields.
  • #3974 makes exact?% behave like by exact? rather than by apply?.
  • #3994 makes elaboration of he ▸ h notation more predictable.
  • #3991 adjusts transparency for decreasing_trivial macros.
  • #4092 improves performance of binop% and binrel% expression tree elaborators.

• Docs: #3748, #3796, #3800, #3874, #3863, #3862, #3891, #3873, #3908, #3872.

Language server and IDE extensions

• #3602 enables import auto-completions.
• #3608 fixes issue leanprover/vscode-lean4#392. Diagnostic ranges had an off-by-one error that would misplace goal states for example.
• #3014 introduces snapshot trees, foundational work for incremental tactics and parallelism. #3849 adds basic incrementality API.
• #3271 adds support for server-to-client requests.
• #3656 fixes jump to definition when there are conflicting names from different files. Fixes issue #1170.
• #3691, #3925, #3932 keep semantic tokens synchronized (used for semantic highlighting), with performance improvements.
• #3247 and #3730 add diagnostics to run "Restart File" when a file dependency is saved.
• #3722 uses the correct module names when displaying references.
• #3728 makes errors in header reliably appear and makes the "Import out of date" warning be at "hint" severity. #3739 simplifies the text of this warning.
• #3778 fixes #3462, where info nodes from before the cursor would be used for computing completions.
• #3985 makes trace timings appear in Infoview.

Pretty printing

• #3797 fixes the hovers over binders so that they show their types.
• #3640 and #3735: Adds attribute @[pp_using_anonymous_constructor] to make structures pretty print as ⟨x, y, z⟩ rather than as {a := x, b := y, c := z}. This attribute is applied to Sigma, PSigma, PProd, Subtype, And, and Fin.
• #3749 Now structure instances pretty print with parent structures' fields inlined. That is, if B extends A, then { toA := { x := 1 }, y := 2 } now pretty prints as { x := 1, y := 2 }. Setting option pp.structureInstances.flatten to false turns this off.
• #3737, #3744 and #3750: Option pp.structureProjections is renamed to pp.fieldNotation, and there is now a suboption pp.fieldNotation.generalized to enable pretty printing function applications using generalized field notation (defaults to true). Field notation can be disabled on a function-by-function basis using the @[pp_nodot] attribute. The notation is not used for theorems.
• #4071 fixes interaction between app unexpanders and pp.fieldNotation.generalized
• #3625 makes delabConstWithSignature (used by #check) have the ability to put arguments "after the colon" to avoid printing inaccessible names.
• #3798, #3978, #3798: Adds options pp.mvars (default: true) and pp.mvars.withType (default: false). When pp.mvars is false, expression metavariables pretty print as ?_ and universe metavariables pretty print as _. When pp.mvars.withType is true, expression metavariables pretty print with a type ascription. These can be set when using #guard_msgs to make tests not depend on the particular names of metavariables.
• #3917 makes binders hoverable and gives them docstrings.
• #4034 makes hovers for RHS terms in match expressions in the Infoview reliably show the correct term.

Library

• Bool/Prop

  • #3508 improves simp confluence for Bool and Prop terms.
  • Theorems: #3604

• Nat

  • #3579 makes Nat.succ_eq_add_one be a simp lemma, now that induction/cases uses n + 1 instead of Nat.succ n.
  • #3808 replaces Nat.succ simp rules with simprocs.
  • #3876 adds faster Nat.repr implementation in C.

• Int

  • Theorems: #3890

• UInts

  • #3960 improves performance of upcasting.

• Array and Subarray

  • #3676 removes Array.eraseIdxAux, Array.eraseIdxSzAux, and Array.eraseIdx'.
  • #3648 simplifies Array.findIdx?.
  • #3851 renames fields of Subarray.

• List

  • #3785 upstreams tail-recursive List operations and @[csimp] lemmas.

• BitVec

  • Theorems: #3593, #3593, #3597, #3598, #3721, #3729, #3880, #4039.
  • #3884 protects Std.BitVec.

• String

  • #3832 fixes String.splitOn.
  • #3959 adds String.Pos.isValid.
  • #3959 UTF-8 string validation.
  • #3961 adds a model implementation for UTF-8 encoding and decoding.

• IO

  • #4097 adds IO.getTaskState which returns whether a task is finished, actively running, or waiting on other Tasks to finish.

• Refactors

  • #3605 reduces imports for Init.Data.Nat and Init.Data.Int.
  • #3613 reduces imports for Init.Omega.Int.
  • #3634 upstreams Std.Data.Nat and #3635 upstreams Std.Data.Int.
  • #3790 reduces more imports for omega.
  • #3694 extends GetElem interface with getElem! and getElem? to simplify containers like RBMap.
  • #3865 renames Option.toMonad (see breaking changes below).
  • #3882 unifies lexOrd with compareLex.

• Other fixes or improvements

  • #3765 makes Quotient.sound be a theorem.
  • #3645 fixes System.FilePath.parent in the case of absolute paths.
  • #3660 ByteArray.toUInt64LE! and ByteArray.toUInt64BE! were swapped.
  • #3881, #3887 fix linearity issues in HashMap.insertIfNew, HashSet.erase, and HashMap.erase. The HashMap.insertIfNew fix improves import performance.
  • #3830 ensures linearity in Parsec.many*Core.
  • #3930 adds FS.Stream.isTty field.
  • #3866 deprecates Option.toBool in favor of Option.isSome.
  • #3975 upstreams Data.List.Init and Data.Array.Init material from Std.
  • #3942 adds instances that make ac_rfl work without Mathlib.
  • #4010 changes Fin.induction to use structural induction.
  • 02753f fixes bug in reduceLeDiff simproc.
  • #4097 adds IO.TaskState and IO.getTaskState to get the task from the Lean runtime's task manager.

• Docs: #3615, #3664, #3707, #3734, #3868, #3861, #3869, #3858, #3856, #3857, #3867, #3864, #3860, #3859, #3871, #3919.

Lean internals

• Defeq and WHNF algorithms
  • #3616 gives better support for reducing Nat.rec expressions.
  • #3774 add tracing for "non-easy" WHNF cases.
  • #3807 fixes an isDefEq performance issue, now trying structure eta after lazy delta reduction.
  • #3816 fixes .yesWithDeltaI behavior to prevent increasing transparency level when reducing projections.
  • #3837 improves heuristic at isDefEq.
  • #3965 improves isDefEq for constraints of the form t.i =?= s.i.
  • #3977 improves isDefEqProj.
  • #3981 adds universe constraint approximations to be able to solve u =?= max u ?v using ?v = u. These approximations are only applied when universe constraints cannot be postponed anymore.
  • #4004 improves isDefEqProj during typeclass resolution.
  • #4012 adds backward.isDefEq.lazyProjDelta and backward.isDefEq.lazyWhnfCore backwards compatibility flags.
• Kernel
  • #3966 removes dead code.
  • #4035 fixes mismatch for TheoremVal between Lean and C++.
• Discrimination trees
  • 423fed and 3218b2: simplify handling of dependent/non-dependent pi types.
• Typeclass instance synthesis
  • #3638 eta-reduces synthesized instances
  • ce350f fixes a linearity issue
  • 917a31 improves performance by considering at most one answer for subgoals not containing metavariables. #4008 adds backward.synthInstance.canonInstances backward compatibility flag.
• Definition processing
  • #3661, #3767 changes automatically generated equational theorems to be named using suffix .eq_<idx> instead of ._eq_<idx>, and .eq_def instead of ._unfold. (See breaking changes below.) #3675 adds a mechanism to reserve names. #3803 fixes reserved name resolution inside namespaces and fixes handling of matcher declarations and equation lemmas.
  • #3662 causes auxiliary definitions nested inside theorems to become defs if they are not proofs.
  • #4006 makes proposition fields of structures be theorems.
  • #4018 makes it an error for a theorem to be extern.
  • #4047 improves performance making equations for well-founded recursive definitions.
• Refactors
  • #3614 avoids unfolding in Lean.Meta.evalNat.
  • #3621 centralizes functionality for Fix/GuessLex/FunInd in the ArgsPacker module.
  • #3186 rewrites the UnusedVariable linter to be more performant.
  • #3589 removes coercion from String to Name (see breaking changes below).
  • #3237 removes the lines field from FileMap.
  • #3951 makes msg parameter to throwTacticEx optional.
• Diagnostics
  • #4016, #4019, #4020, #4030, #4031, c3714b, #4049 adds set_option diagnostics true for diagnostic counters. Tracks number of unfolded declarations, instances, reducible declarations, used instances, recursor reductions, isDefEq heuristic applications, among others. This option is suggested in exceptional situations, such as at deterministic timeout and maximum recursion depth.
  • 283587 adds diagnostic information for simp.
  • #4043 adds diagnostic information for congruence theorems.
  • #4048 display diagnostic information for set_option diagnostics true in <tactic> and set_option diagnostics true in <term>.
• Other features
  • #3800 adds environment extension to record which definitions use structural or well-founded recursion.
  • #3801 trace.profiler can now export to Firefox Profiler.
  • #3918, #3953 adds @[builtin_doc] attribute to make docs and location of a declaration available as a builtin.
  • #3939 adds the lean --json CLI option to print messages as JSON.
  • #3075 improves test_extern command.
  • #3970 gives monadic generalization of FindExpr.
• Docs: #3743, #3921, #3954.
• Other fixes: #3622, #3726, #3823, #3897, #3964, #3946, #4007, #4026.

Compiler, runtime, and FFI

• #3632 makes it possible to allocate and free thread-local runtime resources for threads not started by Lean itself.
• #3627 improves error message about compacting closures.
• #3692 fixes deadlock in IO.Promise.resolve.
• #3753 catches error code from MoveFileEx on Windows.
• #4028 fixes a double reset bug in ResetReuse transformation.
• 6e731b removes interpreter copy constructor to avoid potential memory safety issues.

Lake

• TOML Lake configurations. #3298, #4104.

  Lake packages can now use TOML as a alternative configuration file format instead of Lean. If the default lakefile.lean is missing, Lake will also look for a lakefile.toml. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.

  As part of the introduction of this new feature, we have been helping maintainers of some major packages within the ecosystem switch to this format. For example, the following is Aesop's new lakefile.toml:

  leanprover-community/aesop/lakefile.toml

  name = "aesop"
  defaultTargets = ["Aesop"]
  testRunner = "test"
  precompileModules = false
  
  [[require]]
  name = "batteries"
  git = "https://github.com/leanprover-community/batteries"
  rev = "main"
  
  [[lean_lib]]
  name = "Aesop"
  
  [[lean_lib]]
  name = "AesopTest"
  globs = ["AesopTest.+"]
  leanOptions = {linter.unusedVariables = false}
  
  [[lean_exe]]
  name = "test"
  srcDir = "scripts"
  

  To assist users who wish to transition their packages between configuration file formats, there is also a new lake translate-config command for migrating to/from TOML.

  Running lake translate-config toml will produce a lakefile.toml version of a package's lakefile.lean. Any configuration options unsupported by the TOML format will be discarded during translation, but the original lakefile.lean will remain so that you can verify the translation looks good before deleting it.

• Build progress overhaul. #3835, #4115, #4127, #4220, #4232, #4236.

  Builds are now managed by a top-level Lake build monitor, this makes the output of Lake builds more standardized and enables producing prettier and more configurable progress reports.

  As part of this change, job isolation has improved. Stray I/O and other build related errors in custom targets are now properly isolated and caught as part of their job. Import errors no longer cause Lake to abort the entire build and are instead localized to the build jobs of the modules in question.

  Lake also now uses ANSI escape sequences to add color and produce progress lines that update in-place; this can be toggled on and off using --ansi / --no-ansi.

  --wfail and --iofail options have been added that causes a build to fail if any of the jobs log a warning (--wfail) or produce any output or log information messages (--iofail). Unlike some other build systems, these options do NOT convert these logs into errors, and Lake does not abort jobs on such a log (i.e., dependent jobs will still continue unimpeded).

• lake test. #3779.

  Lake now has a built-in test command which will run a script or executable labelled @[test_runner] (in Lean) or defined as the testRunner (in TOML) in the root package.

  Lake also provides a lake check-test command which will exit with code 0 if the package has a properly configured test runner or error with 1 otherwise.

• lake lean. #3793.

  The new command lake lean <file> [-- <args...>] functions like lake env lean <file> <args...>, except that it builds the imports of file before running lean. This makes it very useful for running test or example code that imports modules that are not guaranteed to have been built beforehand.

• Miscellaneous bug fixes and improvements

  • #3609 LEAN_GITHASH environment variable to override the detected Git hash for Lean when computing traces, useful for testing custom builds of Lean.
  • #3795 improves relative package directory path normalization in the pre-rename check.
  • #3957 fixes handling of packages that appear multiple times in a dependency tree.
  • #3999 makes it an error for there to be a mismatch between a package name and what it is required as. Also adds a special message for the std-to-batteries rename.
  • #4033 fixes quiet mode.

• Docs: #3704.

DevOps

• #3536 and #3833 add a checklist for the release process.

• #3600 runs nix-ci more uniformly.

• #3612 avoids argument limits when building on Windows.

• #3682 builds Lean's .o files in parallel to rest of core.

• #3601 changes the way Lean is built on Windows (see breaking changes below). As a result, Lake now dynamically links executables with supportInterpreter := true on Windows to libleanshared.dll and libInit_shared.dll. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of PATH. Running the executable via lake exe will ensure these libraries are part of PATH.

  In a related change, the signature of the nativeFacets Lake configuration options has changed from a static Array to a function (shouldExport : Bool) → Array. See its docstring or Lake's README for further details on the changed option.

• #3690 marks "Build matrix complete" as canceled if the build is canceled.

• #3700, #3702, #3701, #3834, #3923: fixes and improvements for std and mathlib CI.

• #3712 fixes nix build . on macOS.

• #3717 replaces shell.nix in devShell with flake.nix.

• #3715 and #3790 add test result summaries.

• #3971 prevents stage0 changes via the merge queue.

• #3979 adds handling for changes-stage0 label.

• #3952 adds a script to summarize GitHub issues.

• 18a699 fixes asan linking

Breaking changes

• Due to the major Lake build refactor, code using the affected parts of the Lake API or relying on the previous output format of Lake builds is likely to have been broken. We have tried to minimize the breakages and, where possible, old definitions have been marked @[deprecated] with a reference to the new alternative.

• Executables configured with supportInterpreter := true on Windows should now be run via lake exe to function properly.

• Automatically generated equational theorems are now named using suffix .eq_<idx> instead of ._eq_<idx>, and .eq_def instead of ._unfold. Example:

def fact : Nat → Nat
  | 0 => 1
  | n+1 => (n+1) * fact n

theorem ex : fact 0 = 1 := by unfold fact; decide

#check fact.eq_1
-- fact.eq_1 : fact 0 = 1

#check fact.eq_2
-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n

#check fact.eq_def
/-
fact.eq_def :
  ∀ (x : Nat),
    fact x =
      match x with
      | 0 => 1
      | Nat.succ n => (n + 1) * fact n
-/

• The coercion from String to Name was removed. Previously, it was Name.mkSimple, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to Name.mkSimple.

• The Subarray fields as, h₁ and h₂ have been renamed to array, start_le_stop, and stop_le_array_size, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.

• The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.

• Option.toMonad has been renamed to Option.getM and the unneeded [Monad m] instance argument has been removed.

v4.7.0

• simp and rw now use instance arguments found by unification, rather than always resynthesizing. For backwards compatibility, the original behaviour is available via set_option tactic.skipAssignedInstances false. #3507 and #3509.

• When the pp.proofs is false, now omitted proofs use ⋯ rather than _, which gives a more helpful error message when copied from the Infoview. The pp.proofs.threshold option lets small proofs always be pretty printed. #3241.

• pp.proofs.withType is now set to false by default to reduce noise in the info view.

• The pretty printer for applications now handles the case of over-application itself when applying app unexpanders. In particular, the | `($_ $a $b $xs*) => `(($a + $b) $xs*) case of an app_unexpander is no longer necessary. #3495.

• New simp (and dsimp) configuration option: zetaDelta. It is false by default. The zeta option is still true by default, but their meaning has changed.

  • When zeta := true, simp and dsimp reduce terms of the form let x := val; e[x] into e[val].
  • When zetaDelta := true, simp and dsimp will expand let-variables in the context. For example, suppose the context contains x := val. Then, any occurrence of x is replaced with val.

  See issue #2682 for additional details. Here are some examples:

  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
    intro x
    simp
    /-
    New goal:
    h : z = 9; x := 5 |- x + 4 = z
    -/
    rw [h]
  
  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
    intro x
    -- Using both `zeta` and `zetaDelta`.
    simp (config := { zetaDelta := true })
    /-
    New goal:
    h : z = 9; x := 5 |- 9 = z
    -/
    rw [h]
  
  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
    intro x
    simp [x] -- asks `simp` to unfold `x`
    /-
    New goal:
    h : z = 9; x := 5 |- 9 = z
    -/
    rw [h]
  
  example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
    intro x
    simp (config := { zetaDelta := true, zeta := false })
    /-
    New goal:
    h : z = 9; x := 5 |- let y := 4; 5 + y = z
    -/
    rw [h]
  

• When adding new local theorems to simp, the system assumes that the function application arguments have been annotated with no_index. This modification, which addresses issue #2670, restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:

  example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
    (a : α) (b : β) : f (a, b) b = b := by
    simp [h]
  
  example {α β : Type} {f : α × β → β → β}
    (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
    simp [h]
  

  In both cases, h is applicable because simp does not index f-arguments anymore when adding h to the simp-set. It's important to note, however, that global theorems continue to be indexed in the usual manner.

• Improved the error messages produced by the decide tactic. #3422

• Improved auto-completion performance. #3460

• Improved initial language server startup performance. #3552

• Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. #3482

• There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. #3413

• You can now write termination_by? after a declaration to see the automatically inferred termination argument, and turn it into a termination_by … clause using the “Try this” widget or a code action. #3514

• A large fraction of Std has been moved into the Lean repository. This was motivated by:

  1. Making universally useful tactics such as ext, by_cases, change at, norm_cast, rcases, simpa, simp?, omega, and exact? available to all users of Lean, without imports.
  2. Minimizing the syntactic changes between plain Lean and Lean with import Std.
  3. Simplifying the development process for the basic data types Nat, Int, Fin (and variants such as UInt64), List, Array, and BitVec as we begin making the APIs and simp normal forms for these types more complete and consistent.
  4. Laying the groundwork for the Std roadmap, as a library focused on essential datatypes not provided by the core language (e.g. RBMap) and utilities such as basic IO. While we have achieved most of our initial aims in v4.7.0-rc1, some upstreaming will continue over the coming months.

• The / and % notations in Int now use Int.ediv and Int.emod (i.e. the rounding conventions have changed). Previously Std overrode these notations, so this is no change for users of Std. There is now kernel support for these functions. #3376.

• omega, our integer linear arithmetic tactic, is now available in the core language.

  • It is supplemented by a preprocessing tactic bv_omega which can solve goals about BitVec which naturally translate into linear arithmetic problems. #3435.
  • omega now has support for Fin #3427, the <<< operator #3433.
  • During the port omega was modified to no longer identify atoms up to definitional equality (so in particular it can no longer prove id x ≤ x). #3525. This may cause some regressions. We plan to provide a general purpose preprocessing tactic later, or an omega! mode.
  • omega is now invoked in Lean's automation for termination proofs #3503 as well as in array indexing proofs #3515. This automation will be substantially revised in the medium term, and while omega does help automate some proofs, we plan to make this much more robust.

• The library search tactics exact? and apply? that were originally in Mathlib are now available in Lean itself. These use the implementation using lazy discrimination trees from Std, and thus do not require a disk cache but have a slightly longer startup time. The order used for selection lemmas has changed as well to favor goals purely based on how many terms in the head pattern match the current goal.

• The solve_by_elim tactic has been ported from Std to Lean so that library search can use it.

• New #check_tactic and #check_simp commands have been added. These are useful for checking tactics (particularly simp) behave as expected in test suites.

• Previously, app unexpanders would only be applied to entire applications. However, some notations produce functions, and these functions can be given additional arguments. The solution so far has been to write app unexpanders so that they can take an arbitrary number of additional arguments. However this leads to misleading hover information in the Infoview. For example, while HAdd.hAdd f g 1 pretty prints as (f + g) 1, hovering over f + g shows f. There is no way to fix the situation from within an app unexpander; the expression position for HAdd.hAdd f g is absent, and app unexpanders cannot register TermInfo.

  This commit changes the app delaborator to try running app unexpanders on every prefix of an application, from longest to shortest prefix. For efficiency, it is careful to only try this when app delaborators do in fact exist for the head constant, and it also ensures arguments are only delaborated once. Then, in (f + g) 1, the f + g gets TermInfo registered for that subexpression, making it properly hoverable.

  #3375

Breaking changes:

• Lean.withTraceNode and variants got a stronger MonadAlwaysExcept assumption to fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration monads built on EIO Exception should be synthesized automatically.
• The match ... with. and fun. notations previously in Std have been replaced by nomatch ... and nofun. #3279 and #3286

Other improvements:

• several bug fixes for simp:
  • we should not crash when simp loops #3269
  • simp gets stuck on autoParam #3315
  • simp fails when custom discharger makes no progress #3317
  • simp fails to discharge autoParam premises even when it can reduce them to True #3314
  • simp? suggests generated equations lemma names, fixes #3547 #3573
• fixes for match expressions:
  • fix regression with builtin literals #3521
  • accept match when patterns cover all cases of a BitVec finite type #3538
  • fix matching Int literals #3504
  • patterns containing int values and constructors #3496
• improve termination_by error messages #3255
• fix rename_i in macros, fixes #3553 #3581
• fix excessive resource usage in generalize, fixes #3524 #3575
• an equation lemma with autoParam arguments fails to rewrite, fixing #2243 #3316
• add_decl_doc should check that declarations are local #3311
• instantiate the types of inductives with the right parameters, closing #3242 #3246
• New simprocs for many basic types. #3407

Lake fixes:

• Warn on fetch cloud release failure #3401
• Cloud release trace & lake build :release errors #3248

v4.6.1

• Backport of #3552 fixing a performance regression in server startup.

v4.6.0

• Add custom simplification procedures (aka simprocs) to simp. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example:

  import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
  
  def foo (x : Nat) : Nat :=
    x + 10
  
  /--
  The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
  -/
  simproc reduceFoo (foo _) :=
    /- A term of type `Expr → SimpM Step -/
    fun e => do
      /-
      The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
      * The constructor `.done` instructs `simp` that the result does
        not need to be simplified further.
      * The constructor `.visit` instructs `simp` to visit the resulting expression.
      * The constructor `.continue` instructs `simp` to try other simplification procedures.
  
      All three constructors take a `Result`. The `.continue` constructor may also take `none`.
      `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
       If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
      -/
      /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
      unless e.isAppOfArity ``foo 1 do
        return .continue
      /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
      let some n ← Nat.fromExpr? e.appArg!
        | return .continue
      return .done { expr := Lean.mkNatLit (n+10) }
  

  We disable simprocs support by using the command set_option simprocs false. This command is particularly useful when porting files to v4.6.0. Simprocs can be scoped, manually added to simp commands, and suppressed using -. They are also supported by simp?. simp only does not execute any simproc. Here are some examples for the simproc defined above.

  example : x + foo 2 = 12 + x := by
    set_option simprocs false in
      /- This `simp` command does not make progress since `simproc`s are disabled. -/
      fail_if_success simp
    simp_arith
  
  example : x + foo 2 = 12 + x := by
    /- `simp only` must not use the default simproc set. -/
    fail_if_success simp only
    simp_arith
  
  example : x + foo 2 = 12 + x := by
    /-
    `simp only` does not use the default simproc set,
    but we can provide simprocs as arguments. -/
    simp only [reduceFoo]
    simp_arith
  
  example : x + foo 2 = 12 + x := by
    /- We can use `-` to disable `simproc`s. -/
    fail_if_success simp [-reduceFoo]
    simp_arith
  

  The command register_simp_attr <id> now creates a simp and a simproc set with the name <id>. The following command instructs Lean to insert the reduceFoo simplification procedure into the set my_simp. If no set is specified, Lean uses the default simp set.

  simproc [my_simp] reduceFoo (foo _) := ...
  

• The syntax of the termination_by and decreasing_by termination hints is overhauled:

  • They are now placed directly after the function they apply to, instead of after the whole mutual block.
  • Therefore, the function name no longer has to be mentioned in the hint.
  • If the function has a where clause, the termination_by and decreasing_by for that function come before the where. The functions in the where clause can have their own termination hints, each following the corresponding definition.
  • The termination_by clause can only bind “extra parameters”, that are not already bound by the function header, but are bound in a lambda (:= fun x y z =>) or in patterns (| x, n + 1 => …). These extra parameters used to be understood as a suffix of the function parameters; now it is a prefix.

  Migration guide: In simple cases just remove the function name, and any variables already bound at the header.

   def foo : Nat → Nat → Nat := …
  -termination_by foo a b => a - b
  +termination_by a b => a - b
  

  or

   def foo : Nat → Nat → Nat := …
  -termination_by _ a b => a - b
  +termination_by a b => a - b
  

  If the parameters are bound in the function header (before the :), remove them as well:

   def foo (a b : Nat) : Nat := …
  -termination_by foo a b => a - b
  +termination_by a - b
  

  Else, if there are multiple extra parameters, make sure to refer to the right ones; the bound variables are interpreted from left to right, no longer from right to left:

   def foo : Nat → Nat → Nat → Nat
     | a, b, c => …
  -termination_by foo b c => b
  +termination_by a b => b
  

  In the case of a mutual block, place the termination arguments (without the function name) next to the function definition:

  -mutual
  -def foo : Nat → Nat → Nat := …
  -def bar : Nat → Nat := …
  -end
  -termination_by
  -  foo a b => a - b
  -  bar a => a
  +mutual
  +def foo : Nat → Nat → Nat := …
  +termination_by a b => a - b
  +def bar : Nat → Nat := …
  +termination_by a => a
  +end
  

  Similarly, if you have (mutual) recursion through where or let rec, the termination hints are now placed directly after the function they apply to:

  -def foo (a b : Nat) : Nat := …
  -  where bar (x : Nat) : Nat := …
  -termination_by
  -  foo a b => a - b
  -  bar x => x
  +def foo (a b : Nat) : Nat := …
  +termination_by a - b
  +  where
  +    bar (x : Nat) : Nat := …
  +    termination_by x
  
  -def foo (a b : Nat) : Nat :=
  -  let rec bar (x : Nat) :  Nat := …
  -  …
  -termination_by
  -  foo a b => a - b
  -  bar x => x
  +def foo (a b : Nat) : Nat :=
  +  let rec bar (x : Nat) : Nat := …
  +    termination_by x
  +  …
  +termination_by a - b
  

  In cases where a single decreasing_by clause applied to multiple mutually recursive functions before, the tactic now has to be duplicated.

• The semantics of decreasing_by changed; the tactic is applied to all termination proof goals together, not individually.

  This helps when writing termination proofs interactively, as one can focus each subgoal individually, for example using ·. Previously, the given tactic script had to work for all goals, and one had to resort to tactic combinators like first:

   def foo (n : Nat) := … foo e1 … foo e2 …
  -decreasing_by
  -simp_wf
  -first | apply something_about_e1; …
  -      | apply something_about_e2; …
  +decreasing_by
  +all_goals simp_wf
  +· apply something_about_e1; …
  +· apply something_about_e2; …
  

  To obtain the old behaviour of applying a tactic to each goal individually, use all_goals:

   def foo (n : Nat) := …
  -decreasing_by some_tactic
  +decreasing_by all_goals some_tactic
  

  In the case of mutual recursion each decreasing_by now applies to just its function. If some functions in a recursive group do not have their own decreasing_by, the default decreasing_tactic is used. If the same tactic ought to be applied to multiple functions, the decreasing_by clause has to be repeated at each of these functions.

• Modify InfoTree.context to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the InfoTree manually instead of going through the functions in InfoUtils.lean, as well as those manually creating and saving InfoTrees. See PR #3159 for how to migrate your code.

• Add language server support for call hierarchy requests (PR #3082). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.

• Structure instances with multiple sources (for example {a, b, c with x := 0}) now have their fields filled from these sources in strict left-to-right order. Furthermore, the structure instance elaborator now aggressively use sources to fill in subobject fields, which prevents unnecessary eta expansion of the sources, and hence greatly reduces the reliance on costly structure eta reduction. This has a large impact on mathlib, reducing total CPU instructions by 3% and enabling impactful refactors like leanprover-community/mathlib4#8386 which reduces the build time by almost 20%. See PR #2478 and RFC #2451.

• Add pretty printer settings to omit deeply nested terms (pp.deepTerms false and pp.deepTerms.threshold) (PR #3201)

• Add pretty printer options pp.numeralTypes and pp.natLit. When pp.numeralTypes is true, then natural number literals, integer literals, and rational number literals are pretty printed with type ascriptions, such as (2 : Rat), (-2 : Rat), and (-2 / 3 : Rat). When pp.natLit is true, then raw natural number literals are pretty printed as nat_lit 2. PR #2933 and RFC #3021.

Lake updates:

• improved platform information & control #3226
• lake update from unsupported manifest versions #3149

Other improvements:

• make intro be aware of let_fun #3115
• produce simpler proof terms in rw #3121
• fuse nested mkCongrArg calls in proofs generated by simp #3203
• induction using followed by a general term #3188
• allow generalization in let #3060, fixing #3065
• reducing out-of-bounds swap! should return a, not `default`` #3197, fixing #3196
• derive BEq on structure with Prop-fields #3191, fixing #3140
• refine through more casesOnApp/matcherApp #3176, fixing #3175
• do not strip dotted components from lean module names #2994, fixing #2999
• fix deriving only deriving the first declaration for some handlers #3058, fixing #3057
• do not instantiate metavariables in kabstract/rw for disallowed occurrences #2539, fixing #2538
• hover info for cases h : ... #3084

v4.5.0

• Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form "\" newline whitespace*. These have the interpretation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace. The following is equivalent to "this is a string".

  "this is \
     a string"
  

  PR #2821 and RFC #2838.

• Add raw string literal syntax. For example, r"\n" is equivalent to "\\n", with no escape processing. To include double quote characters in a raw string one can add sufficiently many # characters before and after the bounding "s, as in r#"the "the" is in quotes"# for "the \"the\" is in quotes". PR #2929 and issue #1422.

• The low-level termination_by' clause is no longer supported.

  Migration guide: Use termination_by instead, e.g.:

  -termination_by' measure (fun ⟨i, _⟩ => as.size - i)
  +termination_by i _ => as.size - i
  

  If the well-founded relation you want to use is not the one that the WellFoundedRelation type class would infer for your termination argument, you can use WellFounded.wrap from the std library to explicitly give one:

  -termination_by' ⟨r, hwf⟩
  +termination_by x => hwf.wrap x
  

• Support snippet edits in LSP TextEdits. See Lean.Lsp.SnippetString for more details.

• Deprecations and changes in the widget API.

  • Widget.UserWidgetDefinition is deprecated in favour of Widget.Module. The annotation @[widget] is deprecated in favour of @[widget_module]. To migrate a definition of type UserWidgetDefinition, remove the name field and replace the type with Widget.Module. Removing the name results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using <details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>. See an example migration here.
  • The new command show_panel_widgets allows displaying always-on and locally-on panel widgets.
  • RpcEncodable widget props can now be stored in the infotree.
  • See RFC 2963 for more details and motivation.

• If no usable lexicographic order can be found automatically for a termination proof, explain why. See feat: GuessLex: if no measure is found, explain why.

• Option to print inferred termination argument. With set_option showInferredTerminationBy true you will get messages like

  Inferred termination argument:
  termination_by
  ackermann n m => (sizeOf n, sizeOf m)
  

  for automatically generated termination_by clauses.

• More detailed error messages for invalid mutual blocks.

• Multiple improvements to the output of simp? and simp_all?.

• Tactics with withLocation * no longer fail if they close the main goal.

• Implementation of a test_extern command for writing tests for @[extern] and @[implemented_by] functions. Usage is

  import Lean.Util.TestExtern
  
  test_extern Nat.add 17 37
  

  The head symbol must be the constant with the @[extern] or @[implemented_by] attribute. The return type must have a DecidableEq instance.

Bug fixes for #2853, #2953, #2966, #2971, #2990, #3094.

Bug fix for eager evaluation of default value in Option.getD. Avoid panic in leanPosToLspPos when file source is unavailable. Improve short-circuiting behavior for List.all and List.any.

Several Lake bug fixes: #3036, #3064, #3069.

v4.4.0

• Lake and the language server now support per-package server options using the moreServerOptions config field, as well as options that apply to both the language server and lean using the leanOptions config field. Setting either of these fields instead of moreServerArgs ensures that viewing files from a dependency uses the options for that dependency. Additionally, moreServerArgs is being deprecated in favor of the moreGlobalServerArgs field. See PR #2858.

  A Lakefile with the following deprecated package declaration:

  def moreServerArgs := #[
    "-Dpp.unicode.fun=true"
  ]
  def moreLeanArgs := moreServerArgs
  
  package SomePackage where
    moreServerArgs := moreServerArgs
    moreLeanArgs := moreLeanArgs
  

  ... can be updated to the following package declaration to use per-package options:

  package SomePackage where
    leanOptions := #[⟨`pp.unicode.fun, true⟩]
  

• Rename request handler.

• Import auto-completion.

• `pp.beta`` to apply beta reduction when pretty printing.

• Embed and check githash in .olean.

• Guess lexicographic order for well-founded recursion.

• Allow trailing comma in tuples, lists, and tactics.

Bug fixes for #2628, #2883, #2810, #2925, and #2914.

Lake:

• lake init . and a bare lake init and will now use the current directory as the package name. #2890
• lake new and lake init will now produce errors on invalid package names such as .., foo/bar, Init, Lean, Lake, and Main. See issue #2637 and PR #2890.
• lean_lib no longer converts its name to upper camel case (e.g., lean_lib bar will include modules named bar.* rather than Bar.*). See issue #2567 and PR #2889.
• Lean and Lake now properly support non-identifier library names (e.g., lake new 123-hello and import «123Hello» now work correctly). See issue #2865 and PR #2889.
• Lake now filters the environment extensions loaded from a compiled configuration (lakefile.olean) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via elab in configurations). See issue #2632 and PR #2896.
• Cloud releases will now properly be re-unpacked if the build directory is removed. See PR #2928.
• Lake's math template has been simplified. See PR #2930.
• lake exe <target> now parses target like a build target (as the help text states it should) rather than as a basic name. For example, lake exe @mathlib/runLinter should now work. See PR #2932.
• lake new foo.bar [std] now generates executables named foo-bar and lake new foo.bar exe properly creates foo/bar.lean. See PR #2932.
• Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue #2548 and PR #2937.
• Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by findModule?. See PR #2937.

v4.3.0

• simp [f] does not unfold partial applications of f anymore. See issue #2042. To fix proofs affected by this change, use unfold f or simp (config := { unfoldPartialApp := true }) [f].

• By default, simp will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by simp, and the decide tactic may be useful in such cases. The decide simp configuration option can be used to locally restore the old simp behavior, as in simp (config := {decide := true}); this includes using Decidable instances to verify side goals such as numeric inequalities.

• Many bug fixes:

  • Add left/right actions to term tree coercion elaborator and make `^`` a right action
  • Fix for #2775, don't catch max recursion depth errors
  • Reduction of Decidable instances very slow when using cases tactic
  • simp not rewriting in binder
  • simp unfolding let even with zeta := false option
  • simp (with beta/zeta disabled) and discrimination trees
  • unknown free variable introduced by rw ... at h
  • dsimp doesn't use rfl theorems which consist of an unapplied constant
  • dsimp does not close reflexive equality goals if they are wrapped in metadata
  • rw [h] uses h from the environment in preference to h from the local context
  • missing withAssignableSyntheticOpaque for assumption tactic
  • ignoring default value for field warning

• Cancel outstanding tasks on document edit in the language server.

• Remove unnecessary % operations in Fin.mod and Fin.div

• Avoid DecidableEq in Array.mem

• Ensure USize.size unifies with ?m + 1

• Improve compatibility with emacs eglot client

Lake:

• Sensible defaults for lake new MyProject math
• Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.
• A manifest is automatically created on workspace load if one does not exists..
• The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.
• support for overriding package URLs via LAKE_PKG_URL_MAP
• Moved the default build directory (e.g., build), default packages directory (e.g., lake-packages), and the compiled configuration (e.g., lakefile.olean) into a new dedicated directory for Lake outputs, .lake. The cloud release build archives are also stored here, fixing #2713.
• Update manifest format to version 7 (see lean4#2801 for details on the changes).
• Deprecate the manifestFile field of a package configuration.
• There is now a more rigorous check on lakefile.olean compatibility (see #2842 for more details).

v4.2.0

• isDefEq cache for terms not containing metavariables..
• Make Environment.mk and Environment.add private, and add replay as a safer alternative.
• IO.Process.output no longer inherits the standard input of the caller.
• Do not inhibit caching of default-level match reduction.
• List the valid case tags when the user writes an invalid one.
• The derive handler for DecidableEq now handles mutual inductive types.
• Show path of failed import in Lake.
• Fix linker warnings on macOS.
• Lake: Add postUpdate? package configuration option. Used by a package to specify some code which should be run after a successful lake update of the package or one of its downstream dependencies. (lake#185)
• Improvements to Lake startup time (#2572, #2573)
• refine e now replaces the main goal with metavariables which were created during elaboration of e and no longer captures pre-existing metavariables that occur in e (#2502).
  • This is accomplished via changes to withCollectingNewGoalsFrom, which also affects elabTermWithHoles, refine', calc (tactic), and specialize. Likewise, all of these now only include newly-created metavariables in their output.
  • Previously, both newly-created and pre-existing metavariables occurring in e were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue #2495), erroneously closed goals (issue #2434), and unintuitive behavior due to refine e capturing previously-created goals appearing unexpectedly in e (no issue; see PR).

v4.1.0

• The error positioning on missing tokens has been improved. In particular, this should make it easier to spot errors in incomplete tactic proofs.

• After elaborating a configuration file, Lake will now cache the configuration to a lakefile.olean. Subsequent runs of Lake will import this OLean instead of elaborating the configuration file. This provides a significant performance improvement (benchmarks indicate that using the OLean cuts Lake's startup time in half), but there are some important details to keep in mind:

  • Lake will regenerate this OLean after each modification to the lakefile.lean or lean-toolchain. You can also force a reconfigure by passing the new --reconfigure / -R option to lake.
  • Lake configuration options (i.e., -K) will be fixed at the moment of elaboration. Setting these options when lake is using the cached configuration will have no effect. To change options, run lake with -R / --reconfigure.
  • The lakefile.olean is a local configuration and should not be committed to Git. Therefore, existing Lake packages need to add it to their .gitignore.

• The signature of Lake.buildO has changed, args has been split into weakArgs and traceArgs. traceArgs are included in the input trace and weakArgs are not. See Lake's FFI example for a demonstration of how to adapt to this change.

• The signatures of Lean.importModules, Lean.Elab.headerToImports, and Lean.Elab.parseImports have changed from taking List Import to Array Import.

• There is now an occs field in the configuration object for the rewrite tactic, allowing control of which occurrences of a pattern should be rewritten. This was previously a separate argument for Lean.MVarId.rewrite, and this has been removed in favour of an additional field of Rewrite.Config. It was not previously accessible from user tactics.

v4.0.0

• Lean.Meta.getConst? has been renamed. We have renamed getConst? to getUnfoldableConst? (and getConstNoEx? to getUnfoldableConstNoEx?). These were not intended to be part of the public API, but downstream projects had been using them (sometimes expecting different behaviour) incorrectly instead of Lean.getConstInfo.

• dsimp / simp / simp_all now fail by default if they make no progress.

  This can be overridden with the (config := { failIfUnchanged := false }) option. This change was made to ease manual use of simp (with complicated goals it can be hard to tell if it was effective) and to allow easier flow control in tactics internally using simp. See the summary discussion on zulip for more details.

• simp_all now preserves order of hypotheses.

  In order to support the failIfUnchanged configuration option for dsimp / simp / simp_all the way simp_all replaces hypotheses has changed. In particular it is now more likely to preserve the order of hypotheses. See simp_all reorders hypotheses unnecessarily. (Previously all non-dependent propositional hypotheses were reverted and reintroduced. Now only such hypotheses which were changed, or which come after a changed hypothesis, are reverted and reintroduced. This has the effect of preserving the ordering amongst the non-dependent propositional hypotheses, but now any dependent or non-propositional hypotheses retain their position amongst the unchanged non-dependent propositional hypotheses.) This may affect proofs that use rename_i, case ... =>, or next ... =>.

• New have this implementation.

  this is now a regular identifier again that is implicitly introduced by anonymous have := for the remainder of the tactic block. It used to be a keyword that was visible in all scopes and led to unexpected behavior when explicitly used as a binder name.

• Show typeclass and tactic names in profile output.

• Make calc require the sequence of relation/proof-s to have the same indentation, and add calc alternative syntax allowing underscores _ in the first relation.

  The flexible indentation in calc was often used to align the relation symbols:

  example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
    calc
        (x + y) * (x + y) = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
                        -- improper indentation
                        _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
                        _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
                        _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]
  

  This is no longer legal. The new syntax puts the first term right after the calc and each step has the same indentation:

  example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
    calc (x + y) * (x + y)
      _ = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
      _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
      _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
      _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]
  

• Update Lake to latest prerelease.

• Make go-to-definition on a typeclass projection application go to the instance(s).

• Include timings in trace messages when profiler is true.

• Pretty-print signatures in hover and #check <ident>.

• Introduce parser memoization to avoid exponential behavior.

• feat: allow doSeq in let x <- e | seq.

• Add hover/go-to-def/refs for options.

• Add empty type ascription syntax (e :).

• Make tokens in <|> relevant to syntax match.

• Add linter.deprecated option to silence deprecation warnings.

• Improve fuzzy-matching heuristics.

• Implementation-detail hypotheses.

• Hover information for cases/induction case names.

• Prefer longer parse even if unsuccessful.

• Show declaration module in hover.

• New conv mode structuring tactics.

• simp can track information and can print an equivalent simp only. PR #1626.

• Enforce uniform indentation in tactic blocks / do blocks. See issue #1606.

• Moved AssocList, HashMap, HashSet, RBMap, RBSet, PersistentArray, PersistentHashMap, PersistentHashSet to the Lean package. The standard library contains versions that will evolve independently to simplify bootstrapping process.

• Standard library moved to the std4 GitHub repository.

• InteractiveGoals now has information that a client infoview can use to show what parts of the goal have changed after applying a tactic. PR #1610.

• Add [inheritDoc] attribute. PR #1480.

• Expose that panic = default. PR #1614.

• New code generator project has started.

• Remove description argument from register_simp_attr. PR #1566.

• Additional concurrency primitives.

• Collapsible traces with messages.

• Hygienic resolution of namespaces.

• New Float functions.

• Many new doc strings have been added to declarations at Init.

v4.0.0-m5 (07 August 2022)

• Update Lake to v4.0.0. See the v4.0.0 release notes for detailed changes.

• Mutual declarations in different namespaces are now supported. Example:

  mutual
    def Foo.boo (x : Nat) :=
      match x with
      | 0 => 1
      | x + 1 => 2*Boo.bla x
  
    def Boo.bla (x : Nat) :=
      match x with
      | 0 => 2
      | x+1 => 3*Foo.boo x
  end
  

  A namespace is automatically created for the common prefix. Example:

  mutual
    def Tst.Foo.boo (x : Nat) := ...
    def Tst.Boo.bla (x : Nat) := ...
  end
  

  expands to

  namespace Tst
  mutual
    def Foo.boo (x : Nat) := ...
    def Boo.bla (x : Nat) := ...
  end
  end Tst
  

• Allow users to install their own deriving handlers for existing type classes. See example at Simple.lean.

• Add tactic congr (num)?. See doc string for additional details.

• Missing doc linter

• match-syntax notation now checks for unused alternatives. See issue #1371.

• Auto-completion for structure instance fields. Example:

  example : Nat × Nat := {
    f -- HERE
  }
  

  fst now appears in the list of auto-completion suggestions.

• Auto-completion for dotted identifier notation. Example:

  example : Nat :=
    .su -- HERE
  

  succ now appears in the list of auto-completion suggestions.

• nat_lit is not needed anymore when declaring OfNat instances. See issues #1389 and #875. Example:

  inductive Bit where
    | zero
    | one
  
  instance inst0 : OfNat Bit 0 where
    ofNat := Bit.zero
  
  instance : OfNat Bit 1 where
    ofNat := Bit.one
  
  example : Bit := 0
  example : Bit := 1
  

• Add [elabAsElim] attribute (it is called elab_as_eliminator in Lean 3). Motivation: simplify the Mathlib port to Lean 4.

• Trans type class now accepts relations in Type u. See this Zulip issue.

• Accept unescaped keywords as inductive constructor names. Escaping can often be avoided at use sites via dot notation.

  inductive MyExpr
    | let : ...
  
  def f : MyExpr → MyExpr
    | .let ... => .let ...
  

• Throw an error message at parametric local instances such as [Nat -> Decidable p]. The type class resolution procedure cannot use this kind of local instance because the parameter does not have a forward dependency. This check can be disabled using set_option checkBinderAnnotations false.

• Add option pp.showLetValues. When set to false, the info view hides the value of let-variables in a goal. By default, it is true when visualizing tactic goals, and false otherwise. See issue #1345 for additional details.

• Add option warningAsError. When set to true, warning messages are treated as errors.

• Support dotted notation and named arguments in patterns. Example:

  def getForallBinderType (e : Expr) : Expr :=
    match e with
    | .forallE (binderType := type) .. => type
    | _ => panic! "forall expected"
  

• "jump-to-definition" now works for function names embedded in the following attributes @[implementedBy funName], @[tactic parserName], @[termElab parserName], @[commandElab parserName], @[builtinTactic parserName], @[builtinTermElab parserName], and @[builtinCommandElab parserName]. See issue #1350.

• Improve MVarId methods discoverability. See issue #1346. We still have to add similar methods for FVarId, LVarId, Expr, and other objects. Many existing methods have been marked as deprecated.

• Add attribute [deprecated] for marking deprecated declarations. Examples:

  def g (x : Nat) := x + 1
  
  -- Whenever `f` is used, a warning message is generated suggesting to use `g` instead.
  @[deprecated g]
  def f (x : Nat) := x + 1
  
  #check f 0 -- warning: `f` has been deprecated, use `g` instead
  
  -- Whenever `h` is used, a warning message is generated.
  @[deprecated]
  def h (x : Nat) := x + 1
  
  #check h 0 -- warning: `h` has been deprecated
  

• Add type LevelMVarId (and abbreviation LMVarId) for universe level metavariable ids. Motivation: prevent meta-programmers from mixing up universe and expression metavariable ids.

• Improve calc term and tactic. See issue #1342.

• Relaxed antiquotation parsing further reduces the need for explicit $x:p antiquotation kind annotations.

• Add support for computed fields in inductives. Example:

  inductive Exp
    | var (i : Nat)
    | app (a b : Exp)
  with
    @[computedField] hash : Exp → Nat
      | .var i => i
      | .app a b => a.hash * b.hash + 1
  

  The result of the Exp.hash function is then stored as an extra "computed" field in the .var and .app constructors; Exp.hash accesses this field and thus runs in constant time (even on dag-like values).

• Update a[i] notation. It is now based on the typeclass

  class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
    getElem (xs : cont) (i : idx) (h : dom xs i) : Elem
  

  The notation a[i] is now defined as follows

  macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
  

  The proof that i is a valid index is synthesized using the tactic get_elem_tactic. For example, the type Array α has the following instances

  instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where ...
  instance : GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where ...
  

  You can use the notation a[i]'h to provide the proof manually. Two other notations were introduced: a[i]! and a[i]?, For a[i]!, a panic error message is produced at runtime if i is not a valid index. a[i]? has type Option α, and a[i]? evaluates to none if the index i is not valid. The three new notations are defined as follows:

  @[inline] def getElem' [GetElem cont idx elem dom] (xs : cont) (i : idx) (h : dom xs i) : elem :=
  getElem xs i h
  
  @[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
    if h : _ then getElem xs i h else panic! "index out of bounds"
  
  @[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
    if h : _ then some (getElem xs i h) else none
  
  macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
  macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
  macro x:term noWs "[" i:term "]'" h:term:max : term => `(getElem' $x $i $h)
  

  See discussion on Zulip. Examples:

  example (a : Array Int) (i : Nat) : Int :=
    a[i] -- Error: failed to prove index is valid ...
  
  example (a : Array Int) (i : Nat) (h : i < a.size) : Int :=
    a[i] -- Ok
  
  example (a : Array Int) (i : Nat) : Int :=
    a[i]! -- Ok
  
  example (a : Array Int) (i : Nat) : Option Int :=
    a[i]? -- Ok
  
  example (a : Array Int) (h : a.size = 2) : Int :=
    a[0]'(by rw [h]; decide) -- Ok
  
  example (a : Array Int) (h : a.size = 2) : Int :=
    have : 0 < a.size := by rw [h]; decide
    have : 1 < a.size := by rw [h]; decide
    a[0] + a[1] -- Ok
  
  example (a : Array Int) (i : USize) (h : i.toNat < a.size) : Int :=
    a[i] -- Ok
  

  The get_elem_tactic is defined as

  macro "get_elem_tactic" : tactic =>
    `(first
      | get_elem_tactic_trivial
      | fail "failed to prove index is valid, ..."
     )
  

  The get_elem_tactic_trivial auxiliary tactic can be extended using macro_rules. By default, it tries trivial, simp_arith, and a special case for Fin. In the future, it will also try linarith. You can extend get_elem_tactic_trivial using my_tactic as follows

  macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| my_tactic)
  

  Note that Idx's type in GetElem does not depend on Cont. So, you cannot write the instance instance : GetElem (Array α) (Fin ??) α fun xs i => ..., but the Lean library comes equipped with the following auxiliary instance:

  instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
    getElem xs i h := getElem xs i.1 h
  

  and helper tactic

  macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
  

  Example:

  example (a : Array Nat) (i : Fin a.size) :=
    a[i] -- Ok
  
  example (a : Array Nat) (h : n ≤ a.size) (i : Fin n) :=
    a[i] -- Ok
  

• Better support for qualified names in recursive declarations. The following is now supported:

  namespace Nat
    def fact : Nat → Nat
    | 0 => 1
    | n+1 => (n+1) * Nat.fact n
  end Nat
  

• Add support for CommandElabM monad at #eval. Example:

  import Lean
  
  open Lean Elab Command
  
  #eval do
    let id := mkIdent `foo
    elabCommand (← `(def $id := 10))
  
  #eval foo -- 10
  

• Try to elaborate do notation even if the expected type is not available. We still delay elaboration when the expected type is not available. This change is particularly useful when writing examples such as

  #eval do
    IO.println "hello"
    IO.println "world"
  

  That is, we don't have to use the idiom #eval show IO _ from do ... anymore. Note that auto monadic lifting is less effective when the expected type is not available. Monadic polymorphic functions (e.g., ST.Ref.get) also require the expected type.

• On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable LEAN_BACKTRACE to 0. Other platforms are TBD.

• The group(·) syntax combinator is now introduced automatically where necessary, such as when using multiple parsers inside (...)+.

• Add "Typed Macros": syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit :kind antiquotation annotations. See PR for details.

• Aliases of protected definitions are protected too. Example:

  protected def Nat.double (x : Nat) := 2*x
  
  namespace Ex
  export Nat (double) -- Add alias Ex.double for Nat.double
  end Ex
  
  open Ex
  #check Ex.double -- Ok
  #check double -- Error, `Ex.double` is alias for `Nat.double` which is protected
  

• Use IO.getRandomBytes to initialize random seed for IO.rand. See discussion at this PR.

• Improve dot notation and aliases interaction. See discussion on Zulip for additional details. Example:

  def Set (α : Type) := α → Prop
  def Set.union (s₁ s₂ : Set α) : Set α := fun a => s₁ a ∨ s₂ a
  def FinSet (n : Nat) := Fin n → Prop
  
  namespace FinSet
    export Set (union) -- FinSet.union is now an alias for `Set.union`
  end FinSet
  
  example (x y : FinSet 10) : FinSet 10 :=
    x.union y -- Works
  

• ext and enter conv tactics can now go inside let-declarations. Example:

  example (g : Nat → Nat) (y : Nat) (h : let x := y + 1; g (0+x) = x) : g (y + 1) = y + 1 := by
    conv at h => enter [x, 1, 1]; rw [Nat.zero_add]
    /-
      g : Nat → Nat
      y : Nat
      h : let x := y + 1;
          g x = x
      ⊢ g (y + 1) = y + 1
    -/
    exact h
  

• Add zeta conv tactic to expand let-declarations. Example:

  example (h : let x := y + 1; 0 + x = y) : False := by
    conv at h => zeta; rw [Nat.zero_add]
    /-
      y : Nat
      h : y + 1 = y
      ⊢ False
    -/
    simp_arith at h
  

• Improve namespace resolution. See issue #1224. Example:

  import Lean
  open Lean Parser Elab
  open Tactic -- now opens both `Lean.Parser.Tactic` and `Lean.Elab.Tactic`
  

• Rename constant command to opaque. See discussion at Zulip.

• Extend induction and cases syntax: multiple left-hand-sides in a single alternative. This extension is very similar to the one implemented for match expressions. Examples:

  inductive Foo where
    | mk1 (x : Nat) | mk2 (x : Nat) | mk3
  
  def f (v : Foo) :=
    match v with
    | .mk1 x => x + 1
    | .mk2 x => 2*x + 1
    | .mk3   => 1
  
  theorem f_gt_zero : f v > 0 := by
    cases v with
    | mk1 x | mk2 x => simp_arith!  -- New feature used here!
    | mk3 => decide
  

• let/if indentation in do blocks in now supported.

• Add unnamed antiquotation $_ for use in syntax quotation patterns.

• Add unused variables linter. Feedback welcome!

• Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter. Examples:

  /-
  The following declaration now produces an error because `PUnit` is universe polymorphic,
  but the universe parameter does not occur in the function type `Nat → Nat`
  -/
  def f (n : Nat) : Nat :=
    let aux (_ : PUnit) : Nat := n + 1
    aux ⟨⟩
  
  /-
  The following declaration is accepted because the universe parameter was explicitly provided in the
  function signature.
  -/
  def g.{u} (n : Nat) : Nat :=
    let aux (_ : PUnit.{u}) : Nat := n + 1
    aux ⟨⟩
  

• Add subst_vars tactic.

• Fix autoParam in structure fields lost in multiple inheritance..

• Add [eliminator] attribute. It allows users to specify default recursor/eliminators for the induction and cases tactics. It is an alternative for the using notation. Example:

  @[eliminator] protected def recDiag {motive : Nat → Nat → Sort u}
      (zero_zero : motive 0 0)
      (succ_zero : (x : Nat) → motive x 0 → motive (x + 1) 0)
      (zero_succ : (y : Nat) → motive 0 y → motive 0 (y + 1))
      (succ_succ : (x y : Nat) → motive x y → motive (x + 1) (y + 1))
      (x y : Nat) :  motive x y :=
    let rec go : (x y : Nat) → motive x y
      | 0,     0 => zero_zero
      | x+1, 0   => succ_zero x (go x 0)
      | 0,   y+1 => zero_succ y (go 0 y)
      | x+1, y+1 => succ_succ x y (go x y)
    go x y
  termination_by go x y => (x, y)
  
  def f (x y : Nat) :=
    match x, y with
    | 0,   0   => 1
    | x+1, 0   => f x 0
    | 0,   y+1 => f 0 y
    | x+1, y+1 => f x y
  termination_by f x y => (x, y)
  
  example (x y : Nat) : f x y > 0 := by
    induction x, y <;> simp [f, *]
  

• Add support for casesOn applications to structural and well-founded recursion modules. This feature is useful when writing definitions using tactics. Example:

  inductive Foo where
    | a | b | c
    | pair: Foo × Foo → Foo
  
  def Foo.deq (a b : Foo) : Decidable (a = b) := by
    cases a <;> cases b
    any_goals apply isFalse Foo.noConfusion
    any_goals apply isTrue rfl
    case pair a b =>
      let (a₁, a₂) := a
      let (b₁, b₂) := b
      exact match deq a₁ b₁, deq a₂ b₂ with
      | isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
      | isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
      | _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
  

• Option is again a monad. The auxiliary type OptionM has been removed. See Zulip thread.

• Improve split tactic. It used to fail on match expressions of the form match h : e with ... where e is not a free variable. The failure used to occur during generalization.

• New encoding for match-expressions that use the h : notation for discriminants. The information is not lost during delaboration, and it is the foundation for a better split tactic. at delaboration time. Example:

  #print Nat.decEq
  /-
  protected def Nat.decEq : (n m : Nat) → Decidable (n = m) :=
  fun n m =>
    match h : Nat.beq n m with
    | true => isTrue (_ : n = m)
    | false => isFalse (_ : ¬n = m)
  -/
  

• exists tactic is now takes a comma separated list of terms.

• Add dsimp and dsimp! tactics. They guarantee the result term is definitionally equal, and only apply rfl-theorems.

• Fix binder information for match patterns that use definitions tagged with [matchPattern] (e.g., Nat.add). We now have proper binder information for the variable y in the following example.

  def f (x : Nat) : Nat :=
    match x with
    | 0 => 1
    | y + 1 => y
  

• (Fix) the default value for structure fields may now depend on the structure parameters. Example:

  structure Something (i: Nat) where
  n1: Nat := 1
  n2: Nat := 1 + i
  
  def s : Something 10 := {}
  example : s.n2 = 11 := rfl
  

• Apply rfl theorems at the dsimp auxiliary method used by simp. dsimp can be used anywhere in an expression because it preserves definitional equality.

• Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same name of a declaration being defined. Example:

  def f : f → Bool := -- Error at second `f`
    fun _ => true
  
  inductive Foo : List Foo → Type -- Error at second `Foo`
    | x : Foo []
  

  Before this refinement, the declarations above would be accepted and the second f and Foo would be treated as auto implicit variables. That is, f : {f : Sort u} → f → Bool, and Foo : {Foo : Type u} → List Foo → Type.

• Fix syntax highlighting for recursive declarations. Example

  inductive List (α : Type u) where
    | nil : List α  -- `List` is not highlighted as a variable anymore
    | cons (head : α) (tail : List α) : List α
  
  def List.map (f : α → β) : List α → List β
    | []    => []
    | a::as => f a :: map f as -- `map` is not highlighted as a variable anymore
  

• Add autoUnfold option to Lean.Meta.Simp.Config, and the following macros

  • simp! for simp (config := { autoUnfold := true })
  • simp_arith! for simp (config := { autoUnfold := true, arith := true })
  • simp_all! for simp_all (config := { autoUnfold := true })
  • simp_all_arith! for simp_all (config := { autoUnfold := true, arith := true })

  When the autoUnfold is set to true, simp tries to unfold the following kinds of definition

  • Recursive definitions defined by structural recursion.
  • Non-recursive definitions where the body is a match-expression. This kind of definition is only unfolded if the match can be reduced. Example:

  def append (as bs : List α) : List α :=
    match as with
    | [] => bs
    | a :: as => a :: append as bs
  
  theorem append_nil (as : List α) : append as [] = as := by
    induction as <;> simp_all!
  
  theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
    induction as <;> simp_all!
  

• Add save tactic for creating checkpoints more conveniently. Example:

  example : <some-proposition> := by
    tac_1
    tac_2
    save
    tac_3
    ...
  

  is equivalent to

  example : <some-proposition> := by
    checkpoint
      tac_1
      tac_2
    tac_3
    ...
  

• Remove support for {} annotation from inductive datatype constructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using {}

  inductive LE' (n : Nat) : Nat → Prop where
    | refl {} : LE' n n -- Want `n` to be explicit
    | succ  : LE' n m → LE' n (m+1)
  

  can now be written as

  inductive LE' : Nat → Nat → Prop where
    | refl (n : Nat) : LE' n n
    | succ : LE' n m → LE' n (m+1)
  

  In both cases, the inductive family has one parameter and one index. Recall that the actual number of parameters can be retrieved using the command #print.

• Remove support for {} annotation in the structure command.

• Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.

• In macro ... xs:p* ... and similar macro bindings of combinators, xs now has the correct type Array Syntax

• Identifiers in syntax patterns now ignore macro scopes during matching.

• Improve binder names for constructor auto implicit parameters. Example, given the inductive datatype

  inductive Member : α → List α → Type u
    | head : Member a (a::as)
    | tail : Member a bs → Member a (b::bs)
  

  before:

  #check @Member.head
  -- @Member.head : {x : Type u_1} → {a : x} → {as : List x} → Member a (a :: as)
  

  now:

  #check @Member.head
  -- @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)
  

• Improve error message when constructor parameter universe level is too big.

• Add support for for h : i in [start:stop] do .. where h : i ∈ [start:stop]. This feature is useful for proving termination of functions such as:

  inductive Expr where
    | app (f : String) (args : Array Expr)
  
  def Expr.size (e : Expr) : Nat := Id.run do
    match e with
    | app f args =>
      let mut sz := 1
      for h : i in [: args.size] do
        -- h.upper : i < args.size
        sz := sz + size (args.get ⟨i, h.upper⟩)
      return sz
  

• Add tactic case'. It is similar to case, but does not admit the goal on failure. For example, the new tactic is useful when writing tactic scripts where we need to use case' at first | ... | ..., and we want to take the next alternative when case' fails.

• Add tactic macro

  macro "stop" s:tacticSeq : tactic => `(repeat sorry)
  

  See discussion on Zulip.

• When displaying goals, we do not display inaccessible proposition names if they do not have forward dependencies. We still display their types. For example, the goal

  case node.inl.node
  β : Type u_1
  b : BinTree β
  k : Nat
  v : β
  left : Tree β
  key : Nat
  value : β
  right : Tree β
  ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
  ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
  h✝ : k < key
  a✝³ : BST left
  a✝² : ForallTree (fun k v => k < key) left
  a✝¹ : BST right
  a✝ : ForallTree (fun k v => key < k) right
  ⊢ BST left
  

  is now displayed as

  case node.inl.node
  β : Type u_1
  b : BinTree β
  k : Nat
  v : β
  left : Tree β
  key : Nat
  value : β
  right : Tree β
  ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
  ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
   : k < key
   : BST left
   : ForallTree (fun k v => k < key) left
   : BST right
   : ForallTree (fun k v => key < k) right
  ⊢ BST left
  

• The hypothesis name is now optional in the by_cases tactic.

• Fix inconsistency between syntax and kind names. The node kinds numLit, charLit, nameLit, strLit, and scientificLit are now called num, char, name, str, and scientific respectively. Example: we now write

  macro_rules | `($n:num) => `("hello")
  

  instead of

  macro_rules | `($n:numLit) => `("hello")
  

• (Experimental) New checkpoint <tactic-seq> tactic for big interactive proofs.

• Rename tactic nativeDecide => native_decide.

• Antiquotations are now accepted in any syntax. The incQuotDepth syntax parser is therefore obsolete and has been removed.

• Renamed tactic nativeDecide => native_decide.

• "Cleanup" local context before elaborating a match alternative right-hand-side. Examples:

  example (x : Nat) : Nat :=
    match g x with
    | (a, b) => _ -- Local context does not contain the auxiliary `_discr := g x` anymore
  
  example (x : Nat × Nat) (h : x.1 > 0) : f x > 0 := by
    match x with
    | (a, b) => _ -- Local context does not contain the `h✝ : x.fst > 0` anymore
  

• Improve let-pattern (and have-pattern) macro expansion. In the following example,

  example (x : Nat × Nat) : f x > 0 := by
    let (a, b) := x
    done
  

  The resulting goal is now ... |- f (a, b) > 0 instead of ... |- f x > 0.

• Add cross-compiled aarch64 Linux and aarch64 macOS releases.

• Add tutorial-like examples to our documentation, rendered using LeanInk+Alectryon.

v4.0.0-m4 (23 March 2022)

• simp now takes user-defined simp-attributes. You can define a new simp attribute by creating a file (e.g., MySimp.lean) containing

  import Lean
  open Lean.Meta
  
  initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
  

  If you don't need to access my_ext, you can also use the macro

  import Lean
  
  register_simp_attr my_simp "my own simp attribute"
  

  Recall that the new simp attribute is not active in the Lean file where it was defined. Here is a small example using the new feature.

  import MySimp
  
  def f (x : Nat) := x + 2
  def g (x : Nat) := x + 1
  
  @[my_simp] theorem f_eq : f x = x + 2 := rfl
  @[my_simp] theorem g_eq : g x = x + 1 := rfl
  
  example : f x + g x = 2*x + 3 := by
    simp_arith [my_simp]
  

• Extend match syntax: multiple left-hand-sides in a single alternative. Example:

  def fib : Nat → Nat
  | 0 | 1 => 1
  | n+2 => fib n + fib (n+1)
  

  This feature was discussed at issue 371. It was implemented as a macro expansion. Thus, the following is accepted.

  inductive StrOrNum where
    | S (s : String)
    | I (i : Int)
  
  def StrOrNum.asString (x : StrOrNum) :=
    match x with
    | I a | S a => toString a
  

• Improve #eval command. Now, when it fails to synthesize a Lean.MetaEval instance for the result type, it reduces the type and tries again. The following example now works without additional annotations

  def Foo := List Nat
  
  def test (x : Nat) : Foo :=
    [x, x+1, x+2]
  
  #eval test 4
  

• rw tactic can now apply auto-generated equation theorems for a given definition. Example:

  example (a : Nat) (h : n = 1) : [a].length = n := by
    rw [List.length]
    trace_state -- .. |- [].length + 1 = n
    rw [List.length]
    trace_state -- .. |- 0 + 1 = n
    rw [h]
  

• Fuzzy matching for auto completion

• Extend dot-notation x.field for arrow types. If type of x is an arrow, we look up for Function.field. For example, given f : Nat → Nat and g : Nat → Nat, f.comp g is now notation for Function.comp f g.

• The new .<identifier> notation is now also accepted where a function type is expected.

  example (xs : List Nat) : List Nat := .map .succ xs
  example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅
  

• Add code folding support to the language server.

• Support notation let <pattern> := <expr> | <else-case> in do blocks.

• Remove support for "auto" pure. In the Zulip thread, the consensus seemed to be that "auto" pure is more confusing than it's worth.

• Remove restriction in congr theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid congr theorem.

  @[congr]
  theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
                    ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=
  

• Partially applied congruence theorems.

• Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.

• Remove deprecated leanpkg in favor of Lake now bundled with Lean.

• Various improvements to go-to-definition & find-all-references accuracy.

• Auto generated congruence lemmas with support for casts on proofs and Decidable instances (see wishlist).

• Rename option autoBoundImplicitLocal => autoImplicit.

• Relax auto-implicit restrictions. The command set_option relaxedAutoImplicit false disables the relaxations.

• contradiction tactic now closes the goal if there is a False.elim application in the target.

• Renamed tatic byCases => by_cases (motivation: enforcing naming convention).

• Local instances occurring in patterns are now considered by the type class resolution procedure. Example:

  def concat : List ((α : Type) × ToString α × α) → String
    | [] => ""
    | ⟨_, _, a⟩ :: as => toString a ++ concat as
  

• Notation for providing the motive for match expressions has changed. before:

  match x, rfl : (y : Nat) → x = y → Nat with
  | 0,   h => ...
  | x+1, h => ...
  

  now:

  match (motive := (y : Nat) → x = y → Nat) x, rfl with
  | 0,   h => ...
  | x+1, h => ...
  

  With this change, the notation for giving names to equality proofs in match-expressions is not whitespace sensitive anymore. That is, we can now write

  match h : sort.swap a b with
  | (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
  

• (generalizing := true) is the default behavior for match expressions even if the expected type is not a proposition. In the following example, we used to have to include (generalizing := true) manually.

  inductive Fam : Type → Type 1 where
    | any : Fam α
    | nat : Nat → Fam Nat
  
  example (a : α) (x : Fam α) : α :=
    match x with
    | Fam.any   => a
    | Fam.nat n => n
  

• We now use PSum (instead of Sum) when compiling mutually recursive definitions using well-founded recursion.

• Better support for parametric well-founded relations. See issue #1017. This change affects the low-level termination_by' hint because the fixed prefix of the function parameters in not "packed" anymore when constructing the well-founded relation type. For example, in the following definition, as is part of the fixed prefix, and is not packed anymore. In previous versions, the termination_by' term would be written as measure fun ⟨as, i, _⟩ => as.size - i

  def sum (as : Array Nat) (i : Nat) (s : Nat) : Nat :=
    if h : i < as.size then
      sum as (i+1) (s + as.get ⟨i, h⟩)
    else
      s
  termination_by' measure fun ⟨i, _⟩ => as.size - i
  

• Add while <cond> do <do-block>, repeat <do-block>, and repeat <do-block> until <cond> macros for do-block. These macros are based on partial definitions, and consequently are useful only for writing programs we don't want to prove anything about.

• Add arith option to Simp.Config, the macro simp_arith expands to simp (config := { arith := true }). Only Nat and linear arithmetic is currently supported. Example:

  example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
    simp_arith
  

• Add fail <string>? tactic that always fail.

• Add support for acyclicity at dependent elimination. See issue #1022.

• Add trace <string> tactic for debugging purposes.

• Add nontrivial SizeOf instance for types Unit → α, and add support for them in the auto-generated SizeOf instances for user-defined inductive types. For example, given the inductive datatype

  inductive LazyList (α : Type u) where
    | nil                               : LazyList α
    | cons (hd : α) (tl : LazyList α)   : LazyList α
    | delayed (t : Thunk (LazyList α))  : LazyList α
  

  we now have sizeOf (LazyList.delayed t) = 1 + sizeOf t instead of sizeOf (LazyList.delayed t) = 2.

• Add support for guessing (very) simple well-founded relations when proving termination. For example, the following function does not require a termination_by annotation anymore.

  def Array.insertAtAux (i : Nat) (as : Array α) (j : Nat) : Array α :=
    if h : i < j then
      let as := as.swap! (j-1) j;
      insertAtAux i as (j-1)
    else
      as
  

• Add support for for h : x in xs do ... notation where h : x ∈ xs. This is mainly useful for showing termination.

• Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item). For example

  inductive HasType : Index n → Vector Ty n → Ty → Type where
  

  is now interpreted as

  inductive HasType : {n : Nat} → Index n → Vector Ty n → Ty → Type where
  

• To make the previous feature more convenient to use, we promote a fixed prefix of inductive family indices to parameters. For example, the following declaration is now accepted by Lean

  inductive Lst : Type u → Type u
    | nil  : Lst α
    | cons : α → Lst α → Lst α
  

  and α in Lst α is a parameter. The actual number of parameters can be inspected using the command #print Lst. This feature also makes sure we still accept the declaration

  inductive Sublist : List α → List α → Prop
    | slnil : Sublist [] []
    | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
    | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
  

• Added auto implicit "chaining". Unassigned metavariables occurring in the auto implicit types now become new auto implicit locals. Consider the following example:

  inductive HasType : Fin n → Vector Ty n → Ty → Type where
    | stop : HasType 0 (ty :: ctx) ty
    | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
  

  ctx is an auto implicit local in the two constructors, and it has type ctx : Vector Ty ?m. Without auto implicit "chaining", the metavariable ?m will remain unassigned. The new feature creates yet another implicit local n : Nat and assigns n to ?m. So, the declaration above is shorthand for

  inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where
    | stop : {ty : Ty} → {n : Nat} → {ctx : Vector Ty n} → HasType 0 (ty :: ctx) ty
    | pop  : {n : Nat} → {k : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
  

• Eliminate auxiliary type annotations (e.g, autoParam and optParam) from recursor minor premises and projection declarations. Consider the following example

  structure A :=
    x : Nat
    h : x = 1 := by trivial
  
  example (a : A) : a.x = 1 := by
    have aux := a.h
    -- `aux` has now type `a.x = 1` instead of `autoParam (a.x = 1) auto✝`
    exact aux
  
  example (a : A) : a.x = 1 := by
    cases a with
    | mk x h =>
      -- `h` has now type `x = 1` instead of `autoParam (x = 1) auto✝`
      assumption
  

• We now accept overloaded notation in patterns, but we require the set of pattern variables in each alternative to be the same. Example:

  inductive Vector (α : Type u) : Nat → Type u
    | nil : Vector α 0
    | cons : α → Vector α n → Vector α (n+1)
  
  infix:67 " :: " => Vector.cons -- Overloading the `::` notation
  
  def head1 (x : List α) (h : x ≠ []) : α :=
    match x with
    | a :: as => a -- `::` is `List.cons` here
  
  def head2 (x : Vector α (n+1)) : α :=
    match x with
    | a :: as => a -- `::` is `Vector.cons` here
  

• New notation .<identifier> based on Swift. The namespace is inferred from the expected type. See issue #944. Examples:

  def f (x : Nat) : Except String Nat :=
    if x > 0 then
      .ok x
    else
      .error "x is zero"
  
  namespace Lean.Elab
  open Lsp
  
  def identOf : Info → Option (RefIdent × Bool)
    | .ofTermInfo ti => match ti.expr with
      | .const n .. => some (.const n, ti.isBinder)
      | .fvar id .. => some (.fvar id, ti.isBinder)
      | _ => none
    | .ofFieldInfo fi => some (.const fi.projName, false)
    | _ => none
  
  def isImplicit (bi : BinderInfo) : Bool :=
    bi matches .implicit
  
  end Lean.Elab