From b5cdcbf1642c10873709daad9e57d5c409715782 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 17 Dec 2024 14:51:27 +0100 Subject: [PATCH] wip: heuristically render Markdown in docstrings --- doc/UsersGuide/Basic.lean | 10 + src/verso-manual/VersoManual.lean | 2 +- src/verso-manual/VersoManual/Docstring.lean | 221 ++++++++++++++++++-- src/verso-manual/VersoManual/Markdown.lean | 65 ++++-- src/verso-manual/VersoManual/TeX.lean | 3 + src/verso/Verso/Doc/Elab/Monad.lean | 4 + src/verso/Verso/Doc/TeX.lean | 2 +- 7 files changed, 266 insertions(+), 41 deletions(-) diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index da15dfe..1bd2c1f 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -53,6 +53,16 @@ results in {docstring List.forM} +## More Docstring Examples + +{docstring String} + +{docstring Subtype} + +{docstring OfNat} + +{docstring Monad} + # Index %%% number := false diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index a9d5489..721c8aa 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -285,7 +285,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con (extraJsFiles := config.extraJs.toArray ++ state.extraJsFiles.map ("/-verso-js/" ++ ·.1)) def Config.relativize (config : Config) (path : Path) (html : Html) : Html := - if let some _ := config.baseURL then + if config.baseURL.isSome then -- Make all absolute URLS be relative to the site root, because that'll make them `base`-relative Html.relativize #[] html else diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 09b2469..86c6e20 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -352,6 +352,14 @@ def docstring (name : Name) (declType : Docstring.DeclType) (signature : Option name := `Verso.Genre.Manual.Block.docstring data := ToJson.toJson (name, declType, signature) +def docstringSection (header : String) : Block where + name := `Verso.Genre.Manual.Block.docstringSection + data := ToJson.toJson header + +def internalSignature (name : Highlighted) (signature : Option Highlighted) : Block where + name := `Verso.Genre.Manual.Block.internalSignature + data := ToJson.toJson (name, signature) + end Block @@ -470,6 +478,21 @@ def docstringStyle := r#" padding-right: 1rem; } +.namedocs .subdocs .name-and-type { + font-size: 1rem; + margin-left: 0; + margin-top: 0; + margin-right: 0; + margin-bottom: 0.5rem; +} + +.namedocs .subdocs .docs { + margin-left: 1.5rem; + margin-top: 0; + margin-right: 0; + margin-bottom: 0.5rem; +} + .namedocs:has(input[data-parent-idx]) tr[data-inherited-from] { transition-property: opacity, display; transition-duration: 0.4s; @@ -498,6 +521,46 @@ where " +open Verso.Genre.Manual.Markdown in +@[block_extension Block.docstringSection] +def docstringSection.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := none + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok header := FromJson.fromJson? (α := String) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + return {{ +

{{header}}

