lean bump

Stream: mathlib4

[Johan Commelin]

Anybody interested in bumping Lean? That will help with feat: port Data.Fin.Basic (mathlib4#1084)

[Ruben Van de Velde]

Johan Commelin said:

Anybody interested in bumping Lean? That will help with feat: port Data.Fin.Basic (mathlib4#1084)

Nightly isn't out yet, fwiw.

With a bit of luck, we might even be able to do this bump without changing std4/aesop

[Scott Morrison]

Currently mathlib4 is at 2023-01-10 already, and 2023-01-11 won't be out for another 11 hours or so, I think.

If it's critical you can push a tag to your own fork of the Lean 4 repository, and then put that in your lean-toolchain file on a mathlib4 branch. Which commit did you want?

[Johan Commelin]

We need current HEAD of master, aka https://github.com/leanprover/lean4/commit/8cd9ce06843c9d42d6d6dc43d3e81e3b49dfc20f

[Sebastian Ullrich]

After a bit of a delay, nightly-2023-01-12 is released now

[Heather Macbeth]

!4#1999, bumping to nightly-2023-02-03, should be easy to review.