Skip to content

Commit 75cea3e

Browse files
authored
chore: bump toolchain to lean v4.26.0-rc2 and update to latest verso (#198)
1 parent 1ae3091 commit 75cea3e

File tree

4 files changed

+17
-7
lines changed

4 files changed

+17
-7
lines changed

book/Main.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ def config : Config where
1515
emitHtmlMulti := true
1616
htmlDepth := 1
1717
extraFiles := [("static", "static")]
18-
extraCss := [
18+
extraCss := Std.HashSet.ofList [
1919
"/static/theme.css",
2020
"/static/fonts/source-serif/source-serif-text.css",
2121
"/static/fonts/source-code-pro/source-code-pro.css",

book/TPiL/Examples.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -746,8 +746,8 @@ block_extension Block.goals (goals : Array (Highlighted.Goal Highlighted))
746746
{{← if goals.isEmpty then
747747
pure {{"All goals completed! 🐙"}}
748748
else
749-
withCollapsedSubgoals .never <|
750-
.seq <$> goals.mapIndexedM (fun ⟨i, _⟩ x => x.toHtml (g := Verso.Genre.Manual) (·.toHtml) i)}}
749+
withCollapsedSubgoals (g := Verso.Genre.Manual) .never <|
750+
.seq <$> (goals.mapIdxM (fun i x => x.toHtml (·.toHtml) i))}}
751751
</span>
752752
</div>
753753
}}

book/lake-manifest.json

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,27 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "b1cdd66be1f055926796aa804fdc13c9e9ac17c6",
8+
"rev": "bc7bf09465ec53856c2b0fcc3f847af342254238",
99
"name": "verso",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
1424
{"url": "https://github.com/acmepjz/md4lean",
1525
"type": "git",
1626
"subDir": null,
1727
"scope": "",
18-
"rev": "66aefec2852d3e229517694e642659f316576591",
28+
"rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
1929
"name": "MD4Lean",
2030
"manifestFile": "lake-manifest.json",
2131
"inputRev": "main",
@@ -25,7 +35,7 @@
2535
"type": "git",
2636
"subDir": null,
2737
"scope": "",
28-
"rev": "57f4e6c99a4132d54a2105dec21c2e3c2af98b15",
38+
"rev": "08f238aa4e015b7609648369ae64cde26286d115",
2939
"name": "subverso",
3040
"manifestFile": "lake-manifest.json",
3141
"inputRev": "main",

book/lean-toolchain

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

0 commit comments

Comments
 (0)