v4.25.0-rc1

chore: set LEAN_VERSION_IS_RELEASE to 1 for v4.25.0-rc1

v4.24.0

fix: overeager specialisation reuse in codegen (#10429)

This PR fixes and overeager reuse of specialisation in the code
generator.

The issue was originally discovered in
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Miscompilation.20.28incorrect.20code.29.20in.20new.20compiler/near/540037917
and occurs because the specialisation cache didnt't take the name of
alternatives in pattern matches
into account.

v4.24.0-rc1

feat: non-commutative ring normalizer in `grind`  (#10375)

This PR adds support for non-commutative ring normalization in `grind`.
The new normalizer also accounts for the `IsCharP` type class. Examples:
```lean
open Lean Grind

variable (R : Type u) [Ring R]
example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + 2 * b * a + 4 * b^2 := by grind
example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + -b * (-4) * a - 2*b*a + 4 * b^2 := by grind

variable [IsCharP R 4]
example (a b : R) : (a - b)^2 = a^2 - a * b - b * 5 * a + b^2 := by grind
example (a b : R) : (a - b)^2 = 13*a^2 - a * b - b * 5 * a + b*3*b*3 := by grind
```

v4.23.0

refactor: port more of `shell.cpp` to Lean (#10086)

This PR ports more of the post-initialization C++ shell code to Lean.

All that remains is the initialization of the profiler and task manager.
As initialization tasks rather than main shell code, they were left in
C++ (where the rest of the initialization code currently is).

The `max_memory` and `timeout` Lean options used by the the `--memory`
and `--timeout` command-line options are now properly registered. The
server defaults for max memory and max heartbeats (timeout) were removed
as they were not actually used (because the `server` option that was
checked was neither set nor exists).

This PR also makes better use of the module system in `Shell.lean` and
fixes a minor bug in a previous port where the file name check was
dependent on building the `.ilean` rather than the `.c` file (as was
originally the case).

Fixes #9879.

(cherry picked from commit db3fb47109de07fcfbb3e493d387086b0b8c01ae)

v4.23.0-rc2

fix: panic in `delabPRange`

v4.23.0-rc1

chore: set LEAN_VERSION_IS_RELEASE=1

v4.22.0

fix: correctly handle non-`Nat` literal types in LCNF `elimDeadBranch…

v4.22.0-rc4

refactor: Expose DeclNameGenerator idx (#9342)

Backport 275e4838858c1ad7c8618a700fee51c70b923762 from #9020.

Co-authored-by: Leni Aniva <[email protected]>

v4.22.0-rc3

chore: fix test

v4.22.0-rc2

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