v4.22.0-rc3

chore: fix test

v4.22.0-rc2

fix: lake: source file not in module input trace & some logs dropped …

v4.22.0-rc1

chore: set LEAN_VERSION_IS_RELEASE 1

v4.21.0

fix: remove global `NatCast (Fin n)` instance (#8620)

This PR removes the `NatCast (Fin n)` global instance (both the direct
instance, and the indirect one via `Lean.Grind.Semiring`), as that
instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
however that in Mathlib this happens anyway!

v4.21.0-rc3

fix: remove global `NatCast (Fin n)` instance (#8620)

This PR removes the `NatCast (Fin n)` global instance (both the direct
instance, and the indirect one via `Lean.Grind.Semiring`), as that
instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
however that in Mathlib this happens anyway!

v4.20.1

chore: revise environment constant addition details (#8610)

* Move constant registration with elab env from `Lean.addDecl` to
`Lean.Environment.addDeclCore` for compatibility
* Make module system behavior independent of `Elab.async` value

v4.20.1-rc1

chore: revise environment constant addition details (#8610)

* Move constant registration with elab env from `Lean.addDecl` to
`Lean.Environment.addDeclCore` for compatibility
* Make module system behavior independent of `Elab.async` value

v4.21.0-rc2

Empty commit to re-randomize the hash.

Lake uses the first characters of the Lean commit hash in its version
number. When this accidentally is an all-numeric string starting with a
0, some tools expecting SemVer break. We encountered that issue on
v4.21.0-rc1. This empty commit rerolls the dice on the commit hash,
so we hopefully do not start with a 0 or have some non-numeric characters.

v4.21.0-rc1

chore: set release flag

v4.20.0

fix: exponential compilation times due to inlined instances (#8254)

This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr`
instances, which was causing exponential compilation times in `deriving`
clauses for large structures.