From a71fb6d4153ff528186aef3df20732076f71509f Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Thu, 5 Jun 2025 08:59:23 +0200 Subject: [PATCH 1/5] Feature: Convert docComment for LiterateLean --- .../VersoBlog/LiterateLeanPage.lean | 33 +++++++++++++++++-- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 9fae21a30..24af44f70 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -312,19 +312,24 @@ section variable [Monad m] [MonadError m] [MonadQuotation m] -partial def getModuleDocString (hl : Highlighted) : m String := do + +partial def getCommentString (pref : String) (hl : Highlighted) : m String := do let str := (← getString hl).trim - let str := str.stripPrefix "/-!" |>.stripSuffix "-/" |>.trim + let str := str.stripPrefix pref |>.stripSuffix "-/" |>.trim pure str where getString : Highlighted → m String | .text txt => pure txt | .tactics .. => throwError "Tactics found in module docstring!" | .point .. => pure "" - | .span _ hl => getModuleDocString hl + | .span _ hl => getCommentString pref hl | .seq hls => do return (← hls.mapM getString).foldl (init := "") (· ++ ·) | .token ⟨_, txt⟩ => pure txt + +partial def getModuleDocString : Highlighted -> m String := getCommentString "/-!" +partial def getDocCommentString : Highlighted -> m String := getCommentString "/--" end + def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × String) | .span msgs x => msgs[0]? <|> getFirstMessage x @@ -394,6 +399,28 @@ partial def docFromMod (project : System.FilePath) (mod : String) } | other => addBlock (← ofBlock helper other) + | ``declaration => + match code with + | .seq s => + -- Find the index corresponding to the docComment + let docCommentIdx := s.findIdx? (fun + | (.token ⟨.docComment, _⟩) => True + | _ => false) + match docCommentIdx with + | some i => + let str ← getDocCommentString s[i]! + let codeBefore := Highlighted.seq s[:i] + addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote codeBefore)) Array.mkArray0)) + let some ⟨mdBlocks⟩ := MD4Lean.parse str + | throwError m!"Failed to parse Markdown: {str}" + for b in mdBlocks do + addBlock (← ofBlock helper b) + let codeAfter := Highlighted.seq s[i+1:] + addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote codeAfter)) Array.mkArray0)) + | none => + -- No docComment attached to declaration, render definition as usual + addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) + | _ => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) | ``eval | ``evalBang | ``reduceCmd | ``print | ``printAxioms | ``printEqns | ``«where» | ``version | ``synth | ``check => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) if let some (k, msg) := getFirstMessage code then From ca480d98ba3cee064b9c6ce2b8461f3e84269267 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Sat, 7 Jun 2025 11:30:27 +0200 Subject: [PATCH 2/5] Add div around literate docComments --- src/verso-blog/VersoBlog/LiterateLeanPage.lean | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 24af44f70..95003312c 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -408,15 +408,14 @@ partial def docFromMod (project : System.FilePath) (mod : String) | _ => false) match docCommentIdx with | some i => - let str ← getDocCommentString s[i]! - let codeBefore := Highlighted.seq s[:i] - addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote codeBefore)) Array.mkArray0)) - let some ⟨mdBlocks⟩ := MD4Lean.parse str - | throwError m!"Failed to parse Markdown: {str}" - for b in mdBlocks do - addBlock (← ofBlock helper b) - let codeAfter := Highlighted.seq s[i+1:] - addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote codeAfter)) Array.mkArray0)) + let codeBefore ← ``(Block.other + (BlockExt.highlightedCode `name $(quote (Highlighted.seq s[:i]))) Array.mkArray0) + let some ⟨mdBlocks⟩ := MD4Lean.parse (← getDocCommentString s[i]!) + | throwError m!"Failed to parse Markdown: {← getDocCommentString s[i]!}" + let docCommentBlocks ← mdBlocks.mapM (fun b => ofBlock helper b) + let codeAfter ←``(Block.other (BlockExt.highlightedCode `name $(quote (Highlighted.seq s[i+1:]))) Array.mkArray0) + let blocks := #[codeBefore] ++ docCommentBlocks ++ #[codeAfter] + addBlock (← ``(Block.other (BlockExt.htmlDiv "declaration") #[$blocks,*])) | none => -- No docComment attached to declaration, render definition as usual addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) From 56d79b34f49586d95ac0a7c3d71f1342469d025d Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Sun, 8 Jun 2025 10:13:27 +0200 Subject: [PATCH 3/5] Lemma fix --- src/verso-blog/VersoBlog/LiterateLeanPage.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 95003312c..349d23b8e 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -399,7 +399,9 @@ partial def docFromMod (project : System.FilePath) (mod : String) } | other => addBlock (← ofBlock helper other) - | ``declaration => + -- Lemma is purposefully unchecked, such that it can be matched on when a project + -- is dependent on mathlib + | ``declaration | `lemma => match code with | .seq s => -- Find the index corresponding to the docComment From d1c1bbaffac1a6e37ebf25bf79102668d7cc4e6a Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 9 Jun 2025 18:11:31 +0200 Subject: [PATCH 4/5] Hide feature behind option --- examples/website/DemoSiteMain.lean | 2 ++ src/verso-blog/VersoBlog/LiterateLeanPage.lean | 9 ++++++--- src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean | 10 ++++++++++ 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/examples/website/DemoSiteMain.lean b/examples/website/DemoSiteMain.lean index fa6416edc..897250fcb 100644 --- a/examples/website/DemoSiteMain.lean +++ b/examples/website/DemoSiteMain.lean @@ -9,6 +9,8 @@ import DemoSite open Verso Genre Blog Site Syntax +set_option verso.literateMarkdown.convertDoccomments true + open Output Html Template Theme in def theme : Theme := { Theme.default with primaryTemplate := do diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 349d23b8e..259674003 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -402,8 +402,9 @@ partial def docFromMod (project : System.FilePath) (mod : String) -- Lemma is purposefully unchecked, such that it can be matched on when a project -- is dependent on mathlib | ``declaration | `lemma => - match code with - | .seq s => + -- Only convert doccomments if the option is turned on + match (← getConvertDoccomments), code with + | true, .seq s => -- Find the index corresponding to the docComment let docCommentIdx := s.findIdx? (fun | (.token ⟨.docComment, _⟩) => True @@ -421,7 +422,7 @@ partial def docFromMod (project : System.FilePath) (mod : String) | none => -- No docComment attached to declaration, render definition as usual addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) - | _ => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) + | _, _ => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) | ``eval | ``evalBang | ``reduceCmd | ``print | ``printAxioms | ``printEqns | ``«where» | ``version | ``synth | ``check => addBlock (← ``(Block.other (BlockExt.highlightedCode `name $(quote code)) Array.mkArray0)) if let some (k, msg) := getFirstMessage code then @@ -613,6 +614,8 @@ directory that contains a toolchain file and a Lake configuration (`lakefile.tom Set the option `verso.literateMarkdown.logInlines` to `true` to see the error messages that prevented elaboration of inline elements. +Set the option `verso.literateMarkdown.convertDoccomments` to `true` to convert doccomments in +a similar way as the module docstrings, except without allowing headers. -/ syntax "def_literate_post " ident optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean index 0ad40f33e..4b78c524e 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean @@ -13,7 +13,17 @@ register_option verso.literateMarkdown.logInlines : Bool := { descr := "Whether to log failures to elaborate inline code items in Markdown comments." } +register_option verso.literateMarkdown.convertDoccomments : Bool := { + defValue := false + group := "doc" + descr := "Whether to convert doccomments on definitions to text ." +} + + namespace Verso.Genre.Blog.Literate def getLogInlines [Monad m] [MonadOptions m] : m Bool := do return (← getOptions).get verso.literateMarkdown.logInlines.name verso.literateMarkdown.logInlines.defValue + +def getConvertDoccomments [Monad m] [MonadOptions m] : m Bool := do + return (← getOptions).get verso.literateMarkdown.convertDoccomments.name verso.literateMarkdown.convertDoccomments.defValue From adf86b94b7631311225d21184d264a101c606b14 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 9 Jun 2025 18:16:39 +0200 Subject: [PATCH 5/5] Change to bool for consistency --- src/verso-blog/VersoBlog/LiterateLeanPage.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 259674003..80fb2873d 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -407,7 +407,7 @@ partial def docFromMod (project : System.FilePath) (mod : String) | true, .seq s => -- Find the index corresponding to the docComment let docCommentIdx := s.findIdx? (fun - | (.token ⟨.docComment, _⟩) => True + | (.token ⟨.docComment, _⟩) => true | _ => false) match docCommentIdx with | some i =>