Skip to content

Commit d90090f

Browse files
chore: bump toolchain to v4.31.0-rc2 (#40358)
Co-authored-by: Joscha <joscha@plugh.de> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
1 parent 1fcbe87 commit d90090f

4 files changed

Lines changed: 21 additions & 19 deletions

File tree

docs/overview.yaml

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -583,14 +583,16 @@ Data structures:
583583

584584
Maps:
585585
key-value map: 'AList'
586-
red-black map: 'Batteries.RBMap'
586+
# deprecated in https://github.com/leanprover-community/batteries/pull/1792
587+
# red-black map: 'Batteries.RBMap'
587588
hash map: 'Std.HashMap'
588589
finitely supported function: 'Finsupp'
589590
finite map: 'Finmap'
590591

591592
Trees:
592593
tree: 'Tree'
593-
red-black tree: 'Batteries.RBSet'
594+
# deprecated in https://github.com/leanprover-community/batteries/pull/1792
595+
# red-black tree: 'Batteries.RBSet'
594596
size-balanced binary search tree: 'Ordnode'
595597
W type: 'WType'
596598

lake-manifest.json

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "9196a81145e1e291a1469288e77392b0e1b9a493",
8+
"rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347",
99
"name": "plausible",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "leanprover-community",
28-
"rev": "6db47de43aa7f516708053ae2fdadd29dd9baaaa",
28+
"rev": "99c763c8a96d3d44fb4994e96eaa51ca4568449d",
2929
"name": "importGraph",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",
@@ -35,50 +35,50 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "85bb7e7637e84a7d9803be7d954579fdae42c64b",
38+
"rev": "1537e3fc7e680d64e06fe5fb95c4c9edee7941c2",
3939
"name": "proofwidgets",
4040
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.100",
41+
"inputRev": "v0.0.101",
4242
"inherited": false,
4343
"configFile": "lakefile.lean"},
4444
{"url": "https://github.com/leanprover-community/aesop",
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "fafca80479ff95e041d84373dda7122adf1295f2",
48+
"rev": "7897ea6e5cfc6522d355083bdfa798377ab35e11",
4949
"name": "aesop",
5050
"manifestFile": "lake-manifest.json",
51-
"inputRev": "v4.31.0-rc1",
51+
"inputRev": "v4.31.0-rc2",
5252
"inherited": false,
5353
"configFile": "lakefile.toml"},
5454
{"url": "https://github.com/leanprover-community/quote4",
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "8d33324ee877e9735d2829bc6f1f439e60cf98b1",
58+
"rev": "94346b7b49c36ae871639d1434232f057c193d60",
5959
"name": "Qq",
6060
"manifestFile": "lake-manifest.json",
61-
"inputRev": "v4.31.0-rc1",
61+
"inputRev": "v4.31.0-rc2",
6262
"inherited": false,
6363
"configFile": "lakefile.toml"},
6464
{"url": "https://github.com/leanprover-community/batteries",
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "708b057842c4cd0845fba132bd94b08493f6fc42",
68+
"rev": "460b61adc7d183e43db2b99ac6c1dede9f7a76df",
6969
"name": "batteries",
7070
"manifestFile": "lake-manifest.json",
71-
"inputRev": "v4.31.0-rc1",
71+
"inputRev": "v4.31.0-rc2",
7272
"inherited": false,
7373
"configFile": "lakefile.toml"},
7474
{"url": "https://github.com/leanprover/lean4-cli",
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover",
78-
"rev": "48bdcff4c5fa27e09028f9f330e59baa0d4640cf",
78+
"rev": "baf3e62fbb3502305076ca077e004aea78157c63",
7979
"name": "Cli",
8080
"manifestFile": "lake-manifest.json",
81-
"inputRev": "v4.31.0-rc1",
81+
"inputRev": "v4.31.0-rc2",
8282
"inherited": true,
8383
"configFile": "lakefile.toml"}],
8484
"name": "mathlib",

lakefile.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ open Lake DSL
66
## Mathlib dependencies on upstream projects
77
-/
88

9-
require "leanprover-community" / "batteries" @ git "v4.31.0-rc1"
10-
require "leanprover-community" / "Qq" @ git "v4.31.0-rc1"
11-
require "leanprover-community" / "aesop" @ git "v4.31.0-rc1"
12-
require "leanprover-community" / "proofwidgets" @ git "v0.0.100"
9+
require "leanprover-community" / "batteries" @ git "v4.31.0-rc2"
10+
require "leanprover-community" / "Qq" @ git "v4.31.0-rc2"
11+
require "leanprover-community" / "aesop" @ git "v4.31.0-rc2"
12+
require "leanprover-community" / "proofwidgets" @ git "v0.0.101"
1313
with NameMap.empty.insert `errorOnBuild
1414
"ProofWidgets failed to reuse pre-built JS code. \
1515
Please report this issue on the Lean Zulip."

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0-rc1
1+
leanprover/lean4:v4.31.0-rc2

0 commit comments

Comments
 (0)