+ {{← contents.mapM goB}} + }} + +open Verso.Genre.Manual.Markdown in +@[block_extension Block.internalSignature] +def internalSignature.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok (name, signature) := FromJson.fromJson? (α := Highlighted × Option Highlighted) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + return {{ +
+ 
+            {{← name.toHtml}}
+            {{← if let some s := signature then do
+                  pure {{" : " {{← s.toHtml}} }}
+                else pure .empty}}
+
+
+ {{← contents.mapM goB}} +
+
+ }} + + open Verso.Genre.Manual.Markdown in @[block_extension Block.docstring] def docstring.descr : BlockDescr where @@ -601,22 +664,8 @@ where }} }} - let ctorRow ← - if isPrivateName ctor.name then - pure Html.empty - else pure {{ -

{{if isClass then "Instance Constructor" else "Constructor"}}

- - - {{ ← if let some d := ctor.docstring? then do - pure {{}} - else pure Html.empty - }} -
{{← ctor.hlName.toHtml}}
{{← md2html goB d}}
- }} let infos := infos.filter (·.subobject?.isNone) pure {{ - {{ ctorRow }} {{ parentRow }}

{{if isClass then "Methods" else "Fields"}}

@@ -700,9 +749,117 @@ where } modify (·.saveDomainObject docstringDomain name.toString id) - open Verso.Doc.Elab +def leanFromMarkdown := () + +def Inline.leanFromMarkdown (hls : Highlighted) : Inline where + name := ``Verso.Genre.Manual.leanFromMarkdown + data := ToJson.toJson hls + + +@[inline_extension leanFromMarkdown] +def leanFromMarkdown.inlinedescr : InlineDescr where + traverse id data _ := pure none + toTeX := + some <| fun go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output Html in + open Verso.Doc.Html in + some <| fun _ _ data _ => do + match FromJson.fromJson? data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.inlineHtml "docstring-examples" + +open Lean Elab Term in +def tryElabInlineCodeTerm (decl : Name) (str : String) : DocElabM Term := do + dbg_trace "HELLO! {decl} |{str}|" + + match Parser.runParserCategory (← getEnv) `term str s!"" with + | .error e => throw (.error (← getRef) e) + | .ok stx => + dbg_trace "PARSED |{stx}|" + let (newMsgs, tree) ← do + let initMsgs ← Core.getMessageLog + try + Core.resetMessageLog + -- TODO open decls/current namespace + let tree' ← fun _ => do + dbg_trace "Gonna elab..." + let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none + dbg_trace "ELAB'ED! |{e}|" + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← Term.levelMVarToParam (← instantiateMVars e) + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← instantiateMVars e' + dbg_trace "ELAB'ED MORE! |{e'}|" + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + pure <| InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees) + pure (← Core.getMessageLog, tree') + finally + Core.setMessageLog initMsgs + if newMsgs.hasErrors then + for msg in newMsgs.errorsToWarnings.toArray do + logMessage msg + + let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) + + logInfoAt (← getRef) stx + + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) + + +open Lean Elab Term in +def tryElabInlineCodeName (_decl : Name) (str : String) : DocElabM Term := do + let str := str.trim + let x := str.toName + if x.toString == str then + let stx := mkIdent x + let n ← realizeGlobalConstNoOverload stx + let hl : Highlighted ← constTok n str + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) + else + throwError "Not a name: '{str}'" +where + constTok {m} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] + (name : Name) (str : String) : + m Highlighted := do + let docs ← findDocString? (← getEnv) name + let sig := toString (← (PrettyPrinter.ppSignature name)).1 + pure <| .token ⟨.const name sig docs false, str⟩ + +open Lean Elab Term in +def tryElabInlineCode (decl : Name) (str : String) : DocElabM Term := do + -- This brings the parameters into scope, so the term elaboration version catches them! + Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => + try + tryElabInlineCodeName decl str <|> + tryElabInlineCodeTerm decl str + catch + | .error ref e => + logWarningAt ref e + ``(Verso.Doc.Inline.code $(quote str)) + | e => + logWarning m!"Internal exception uncaught: {e.toMessageData}" + ``(Verso.Doc.Inline.code $(quote str)) + +def blockFromMarkdownWithLean (name : Name) (b : MD4Lean.Block) : DocElabM Term := + Markdown.blockFromMarkdown b + (handleHeaders := Markdown.strongEmphHeaders) + (elabInlineCode := tryElabInlineCode name) + @[block_role_expander docstring] def docstring : BlockRoleExpander | args, #[] => do @@ -710,12 +867,14 @@ def docstring : BlockRoleExpander | #[.anon (.name x)] => let name ← Elab.realizeGlobalConstNoOverloadWithInfo x Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation") - let blockStx ← match ← Lean.findDocString? (← getEnv) name with - | none => logWarningAt x m!"No docs found for '{x}'"; pure #[] - | some docs => - let some ast := MD4Lean.parse docs - | throwErrorAt x "Failed to parse docstring as Markdown" - ast.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + let blockStx ← + match ← Lean.findDocString? (← getEnv) name with + | none => logWarningAt x m!"No docs found for '{x}'"; pure #[] + | some docs => + let some ast := MD4Lean.parse docs + | throwErrorAt x "Failed to parse docstring as Markdown" + + ast.blocks.mapM (blockFromMarkdownWithLean name) if Lean.Linter.isDeprecated (← getEnv) name then logInfoAt x m!"'{x}' is deprecated" @@ -735,9 +894,25 @@ def docstring : BlockRoleExpander } let sig := Lean.Widget.tagCodeInfos ctx infos tt let signature ← some <$> renderTagged none sig ⟨{}, false⟩ - pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*])] + let extras ← getExtras declType + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*, $extras,*])] | _ => throwError "Expected exactly one positional argument that is a name" | _, more => throwErrorAt more[0]! "Unexpected block argument" +where + getExtras (declType : Block.Docstring.DeclType) : DocElabM (Array Term) := + match declType with + | .structure (isClass := isClass) (constructor := constructor) .. => do + let header := if isClass then "Instance Constructor" else "Constructor" + let sigDesc ← + if let some docs := constructor.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdownWithLean constructor.name) + else pure #[] + let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*]) + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig])] + | _ => pure #[] + def Block.optionDocs (name : Name) (defaultValue : Option Highlighted) : Block where name := `Verso.Genre.Manual.optionDocs @@ -783,7 +958,7 @@ def optionDocs : BlockRoleExpander Doc.PointOfInterest.save x optDecl.declName.toString let some mdAst := MD4Lean.parse optDecl.descr | throwErrorAt x "Failed to parse docstring as Markdown" - let contents ← mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean x.getId) pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])] | _, more => throwErrorAt more[0]! "Unexpected block argument" diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean index 74e151b..9c91e3e 100644 --- a/src/verso-manual/VersoManual/Markdown.lean +++ b/src/verso-manual/VersoManual/Markdown.lean @@ -25,6 +25,11 @@ generate nested `Part`s, but rather some custom node or some formatted text. private structure HeaderHandlers (m : Type u → Type w) (block : Type u) (inline : Type v) : Type (max u v w) where levels : List (Array inline → m block) := [] +structure MDContext (m : Type u → Type w) (block : Type u) (inline : Type u) : Type (max u w) where + headerHandlers : HeaderHandlers m block inline + elabInlineCode : Option (String → m inline) + elabBlockCode : Option (String → m block) + def attrText : AttrText → Except String String | .normal str => pure str | .nullchar => throw "Null character" @@ -40,7 +45,28 @@ def attr' (val : Array AttrText) : Except String String := do | .error e => .error e | .ok s => pure s -partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] : Text → m Term +private structure MDState where + /-- A mapping from document header levels to actual nesting levels -/ + inHeaders : List (Nat × Nat) := [] +deriving Inhabited + +private abbrev MDT m block inline α := ReaderT (MDContext m block inline) (StateT MDState m) α + +instance {block inline} [Monad m] : MonadLift m (MDT m block inline) where + monadLift act := fun _ s => act <&> (·, s) + +instance {block inline} [Monad m] [AddMessageContext m] : AddMessageContext (MDT m block inline) where + addMessageContext msg := (addMessageContext msg : m _) + + +instance {block inline} [AddMessageContext m] [Monad m] [MonadError m] : MonadError (MDT m block inline) where + throw e := throw (m := m) e + tryCatch a b := fun r s => do + tryCatch (a r s) fun e => b e r s + + + +partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [AddMessageContext m] [MonadError m] : Text → MDT m Term Term Term | .normal str | .br str | .softbr str => ``(Verso.Doc.Inline.text $(quote str)) | .nullchar => throwError "Unexpected null character in parsed Markdown" | .del _ => throwError "Unexpected strikethrough in parsed Markdown" @@ -50,7 +76,12 @@ partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] : Tex | .latexMath m => ``(Verso.Doc.Inline.math Verso.Doc.MathMode.inline $(quote <| String.join m.toList)) | .latexMathDisplay m => ``(Verso.Doc.Inline.math Verso.Doc.MathMode.display $(quote <| String.join m.toList)) | .u txt => throwError "Unexpected underline around {repr txt} in parsed Markdown" - | .code str => ``(Verso.Doc.Inline.code $(quote <| String.join str.toList)) + | .code strs => do + let str := String.join strs.toList + if let some f := (← read).elabInlineCode then + f str + else + ``(Verso.Doc.Inline.code $(quote str)) | .entity ent => throwError s!"Unsupported entity {ent} in parsed Markdown" | .img .. => throwError s!"Unexpected image in parsed Markdown" | .wikiLink .. => throwError s!"Unexpected wiki-style link in parsed Markdown" @@ -70,12 +101,6 @@ partial def inlineFromMarkdown' : Text → Except String (Doc.Inline g) | .img .. => .error s!"Unexpected image in parsed Markdown" | .wikiLink .. => .error s!"Unexpected wiki-style link in parsed Markdown" -private structure MDState where - /-- A mapping from document header levels to actual nesting levels -/ - inHeaders : List (Nat × Nat) := [] -deriving Inhabited - -private abbrev MDT m block inline α := ReaderT (HeaderHandlers m block inline) (StateT MDState m) α instance [Monad m] [MonadError m] : MonadError (MDT m b i) where throw ex := fun _ρ _σ => throw ex @@ -102,14 +127,16 @@ private partial def getHeaderLevel [Monad m] (level : Nat) : MDT m b i Nat := do private def getHeader [Monad m] (level : Nat) : MDT m b i (Except String (Array i → m b)) := do let lvl ← getHeaderLevel level - match (← read).levels.get? lvl with + match (← read).headerHandlers.levels.get? lvl with | none => pure (throw s!"Unexpected header with nesting level {lvl} in parsed Markdown") | some f => pure (pure f) -private partial def blockFromMarkdownAux [Monad m] [MonadQuotation m] [MonadError m] : MD4Lean.Block → MDT m Term Term Term +private partial def blockFromMarkdownAux [Monad m] [AddMessageContext m] [MonadQuotation m] [MonadError m] : MD4Lean.Block → MDT m Term Term Term | .p txt => do ``(Verso.Doc.Block.para #[$[$(← txt.mapM (inlineFromMarkdown ·))],*]) | .blockquote bs => do ``(Verso.Doc.Block.blockquote #[$[$(← bs.mapM blockFromMarkdownAux )],*]) - | .code _ _ _ strs => do ``(Verso.Doc.Block.code $(quote <| String.join strs.toList)) + | .code _ _ _ strs => do + let str := String.join strs.toList + ``(Verso.Doc.Block.code $(quote str)) | .ul _ _ items => do ``(Verso.Doc.Block.ul #[$[$(← items.mapM itemFromMarkdown)],*]) | .ol _ i _ items => do let itemStx ← items.mapM itemFromMarkdown @@ -129,10 +156,13 @@ where else ``(Verso.Doc.ListItem.mk 0 #[$[$(← item.contents.mapM blockFromMarkdownAux)],*]) -def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] +def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] [AddMessageContext m] (md : MD4Lean.Block) - (handleHeaders : List (Array Term → m Term) := []) : m Term := - (·.fst) <$> blockFromMarkdownAux md ⟨handleHeaders⟩ {} + (handleHeaders : List (Array Term → m Term) := []) + (elabInlineCode : Option (String → m Term) := none) + (elabBlockCode : Option (String → m Term) := none) : m Term := + let ctxt := {headerHandlers := ⟨handleHeaders⟩, elabInlineCode, elabBlockCode} + (·.fst) <$> blockFromMarkdownAux md ctxt {} def strongEmphHeaders [Monad m] [MonadQuotation m] : List (Array Term → m Term) := [ fun stxs => ``(Verso.Doc.Block.para #[Verso.Doc.Inline.bold #[$stxs,*]]), @@ -162,8 +192,11 @@ where def blockFromMarkdown' (md : MD4Lean.Block) - (handleHeaders : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := []) : Except String (Doc.Block g) := - (·.fst) <$> blockFromMarkdownAux' md ⟨handleHeaders⟩ {} + (handleHeaders : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := []) + (elabInlineCode : Option (String → Except String (Doc.Inline g)) := none) + (elabBlockCode : Option (String → Except String (Doc.Block g)) := none) : + Except String (Doc.Block g) := + (·.fst) <$> blockFromMarkdownAux' md ⟨⟨handleHeaders⟩, elabInlineCode, elabBlockCode⟩ {} def strongEmphHeaders' : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := [ fun inls => pure <| .para #[.bold inls], diff --git a/src/verso-manual/VersoManual/TeX.lean b/src/verso-manual/VersoManual/TeX.lean index 845ea43..66cdc9d 100644 --- a/src/verso-manual/VersoManual/TeX.lean +++ b/src/verso-manual/VersoManual/TeX.lean @@ -14,6 +14,9 @@ r##" \usepackage{sourcesanspro} \usepackage{sourceserifpro} +\usepackage{fancyvrb} +\usepackage{fvextra} + \makechapterstyle{lean}{% \renewcommand*{\chaptitlefont}{\sffamily\HUGE} \renewcommand*{\chapnumfont}{\chaptitlefont} diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index b2ba9e1..93144a4 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -336,6 +336,10 @@ instance : MonadQuotation DocElabM := inferInstanceAs <| MonadQuotation (ReaderT instance : Monad DocElabM := inferInstanceAs <| Monad (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) +instance : MonadControl TermElabM DocElabM := + let ⟨stM, liftWith, restoreM⟩ := inferInstanceAs <| MonadControlT TermElabM (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) + {stM, liftWith, restoreM := (· >>= restoreM)} + instance : MonadExceptOf Exception DocElabM := inferInstanceAs <| MonadExceptOf Exception (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) instance : MonadAlwaysExcept Exception DocElabM := inferInstanceAs <| MonadAlwaysExcept Exception (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean index e3c5323..8363d06 100644 --- a/src/verso/Verso/Doc/TeX.lean +++ b/src/verso/Verso/Doc/TeX.lean @@ -74,7 +74,7 @@ partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m | .bold content => do pure \TeX{\textbf{\Lean{← content.mapM toTeX}}} | .code str => do - pure \TeX{s!"\\verb|{str}|"} --- TODO choose delimiter automatically + pure \TeX{s!"\\Verb|{str}|"} --- TODO choose delimiter automatically | .math .inline str => pure <| .raw s!"${str}$" | .math .display str => pure <| .raw s!"\\[{str}\\]" | .concat inlines => inlines.mapM toTeX