From be3c211b0a7a9a22191aadb19a3ed3ee5f770ec0 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 14:53:07 +0200 Subject: [PATCH 1/3] perf: batch-highlighting of code This PR migrates more of Verso to the highlightMany API of SubVerso, allowing it to share more caches when highlighting longer chains of commands. It relies on a SubVerso PR, and shouldn't be merged until the SubVerso PR is merged. There is also a change to a proof. With this change, the library works on Lean 4.33 as well, which is important for a downstream user who needs these changes but can't get to latest Lean release candidate. --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- src/multi-verso/MultiVerso/NameMap.lean | 3 +-- src/verso-manual/VersoManual/InlineLean.lean | 19 ++++++++++++++----- 4 files changed, 18 insertions(+), 10 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 34ac03a9..18bb51d1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "847084e80500726e4331dded5f17007ddaf89c31", + "rev": "10caddf4d067ad0f916cbf231f2870a08977124e", "name": "subverso", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "sfl-local", "inherited": false, "configFile": "lakefile.lean"}], "name": "verso", diff --git a/lakefile.lean b/lakefile.lean index ade9bbab..fd98f858 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -require subverso from git "https://github.com/leanprover/subverso"@"main" +require subverso from git "https://github.com/leanprover/subverso"@"sfl-local" require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main" require plausible from git "https://github.com/leanprover-community/plausible"@"main" require illuminate from git "https://github.com/leanprover/illuminate"@"main" diff --git a/src/multi-verso/MultiVerso/NameMap.lean b/src/multi-verso/MultiVerso/NameMap.lean index c73370ce..c12f3f98 100644 --- a/src/multi-verso/MultiVerso/NameMap.lean +++ b/src/multi-verso/MultiVerso/NameMap.lean @@ -233,8 +233,7 @@ public instance : GetElem? (NameMap α) Name α fun xs n => n ∈ xs where getElem xs x ok := if h : isPublic x then show α from GetElem.getElem (coll := TreeMap PublicName α PublicName.quickCmp) (idx := PublicName) (elem := α) (valid := fun xs x => x ∈ xs) xs ⟨x, h⟩ <| by - simp only [Membership.mem, h, dite_eq_left_of_eq_true] at ok - exact ok + simpa [Membership.mem, h] using ok else False.elim <| by simp only [Membership.mem, h] at ok diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 65c466c9..3a18e5c0 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -275,6 +275,7 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit) let mut cmdState : Command.State := { env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := origScopes } let mut pstate := { pos := startPos, recovering := false, hasLeading := false } let mut cmds := #[] + let mut cmdTrees : Array (Option Lean.Elab.InfoTree) := #[] repeat let scope := cmdState.scopes.head! @@ -291,6 +292,13 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit) let savedTrees := cmdState.infoState.trees cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) <| runCommand (Command.elabCommandTopLevel cmd) cmd cctx cmdState + -- `elabCommandTopLevel` reset the info state, so the trees present now are exactly this + -- command's; record them for the batched highlighting pass below. + cmdTrees := cmdTrees.push <| + match cmdState.infoState.trees.toArray with + | #[t] => some t + | #[] => none + | ts => some (.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd}) ts.toPArray') cmdState := { cmdState with messages := savedMsgs ++ cmdState.messages, infoState := { cmdState.infoState with trees := savedTrees ++ cmdState.infoState.trees } @@ -319,12 +327,13 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit) pushInfoTree (disableUnusedVarLinterInInfoTree t) - let mut hls := Highlighted.empty let nonSilentMsgs := cmdState.messages.toArray.filter (!·.isSilent) - let mut lastPos : String.Pos.Raw := startPos - for cmd in cmds do - hls := hls ++ (← highlightIncludingUnparsed cmd nonSilentMsgs cmdState.infoState.trees (startPos? := lastPos)) - lastPos := (cmd.getTrailingTailPos?).getD lastPos + -- One batched highlighting pass shares the alias-table and info-table setup across the + -- whole block's commands. Unparsed regions (e.g. text skipped by parse-error recovery) + -- are included in the output verbatim. + let hlArr ← highlightMany cmds nonSilentMsgs cmdTrees + (includeUnparsed := true) (startPos? := some startPos) + let hls := hlArr.foldl (· ++ ·) Highlighted.empty toHighlightedLeanContent config.show hls str finally From fdd9171979d779818ca89f508596ae29e76e60d7 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Aug 2026 17:07:52 +0200 Subject: [PATCH 2/3] Apply suggestion from @david-christiansen --- src/verso-manual/VersoManual/InlineLean.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 3a18e5c0..a93054b3 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -328,9 +328,7 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit) let nonSilentMsgs := cmdState.messages.toArray.filter (!·.isSilent) - -- One batched highlighting pass shares the alias-table and info-table setup across the - -- whole block's commands. Unparsed regions (e.g. text skipped by parse-error recovery) - -- are included in the output verbatim. + -- One batched highlighting pass shares caches between the whole block's commands. let hlArr ← highlightMany cmds nonSilentMsgs cmdTrees (includeUnparsed := true) (startPos? := some startPos) let hls := hlArr.foldl (· ++ ·) Highlighted.empty From 851769d008da8d9e8c53faf08e91b29c1cc7da47 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 24 Aug 2026 11:07:57 +0200 Subject: [PATCH 3/3] use main subverso --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- test-projects/anchor-examples/lake-manifest.json | 2 +- test-projects/documented-package/lake-manifest.json | 2 +- test-projects/website-examples/lake-manifest.json | 2 +- test-projects/website-literate/lake-manifest.json | 2 +- 6 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 18bb51d1..b09747fa 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "10caddf4d067ad0f916cbf231f2870a08977124e", + "rev": "fda188f7329fa18ce4b2e8cc96c9b0a8f0c78c46", "name": "subverso", "manifestFile": "lake-manifest.json", - "inputRev": "sfl-local", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}], "name": "verso", diff --git a/lakefile.lean b/lakefile.lean index fd98f858..ade9bbab 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -require subverso from git "https://github.com/leanprover/subverso"@"sfl-local" +require subverso from git "https://github.com/leanprover/subverso"@"main" require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main" require plausible from git "https://github.com/leanprover-community/plausible"@"main" require illuminate from git "https://github.com/leanprover/illuminate"@"main" diff --git a/test-projects/anchor-examples/lake-manifest.json b/test-projects/anchor-examples/lake-manifest.json index b3e2fb9b..507c32bc 100644 --- a/test-projects/anchor-examples/lake-manifest.json +++ b/test-projects/anchor-examples/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ea0dc0d7f5c725f64f20aecb44d90c6fbf59ee14", + "rev": "273e19499ee764e020f878b7a45c6a9555ecf10c", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test-projects/documented-package/lake-manifest.json b/test-projects/documented-package/lake-manifest.json index caf9e80a..071bd0a1 100644 --- a/test-projects/documented-package/lake-manifest.json +++ b/test-projects/documented-package/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ea0dc0d7f5c725f64f20aecb44d90c6fbf59ee14", + "rev": "273e19499ee764e020f878b7a45c6a9555ecf10c", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test-projects/website-examples/lake-manifest.json b/test-projects/website-examples/lake-manifest.json index ab01766b..4f31a4d9 100644 --- a/test-projects/website-examples/lake-manifest.json +++ b/test-projects/website-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "ea0dc0d7f5c725f64f20aecb44d90c6fbf59ee14", + "rev": "273e19499ee764e020f878b7a45c6a9555ecf10c", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test-projects/website-literate/lake-manifest.json b/test-projects/website-literate/lake-manifest.json index b8a84867..6393daef 100644 --- a/test-projects/website-literate/lake-manifest.json +++ b/test-projects/website-literate/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ea0dc0d7f5c725f64f20aecb44d90c6fbf59ee14", + "rev": "273e19499ee764e020f878b7a45c6a9555ecf10c", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main",