Skip to content

Commit c41bcf0

Browse files
authored
chore: bump toolchain to v4.6.0 (leanprover-community#34)
* chore: bump toolchain to v4.6.0 * oops, run lake update * sigh
1 parent 6651502 commit c41bcf0

File tree

4 files changed

+13
-13
lines changed

4 files changed

+13
-13
lines changed

lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.6.0-rc1
1+
leanprover/lean4:v4.6.0

test/Mathlib/lake-manifest.json

+10-10
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,16 @@
44
[{"url": "https://github.com/leanprover/std4",
55
"type": "git",
66
"subDir": null,
7-
"rev": "276953b13323ca151939eafaaec9129bf7970306",
7+
"rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
88
"name": "std",
99
"manifestFile": "lake-manifest.json",
10-
"inputRev": "main",
10+
"inputRev": "v4.6.0",
1111
"inherited": true,
1212
"configFile": "lakefile.lean"},
1313
{"url": "https://github.com/leanprover-community/quote4",
1414
"type": "git",
1515
"subDir": null,
16-
"rev": "1c88406514a636d241903e2e288d21dc6d861e01",
16+
"rev": "fd760831487e6835944e7eeed505522c9dd47563",
1717
"name": "Qq",
1818
"manifestFile": "lake-manifest.json",
1919
"inputRev": "master",
@@ -22,19 +22,19 @@
2222
{"url": "https://github.com/leanprover-community/aesop",
2323
"type": "git",
2424
"subDir": null,
25-
"rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
25+
"rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
2626
"name": "aesop",
2727
"manifestFile": "lake-manifest.json",
28-
"inputRev": "master",
28+
"inputRev": "v4.6.0",
2929
"inherited": true,
3030
"configFile": "lakefile.lean"},
3131
{"url": "https://github.com/leanprover-community/ProofWidgets4",
3232
"type": "git",
3333
"subDir": null,
34-
"rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
34+
"rev": "16cae05860b208925f54e5581ec5fd264823440c",
3535
"name": "proofwidgets",
3636
"manifestFile": "lake-manifest.json",
37-
"inputRev": "v0.0.27",
37+
"inputRev": "v0.0.29",
3838
"inherited": true,
3939
"configFile": "lakefile.lean"},
4040
{"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
4949
{"url": "https://github.com/leanprover-community/import-graph.git",
5050
"type": "git",
5151
"subDir": null,
52-
"rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
52+
"rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
5353
"name": "importGraph",
5454
"manifestFile": "lake-manifest.json",
5555
"inputRev": "main",
@@ -58,10 +58,10 @@
5858
{"url": "https://github.com/leanprover-community/mathlib4",
5959
"type": "git",
6060
"subDir": null,
61-
"rev": "490d2d4820d3ed2dea34f47f3cdfe9d72b8fbc80",
61+
"rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
6262
"name": "mathlib",
6363
"manifestFile": "lake-manifest.json",
64-
"inputRev": "master",
64+
"inputRev": "v4.6.0",
6565
"inherited": false,
6666
"configFile": "lakefile.lean"}],
6767
"name": "«repl-mathlib-tests»",

test/Mathlib/lakefile.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ open Lake DSL
33

44
package «repl-mathlib-tests» where
55
-- add package configuration options here
6-
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
6+
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.6.0"
77

88
@[default_target]
99
lean_lib «ReplMathlibTests» where

test/Mathlib/lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.6.0-rc1
1+
leanprover/lean4:v4.6.0

0 commit comments

Comments
 (0)