Skip to content

Commit e09d21a

Browse files
GarmelonGarmelon
authored
chore: bump toolchain to v4.32.0 (#925)
1 parent 8649419 commit e09d21a

10 files changed

Lines changed: 163 additions & 132 deletions

File tree

‎lake-manifest.json‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
8+
"rev": "b3debfe6b629192033ef87257e1c60201881646f",
99
"name": "illuminate",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
18+
"rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
28+
"rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
2929
"name": "MD4Lean",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "",
38-
"rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
38+
"rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
3939
"name": "subverso",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",

‎lean-toolchain‎

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

‎test-projects/anchor-examples/lake-manifest.json‎

Lines changed: 21 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,21 @@
1-
{"version": "1.2.0",
2-
"packagesDir": ".lake/packages",
3-
"packages":
4-
[{"url": "https://github.com/leanprover/subverso",
5-
"type": "git",
6-
"subDir": null,
7-
"scope": "",
8-
"rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
9-
"name": "subverso",
10-
"manifestFile": "lake-manifest.json",
11-
"inputRev": "main",
12-
"inherited": false,
13-
"configFile": "lakefile.lean"}],
14-
"name": "examples",
15-
"lakeDir": ".lake",
16-
"fixedToolchain": false}
1+
{
2+
"version": "1.2.0",
3+
"packagesDir": ".lake/packages",
4+
"packages": [
5+
{
6+
"url": "https://github.com/leanprover/subverso",
7+
"type": "git",
8+
"subDir": null,
9+
"scope": "",
10+
"rev": "efa6467799f50bb896318ef12a1337c14eb3d323",
11+
"name": "subverso",
12+
"manifestFile": "lake-manifest.json",
13+
"inputRev": "main",
14+
"inherited": false,
15+
"configFile": "lakefile.lean"
16+
}
17+
],
18+
"name": "examples",
19+
"lakeDir": ".lake",
20+
"fixedToolchain": false
21+
}

‎test-projects/documented-package/lake-manifest.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
"type": "git",
88
"subDir": null,
99
"scope": "",
10-
"rev": "b899742d040e9eb946daec33c4d129a73537ae6c",
10+
"rev": "efa6467799f50bb896318ef12a1337c14eb3d323",
1111
"name": "subverso",
1212
"manifestFile": "lake-manifest.json",
1313
"inputRev": "main",

‎test-projects/literate-config/lake-manifest.json‎

Lines changed: 66 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,66 @@
1-
{"version": "1.2.0",
2-
"packagesDir": ".lake/packages",
3-
"packages":
4-
[{"type": "path",
5-
"scope": "",
6-
"name": "verso",
7-
"manifestFile": "lake-manifest.json",
8-
"inherited": false,
9-
"dir": "../..",
10-
"configFile": "lakefile.lean"},
11-
{"url": "https://github.com/leanprover/illuminate",
12-
"type": "git",
13-
"subDir": null,
14-
"scope": "",
15-
"rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
16-
"name": "illuminate",
17-
"manifestFile": "lake-manifest.json",
18-
"inputRev": "main",
19-
"inherited": true,
20-
"configFile": "lakefile.lean"},
21-
{"url": "https://github.com/leanprover-community/plausible",
22-
"type": "git",
23-
"subDir": null,
24-
"scope": "",
25-
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
26-
"name": "plausible",
27-
"manifestFile": "lake-manifest.json",
28-
"inputRev": "main",
29-
"inherited": true,
30-
"configFile": "lakefile.toml"},
31-
{"url": "https://github.com/acmepjz/md4lean",
32-
"type": "git",
33-
"subDir": null,
34-
"scope": "",
35-
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
36-
"name": "MD4Lean",
37-
"manifestFile": "lake-manifest.json",
38-
"inputRev": "main",
39-
"inherited": true,
40-
"configFile": "lakefile.lean"},
41-
{"url": "https://github.com/leanprover/subverso",
42-
"type": "git",
43-
"subDir": null,
44-
"scope": "",
45-
"rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
46-
"name": "subverso",
47-
"manifestFile": "lake-manifest.json",
48-
"inputRev": "main",
49-
"inherited": true,
50-
"configFile": "lakefile.lean"}],
51-
"name": "«literate-config-test»",
52-
"lakeDir": ".lake",
53-
"fixedToolchain": false}
1+
{
2+
"version": "1.2.0",
3+
"packagesDir": ".lake/packages",
4+
"packages": [
5+
{
6+
"type": "path",
7+
"scope": "",
8+
"name": "verso",
9+
"manifestFile": "lake-manifest.json",
10+
"inherited": false,
11+
"dir": "../..",
12+
"configFile": "lakefile.lean"
13+
},
14+
{
15+
"url": "https://github.com/leanprover/illuminate",
16+
"type": "git",
17+
"subDir": null,
18+
"scope": "",
19+
"rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
20+
"name": "illuminate",
21+
"manifestFile": "lake-manifest.json",
22+
"inputRev": "main",
23+
"inherited": true,
24+
"configFile": "lakefile.lean"
25+
},
26+
{
27+
"url": "https://github.com/leanprover-community/plausible",
28+
"type": "git",
29+
"subDir": null,
30+
"scope": "",
31+
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
32+
"name": "plausible",
33+
"manifestFile": "lake-manifest.json",
34+
"inputRev": "main",
35+
"inherited": true,
36+
"configFile": "lakefile.toml"
37+
},
38+
{
39+
"url": "https://github.com/acmepjz/md4lean",
40+
"type": "git",
41+
"subDir": null,
42+
"scope": "",
43+
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
44+
"name": "MD4Lean",
45+
"manifestFile": "lake-manifest.json",
46+
"inputRev": "main",
47+
"inherited": true,
48+
"configFile": "lakefile.lean"
49+
},
50+
{
51+
"url": "https://github.com/leanprover/subverso",
52+
"type": "git",
53+
"subDir": null,
54+
"scope": "",
55+
"rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
56+
"name": "subverso",
57+
"manifestFile": "lake-manifest.json",
58+
"inputRev": "main",
59+
"inherited": true,
60+
"configFile": "lakefile.lean"
61+
}
62+
],
63+
"name": "«literate-config-test»",
64+
"lakeDir": ".lake",
65+
"fixedToolchain": false
66+
}

‎test-projects/literate-config/lean-toolchain‎

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

‎test-projects/literate-multi-root/lake-manifest.json‎

Lines changed: 66 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,66 @@
1-
{"version": "1.2.0",
2-
"packagesDir": ".lake/packages",
3-
"packages":
4-
[{"type": "path",
5-
"scope": "",
6-
"name": "verso",
7-
"manifestFile": "lake-manifest.json",
8-
"inherited": false,
9-
"dir": "../..",
10-
"configFile": "lakefile.lean"},
11-
{"url": "https://github.com/leanprover/illuminate",
12-
"type": "git",
13-
"subDir": null,
14-
"scope": "",
15-
"rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
16-
"name": "illuminate",
17-
"manifestFile": "lake-manifest.json",
18-
"inputRev": "main",
19-
"inherited": true,
20-
"configFile": "lakefile.lean"},
21-
{"url": "https://github.com/leanprover-community/plausible",
22-
"type": "git",
23-
"subDir": null,
24-
"scope": "",
25-
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
26-
"name": "plausible",
27-
"manifestFile": "lake-manifest.json",
28-
"inputRev": "main",
29-
"inherited": true,
30-
"configFile": "lakefile.toml"},
31-
{"url": "https://github.com/acmepjz/md4lean",
32-
"type": "git",
33-
"subDir": null,
34-
"scope": "",
35-
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
36-
"name": "MD4Lean",
37-
"manifestFile": "lake-manifest.json",
38-
"inputRev": "main",
39-
"inherited": true,
40-
"configFile": "lakefile.lean"},
41-
{"url": "https://github.com/leanprover/subverso",
42-
"type": "git",
43-
"subDir": null,
44-
"scope": "",
45-
"rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
46-
"name": "subverso",
47-
"manifestFile": "lake-manifest.json",
48-
"inputRev": "main",
49-
"inherited": true,
50-
"configFile": "lakefile.lean"}],
51-
"name": "«literate-multi-root-test»",
52-
"lakeDir": ".lake",
53-
"fixedToolchain": false}
1+
{
2+
"version": "1.2.0",
3+
"packagesDir": ".lake/packages",
4+
"packages": [
5+
{
6+
"type": "path",
7+
"scope": "",
8+
"name": "verso",
9+
"manifestFile": "lake-manifest.json",
10+
"inherited": false,
11+
"dir": "../..",
12+
"configFile": "lakefile.lean"
13+
},
14+
{
15+
"url": "https://github.com/leanprover/illuminate",
16+
"type": "git",
17+
"subDir": null,
18+
"scope": "",
19+
"rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
20+
"name": "illuminate",
21+
"manifestFile": "lake-manifest.json",
22+
"inputRev": "main",
23+
"inherited": true,
24+
"configFile": "lakefile.lean"
25+
},
26+
{
27+
"url": "https://github.com/leanprover-community/plausible",
28+
"type": "git",
29+
"subDir": null,
30+
"scope": "",
31+
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
32+
"name": "plausible",
33+
"manifestFile": "lake-manifest.json",
34+
"inputRev": "main",
35+
"inherited": true,
36+
"configFile": "lakefile.toml"
37+
},
38+
{
39+
"url": "https://github.com/acmepjz/md4lean",
40+
"type": "git",
41+
"subDir": null,
42+
"scope": "",
43+
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
44+
"name": "MD4Lean",
45+
"manifestFile": "lake-manifest.json",
46+
"inputRev": "main",
47+
"inherited": true,
48+
"configFile": "lakefile.lean"
49+
},
50+
{
51+
"url": "https://github.com/leanprover/subverso",
52+
"type": "git",
53+
"subDir": null,
54+
"scope": "",
55+
"rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
56+
"name": "subverso",
57+
"manifestFile": "lake-manifest.json",
58+
"inputRev": "main",
59+
"inherited": true,
60+
"configFile": "lakefile.lean"
61+
}
62+
],
63+
"name": "«literate-multi-root-test»",
64+
"lakeDir": ".lake",
65+
"fixedToolchain": false
66+
}

‎test-projects/literate-multi-root/lean-toolchain‎

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

‎test-projects/website-examples/lake-manifest.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
"url": "https://github.com/leanprover/subverso",
77
"type": "git",
88
"subDir": null,
9-
"rev": "b899742d040e9eb946daec33c4d129a73537ae6c",
9+
"rev": "efa6467799f50bb896318ef12a1337c14eb3d323",
1010
"name": "subverso",
1111
"manifestFile": "lake-manifest.json",
1212
"inputRev": "main",

‎test-projects/website-literate/lake-manifest.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
"type": "git",
88
"subDir": null,
99
"scope": "",
10-
"rev": "b899742d040e9eb946daec33c4d129a73537ae6c",
10+
"rev": "efa6467799f50bb896318ef12a1337c14eb3d323",
1111
"name": "subverso",
1212
"manifestFile": "lake-manifest.json",
1313
"inputRev": "main",

0 commit comments

Comments
 (0)