From ef2866f6fc4868617e26ace55d1614cef72f5da8 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 18 Jun 2026 16:43:54 -0400 Subject: [PATCH 1/6] Full working(?) versobox shim --- src/verso-manual/VersoManual.lean | 92 ++++++++++++++++++++++++++ src/verso-manual/VersoManual/Html.lean | 29 ++++++++ src/verso/Verso/Doc/Concrete.lean | 4 ++ src/verso/Verso/Doc/DocName.lean | 3 + 4 files changed, 128 insertions(+) diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index c252c5779..30ba47d23 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -1045,3 +1045,95 @@ where emit cfg text traverseState for step in extraSteps do step .single cfg.toConfig traverseState text + + + + +section HtmlRPC +/-! +What we *are* doing: doc finalizer elaborates and stores HTML string in +environment extension, RPC retrieves string from environment extension. + +What we *should be* doing: + - Verso is proactively storing a representation of the document in an + environment extension + - The RPC is looking up that representation of the document, incurring the + cost of elaboration and translation to an HTML string, and returning that +-/ + +open Lean + +/-! The environment extension in question -/ + +inductive VersoDocumentData where + | success : String → VersoDocumentData + | errors : Array String → VersoDocumentData +deriving ToJson, FromJson + +initialize versoDocumentExt : EnvExtension (Option VersoDocumentData) ← + registerEnvExtension (pure .none) + +/-! Alternative route to HTML output -/ + +def shortcutToHtml (extensionImpls : ExtensionImpls) (part : Lean.Doc.Part Genre.Manual.Inline Genre.Manual.Block Genre.Manual.PartMetadata) : IO VersoDocumentData := do + let (logs, result) ← runWithLogs do + let (part, traverseState) ← traverse part { htmlDepth := 0 } + let contentGenerator : StateT (State Html) (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Html := do + Manual.toHtml {} {} traverseState (traverseState.definitionIds {}) {} {} part + let (html, htmlState) ← contentGenerator |>.run .empty |>.run {} + + let featureJsFiles := + traverseState.features.toArray.flatMap fun f => + f.jsFilePaths.map fun (name, defer) => ("/verso/view/-verso-data/" ++ name, defer) + let extraJsFiles := + sortJs <| + traverseState.extraJsFiles.toArray.map (false, ·.toStaticJsFile) + let extraJsFiles := featureJsFiles ++ extraJsFiles.map fun + | (true, f) => (f.filename, f.defer) + | (false, f) => ("/verso/view/-verso-data/" ++ f.filename, f.defer) + let cssFiles := + traverseState.extraCssFiles.toArray.map (·.filename) ++ + traverseState.features.toArray.flatMap (fun f => f.cssFilePaths) + + let page := Html.standalonePage html htmlState.dedup.docJson + (extraJsFiles := extraJsFiles) + (extraStylesheets := cssFiles.toList.map ("/verso/view/-verso-data/" ++ ·)) + return Html.doctype ++ page.asString + if logs.size > 0 then + return .errors (logs.map (·.format)) + return .success result +where + runWithLogs {a} (act : ReaderT ExtensionImpls (BuildLogT IO) a) : IO (Array LogMessage × a) := do + let logger ← Logger.new + let result ← ReaderT.run act extensionImpls |> (ReaderT.run · logger) + return (← logger.errors, result) + +/-! When the document is finished parsing, generate HTML and put it in the extension -/ + +open Elab.Command in +def putDocInContext (doc : VersoDocumentData) : CommandElabM Unit := do + modifyEnv (versoDocumentExt.setState · (.some doc)) + +section RPC +open Elab.Command Server + +@[doc_finalize] +unsafe def liveDocFinalizer : CommandElabM Unit := do + let name := docName (← getEnv).mainModule + let versoDoc ← liftTermElabM <| evalConst (VersoDoc Manual) name + let htmlDoc ← shortcutToHtml (by exact extension_impls%) (versoDoc.toPart) + putDocInContext htmlDoc + +@[server_rpc_method] +def _root_.Verso.getLiveDocument (_ : Unit) : RequestM (RequestTask VersoDocumentData) := do + let doc ← RequestM.readDoc + let endPos := doc.meta.text.source.rawEndPos + RequestM.withWaitFindSnap doc (·.endPos >= endPos) (notFoundX := pure (.errors #["notFoundX???"])) + fun snap => + match versoDocumentExt.getState snap.env with + | .none => return .errors #["No document here"] + | .some s => + return s + +end RPC +end HtmlRPC diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index 492ffdc85..b0c206a88 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -516,6 +516,35 @@ public def page }} +public def standalonePage (contents : Html) (highlightingJson : Lean.Json) + (extraJsFiles : Array (String × Bool) := #[]) + (extraStylesheets : List String := []) := + let defer := #[("defer", "defer")] + {{ + + + + + + {{"Verso Document"}} + + + + {{extraJsFiles.map fun f => ({{}})}} + {{extraStylesheets.map (fun url => {{ }})}} + + + + +
+
+ {{contents}} +
+
+ + + }} + public def relativize (path : Path) (html : Html) : Html := html.visitM (m := ReaderT Path Id) (tag := rwTag) |>.run path diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index 29a7ea531..c2206e84d 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -13,6 +13,7 @@ public import Verso.Doc.Elab public meta import Verso.Doc.Elab.Monad import Verso.Doc.Concrete.InlineString import Verso.Doc.Lsp +public meta import Verso.Doc.Elab.Finalize namespace Verso.Doc.Concrete @@ -396,6 +397,7 @@ elab_rules : command -- so we detect that case and call finishDoc. if stopPos.extract txt.source txt.source.rawEndPos |>.all Char.isWhitespace then finishDoc + Finalize.runFinalizers open Command in /-- @@ -423,4 +425,6 @@ public meta def elabVersoLastBlock : Command.CommandElab runVersoBlock b -- Finish up the document finishDoc + Finalize.runFinalizers | _ => throwUnsupportedSyntax + diff --git a/src/verso/Verso/Doc/DocName.lean b/src/verso/Verso/Doc/DocName.lean index 074320d98..9d6863353 100644 --- a/src/verso/Verso/Doc/DocName.lean +++ b/src/verso/Verso/Doc/DocName.lean @@ -16,5 +16,8 @@ open Lean @[match_pattern] private def versoModuleDocNameString : String := "the canonical document object name" + public def docName (moduleName : Name) : Name := id <| .str moduleName versoModuleDocNameString + +#eval docName `Module From 019e0892912f8230e276a63c26eef1d5f9f4b0a8 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 18 Jun 2026 16:53:01 -0400 Subject: [PATCH 2/6] Add missing file --- src/verso/Verso/Doc/Elab/Finalize.lean | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 src/verso/Verso/Doc/Elab/Finalize.lean diff --git a/src/verso/Verso/Doc/Elab/Finalize.lean b/src/verso/Verso/Doc/Elab/Finalize.lean new file mode 100644 index 000000000..41bdb880f --- /dev/null +++ b/src/verso/Verso/Doc/Elab/Finalize.lean @@ -0,0 +1,25 @@ +module +public import Lean +import Verso.Doc + +open Lean +namespace Verso.Doc.Elab.Finalize + +public meta initialize docFinalizeAttr : TagAttribute ← + registerTagAttribute `doc_finalize "Indicate to Verso that this function should be run on documents post-parsing" fun declName => do + let decl ← getConstInfo declName + match decl.type with + | (.app (.const ``Elab.Command.CommandElabM []) (.const ``Unit [])) => return + | _ => throwError "Decl does not have type `CommandElabM Unit` expected for a document finalizer" + +meta def runFinalizer (finalizerName : Name) : Elab.Command.CommandElabM Unit := do + let finalizer := mkIdent finalizerName + Elab.Command.elabCommand (← `(#eval $finalizer)) + +public meta def runFinalizers : Elab.Command.CommandElabM Unit := do + let state := docFinalizeAttr.ext.toEnvExtension.getState (← getEnv) + for list in state.importedEntries do + for finalizerName in list do + runFinalizer finalizerName + for finalizerName in state.state do + runFinalizer finalizerName From 4dcf3e7de7321969ca96082b29a3efdeff34ac6c Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 18 Jun 2026 20:51:29 -0400 Subject: [PATCH 3/6] diff hacking --- src/verso/Verso/Doc/DocName.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/verso/Verso/Doc/DocName.lean b/src/verso/Verso/Doc/DocName.lean index 9d6863353..a5ba2a0c0 100644 --- a/src/verso/Verso/Doc/DocName.lean +++ b/src/verso/Verso/Doc/DocName.lean @@ -19,5 +19,3 @@ private def versoModuleDocNameString : String := "the canonical document object public def docName (moduleName : Name) : Name := id <| .str moduleName versoModuleDocNameString - -#eval docName `Module From bd9ae7fcc317e8d27ddc975babe77b1b4701f059 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 18 Jun 2026 20:51:47 -0400 Subject: [PATCH 4/6] diff hacking --- src/verso/Verso/Doc/DocName.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/verso/Verso/Doc/DocName.lean b/src/verso/Verso/Doc/DocName.lean index a5ba2a0c0..074320d98 100644 --- a/src/verso/Verso/Doc/DocName.lean +++ b/src/verso/Verso/Doc/DocName.lean @@ -16,6 +16,5 @@ open Lean @[match_pattern] private def versoModuleDocNameString : String := "the canonical document object name" - public def docName (moduleName : Name) : Name := id <| .str moduleName versoModuleDocNameString From 50a005062e8503aebf148ecb6160ecc7d84d0720 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 18 Jun 2026 20:52:13 -0400 Subject: [PATCH 5/6] diff hacking --- src/verso/Verso/Doc/Concrete.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index c2206e84d..e0cecb59c 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -427,4 +427,3 @@ public meta def elabVersoLastBlock : Command.CommandElab finishDoc Finalize.runFinalizers | _ => throwUnsupportedSyntax - From 4dcbbbc79d41b313af3ab32e9ddb9cf57571427e Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 19 Jun 2026 17:05:23 -0400 Subject: [PATCH 6/6] Slightly better error messages --- src/verso-manual/VersoManual.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index 30ba47d23..699394fd6 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -1068,6 +1068,7 @@ open Lean inductive VersoDocumentData where | success : String → VersoDocumentData | errors : Array String → VersoDocumentData + | noDoc : VersoDocumentData deriving ToJson, FromJson initialize versoDocumentExt : EnvExtension (Option VersoDocumentData) ← @@ -1128,10 +1129,10 @@ unsafe def liveDocFinalizer : CommandElabM Unit := do def _root_.Verso.getLiveDocument (_ : Unit) : RequestM (RequestTask VersoDocumentData) := do let doc ← RequestM.readDoc let endPos := doc.meta.text.source.rawEndPos - RequestM.withWaitFindSnap doc (·.endPos >= endPos) (notFoundX := pure (.errors #["notFoundX???"])) + RequestM.withWaitFindSnap doc (·.endPos >= endPos) (notFoundX := pure (.errors #["Internal invariant violated: notFoundX"])) fun snap => match versoDocumentExt.getState snap.env with - | .none => return .errors #["No document here"] + | .none => return .noDoc | .some s => return s