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.

v4.20.0-rc5

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.

v4.20.0-rc4

fix: broken goals accomplished (#8242)

This PR fixes the 'goals accomplished' diagnostics. They were
accidentally broken in #7902.

Regression test tbd in a future PR.

(cherry picked from commit 65b37b40ffa6cdef85ee16f36d141453505935dc)