Chore: update Lean to v4.26.0

[quinn-dougherty]

Bump lean-toolchain and silence two warnings:

/Work/LSpec > lake build
  [8/11] Built LSpec.LSpec
warning: LSpec/LSpec.lean:132:13: `String.mk` has been deprecated: Use `String.ofList` instead
  [9/11] Built LSpec.Instances
warning: LSpec/Instances.lean:59:60: `Nat.le_step` has been deprecated: Use `Nat.le_succ_of_le` instead
Build completed successfully (11 jobs).

[arthurpaulino]

Let me ping @samuelburnham for the Nix-related portion of the bump.

[quinn-dougherty]

@lenianiva did not merge the v4.26.0 to her main yet lenianiva/lean4-nix#105, i pushed moving the flake input to her v4.26.0 branch but something happened to nix build (bumping flake-parts to most recent commit didn't help either, i experimented with that but left it in my local tree to keep the impact of this PR as minimal as possible)

nix build:

         from call site
         at /home/q/Documents/Work/LSpec/flake.nix:39:13:
           38|         packages.default =
           39|           ((lean4-nix.lake {inherit pkgs;}).mkPackage {
             |             ^
           40|             src = ./.;

       error: function 'anonymous lambda' called without required argument 'lib'
       at �github:lenianiva/lean4-nix/86c3e53196ff3c08049e464821bcbebbb9ee8ba6?narHash=sha256-81IuI/Q/y9QG5gLK4ZKzlHC%2BmVb2SvbyS71Ro2FmOK8%3D�/lib/lake.nix:1:1:
            1| {
             | ^
            2|   pkgs,

Should be able to figure it out by reading the lean4-nix recent git history, or maybe she wrote a migration guide.

[quinn-dougherty]

i think i see what i have to do--- it'll increase the footprint of the PR but I hope that's ok, you can cherry pick commits if you want

[quinn-dougherty]

Would be better to wait for lenianiva/lean4-nix#105 to merge in so that we're pointing to a commit of main in the flake lock instead of a branch in the flake input.

[lenianiva]

I didn't merge it yesterday because of some error in Garnix that caused the CI to fail. I'll merge it now.

[lenianiva]

@lenianiva did not merge the v4.26.0 to her main yet lenianiva/lean4-nix#105, i pushed moving the flake input to her v4.26.0 branch but something happened to nix build (bumping flake-parts to most recent commit didn't help either, i experimented with that but left it in my local tree to keep the impact of this PR as minimal as possible)

nix build:

         from call site
         at /home/q/Documents/Work/LSpec/flake.nix:39:13:
           38|         packages.default =
           39|           ((lean4-nix.lake {inherit pkgs;}).mkPackage {
             |             ^
           40|             src = ./.;

       error: function 'anonymous lambda' called without required argument 'lib'
       at �github:lenianiva/lean4-nix/86c3e53196ff3c08049e464821bcbebbb9ee8ba6?narHash=sha256-81IuI/Q/y9QG5gLK4ZKzlHC%2BmVb2SvbyS71Ro2FmOK8%3D�/lib/lake.nix:1:1:
            1| {
             | ^
            2|   pkgs,

Should be able to figure it out by reading the lean4-nix recent git history, or maybe she wrote a migration guide.

lean4-nix had a refactoring which moved to using lake itself to build user packages instead of buildLeanPackage. As a result now it has to be called like this:

(pkgs.callPackage lean4-nix.lake {}).mkPackage ...

[samuelburnham]

Looks good pending a few quick changes. Thanks!