Skip to content

Commit f2b41e9

Browse files
authored
Update docbuild to v4.31.0 (#168)
1 parent 3e43b33 commit f2b41e9

3 files changed

Lines changed: 30 additions & 29 deletions

File tree

docbuild/lake-manifest.json

Lines changed: 28 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1-
{"version": "1.1.0",
1+
{"version": "1.2.0",
22
"packagesDir": "../correctness/.lake/packages",
33
"packages":
44
[{"url": "https://github.com/leanprover/doc-gen4",
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover",
8-
"rev": "aa4c3e4e14f5b31495b7c7238762ecceddd9f52c",
8+
"rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921",
99
"name": "«doc-gen4»",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.29.0",
11+
"inputRev": "v4.31.0",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"type": "path",
@@ -18,21 +18,21 @@
1818
"inherited": false,
1919
"dir": "../correctness",
2020
"configFile": "lakefile.toml"},
21-
{"url": "https://github.com/kim-em/leansqlite",
21+
{"url": "https://github.com/leanprover/leansqlite",
2222
"type": "git",
2323
"subDir": null,
2424
"scope": "",
25-
"rev": "d14544c72b593af6a66131bc34cdab16bf7c0940",
25+
"rev": "0be4df908d1a8e75b58961041e2b4973692623df",
2626
"name": "leansqlite",
2727
"manifestFile": "lake-manifest.json",
28-
"inputRev": "suppress-reducibility-warning",
28+
"inputRev": "main",
2929
"inherited": true,
3030
"configFile": "lakefile.lean"},
3131
{"url": "https://github.com/leanprover/lean4-cli",
3232
"type": "git",
3333
"subDir": null,
3434
"scope": "",
35-
"rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
35+
"rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
3636
"name": "Cli",
3737
"manifestFile": "lake-manifest.json",
3838
"inputRev": "main",
@@ -42,7 +42,7 @@
4242
"type": "git",
4343
"subDir": null,
4444
"scope": "",
45-
"rev": "9539e34e5cb2d52a6454d9b6218f6b6835cad071",
45+
"rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c",
4646
"name": "UnicodeBasic",
4747
"manifestFile": "lake-manifest.json",
4848
"inputRev": "main",
@@ -68,16 +68,6 @@
6868
"inputRev": "main",
6969
"inherited": true,
7070
"configFile": "lakefile.lean"},
71-
{"url": "https://github.com/leanprover-community/plausible",
72-
"type": "git",
73-
"subDir": null,
74-
"scope": "",
75-
"rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
76-
"name": "plausible",
77-
"manifestFile": "lake-manifest.json",
78-
"inputRev": "main",
79-
"inherited": true,
80-
"configFile": "lakefile.toml"},
8171
{"type": "path",
8272
"scope": "",
8373
"name": "Regex",
@@ -89,12 +79,22 @@
8979
"type": "git",
9080
"subDir": null,
9181
"scope": "leanprover-community",
92-
"rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
82+
"rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
9383
"name": "mathlib",
9484
"manifestFile": "lake-manifest.json",
95-
"inputRev": "v4.29.0",
85+
"inputRev": "v4.31.0",
9686
"inherited": true,
9787
"configFile": "lakefile.lean"},
88+
{"url": "https://github.com/leanprover-community/plausible",
89+
"type": "git",
90+
"subDir": null,
91+
"scope": "leanprover-community",
92+
"rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
93+
"name": "plausible",
94+
"manifestFile": "lake-manifest.json",
95+
"inputRev": "main",
96+
"inherited": true,
97+
"configFile": "lakefile.toml"},
9898
{"url": "https://github.com/leanprover-community/LeanSearchClient",
9999
"type": "git",
100100
"subDir": null,
@@ -109,7 +109,7 @@
109109
"type": "git",
110110
"subDir": null,
111111
"scope": "leanprover-community",
112-
"rev": "48d5698bc464786347c1b0d859b18f938420f060",
112+
"rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
113113
"name": "importGraph",
114114
"manifestFile": "lake-manifest.json",
115115
"inputRev": "main",
@@ -119,17 +119,17 @@
119119
"type": "git",
120120
"subDir": null,
121121
"scope": "leanprover-community",
122-
"rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
122+
"rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
123123
"name": "proofwidgets",
124124
"manifestFile": "lake-manifest.json",
125-
"inputRev": "v0.0.95",
125+
"inputRev": "main",
126126
"inherited": true,
127127
"configFile": "lakefile.lean"},
128128
{"url": "https://github.com/leanprover-community/aesop",
129129
"type": "git",
130130
"subDir": null,
131131
"scope": "leanprover-community",
132-
"rev": "7152850e7b216a0d409701617721b6e469d34bf6",
132+
"rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
133133
"name": "aesop",
134134
"manifestFile": "lake-manifest.json",
135135
"inputRev": "master",
@@ -139,7 +139,7 @@
139139
"type": "git",
140140
"subDir": null,
141141
"scope": "leanprover-community",
142-
"rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
142+
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
143143
"name": "Qq",
144144
"manifestFile": "lake-manifest.json",
145145
"inputRev": "master",
@@ -149,11 +149,12 @@
149149
"type": "git",
150150
"subDir": null,
151151
"scope": "leanprover-community",
152-
"rev": "756e3321fd3b02a85ffda19fef789916223e578c",
152+
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
153153
"name": "batteries",
154154
"manifestFile": "lake-manifest.json",
155155
"inputRev": "main",
156156
"inherited": true,
157157
"configFile": "lakefile.toml"}],
158158
"name": "RegexDoc",
159-
"lakeDir": ".lake"}
159+
"lakeDir": ".lake",
160+
"fixedToolchain": false}

docbuild/lakefile.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,4 @@ path = "../correctness"
1010
[[require]]
1111
scope = "leanprover"
1212
name = "doc-gen4"
13-
rev = "v4.29.0"
13+
rev = "v4.31.0"

docbuild/lean-toolchain

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

0 commit comments

Comments
 (0)