Skip to content

Commit 0381927

Browse files
GarmelonGarmelon
committed
chore: bump toolchain to v4.33.0-rc1
1 parent 63835f2 commit 0381927

6 files changed

Lines changed: 137 additions & 111 deletions

File tree

‎lake-manifest.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "b3debfe6b629192033ef87257e1c60201881646f",
8+
"rev": "56958b3901ca108830de34fbce6cecd4b5757c1f",
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": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
18+
"rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2026-07-15
1+
leanprover/lean4:v4.33.0-rc1

‎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": "b3debfe6b629192033ef87257e1c60201881646f",
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": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
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": "31907cc18f48a95384f99cee5582c00fb39e0f67",
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": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
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": "b3debfe6b629192033ef87257e1c60201881646f",
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": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
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": "31907cc18f48a95384f99cee5582c00fb39e0f67",
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:nightly-2026-07-15
1+
leanprover/lean4:v4.33.0-rc1

‎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": "b3debfe6b629192033ef87257e1c60201881646f",
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": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
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": "31907cc18f48a95384f99cee5582c00fb39e0f67",
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": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
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": "b3debfe6b629192033ef87257e1c60201881646f",
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": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
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": "31907cc18f48a95384f99cee5582c00fb39e0f67",
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:nightly-2026-07-15
1+
leanprover/lean4:v4.33.0-rc1

0 commit comments

Comments
 (0)