feat: make release notes insert parts from markdown (#599)

Previously, we turned all headers into emphasized text regardless of
level. With this change, we insert nested parts into the current verso
document corresponding to the markdown structure.

Resolves #542.

Author: jcreedcmu

.vale/scripts/rewrite_html.py

@@ -7,6 +7,18 @@
 
 def process_html_file(filepath, output_filepath):
     """Reads an HTML file, removes 'QA' from headers, and writes the result to the output path."""
+
+    # We exclude release notes. Before
+    # https://github.com/leanprover/reference-manual/pull/599 we generated one
+    # block for each release notes document which had class="no-vale" on it.
+    # However, it's currently not easy to add any attributes to verso parts,
+    # which https://github.com/leanprover/reference-manual/pull/599 adds, hence
+    # the current workaround here.
+    #
+    # Reconsider this if https://github.com/leanprover/verso/issues/561 is resolved.
+    if "/releases/" in filepath:
+        return
+
     with open(filepath, 'r', encoding='utf-8') as file:
         soup = BeautifulSoup(file, 'html.parser')
 

Manual/Meta/ErrorExplanation.lean

@@ -292,7 +292,7 @@ structure ExplanElabM.State where
   /-- The index of the next block in the context's `blocks` to elaborate. -/
   blockIdx : Nat := 0
   /-- Active Markdown header levels that can be closed by subsequent Markdown -/
-  levels : HeaderMapping := []
+  levels : Markdown.HeaderMapping := default
   /-- The index of the current code block within this explanation. -/
   codeBlockIdx : Nat := 0
 
@@ -362,7 +362,7 @@ def addPartFromExplanationMarkdown (b : MD4Lean.Block) : ExplanElabM Unit := do
   let keywords := tactics.map (·.userName)
   let ref ← getRef
   let {name, severity .. } ← read
-  let ls ← addPartFromMarkdown b
+  let ls ← addPartFromMarkdown b ((← getThe ExplanElabM.State).levels)
     (handleHeaders := Markdown.strongEmphHeaders)
     (elabInlineCode := some (tryElabInlineCodeStrictRestoringState tactics keywords))
     (elabBlockCode := some fun i l s => withRef ref <|
@@ -438,14 +438,6 @@ private def titleOfCodeBlock? (b : MD4Lean.Block) : Option String := do
   let info ← infoOfCodeBlock b |>.toOption
   info.title?
 
-/-- Closes the last-opened section, throwing an error on failure. -/
-def closeEnclosingSection : PartElabM Unit := do
-  -- We use `default` as the source position because the Markdown doesn't have one
-  if let some ctxt' := (← getThe PartElabM.State).partContext.close default then
-    modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
-  else
-    throwError m!"Failed to close the last-opened explanation part"
-
 /-- Adds explanation blocks until the "Examples" header is reached. -/
 def addNonExampleBlocks : ExplanElabM Unit := do
   repeat
@@ -636,8 +628,7 @@ def addExplanationBlocksFor (name : Name) : PartElabM Unit := do
         | throwErrorAt (← getRef) "Failed to parse docstring as Markdown"
       addExplanationMetadata explan.metadata
       let (_, { levels, .. }) ← addExplanationBodyBlocks.run name explan.metadata.severity ast.blocks
-      for _ in levels do
-        closeEnclosingSection
+      closeEnclosingSections levels
     catch
       | .error ref msg => throw <| .error ref m!"Failed to process explanation for {name}: {msg}"
       | e => throw e

Manual/Meta/Markdown.lean

@@ -6,7 +6,7 @@ Author: Joachim Breitner
 
 import VersoManual
 import Manual.Meta.Figure
-import Lean.Elab.InfoTree.Types
+import Lean.Elab.InfoTree
 
 open Verso Doc Elab
 open Verso.Genre Manual
@@ -28,12 +28,31 @@ def Block.noVale.descr : BlockDescr where
     some <| fun _ goB _ _ content => do
       pure {{<div class="no-vale">{{← content.mapM goB}}</div>}}
 
-@[code_block_expander markdown]
-def markdown : CodeBlockExpander
-  | _args, str => do
-    let str ← parserInputString str
-    let some ast := MD4Lean.parse str
-      | throwError "Failed to parse docstring as Markdown"
-    let content ← ast.blocks.mapM <|
-      Markdown.blockFromMarkdown (handleHeaders := Markdown.strongEmphHeaders)
-    pure #[← ``(Block.other Block.noVale #[$content,*])]
+/-- Closes the last-opened section, throwing an error on failure. -/
+def closeEnclosingSection : PartElabM Unit := do
+  -- We use `default` as the source position because the Markdown doesn't have one
+  if let some ctxt' := (← getThe PartElabM.State).partContext.close default then
+    modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
+  else
+    throwError m!"Failed to close the last-opened explanation part"
+
+/-- Closes as many sections as were created by markdown processing. -/
+def closeEnclosingSections (headerMapping : Markdown.HeaderMapping) : PartElabM Unit := do
+  for _ in headerMapping do
+    closeEnclosingSection
+
+@[part_command Lean.Doc.Syntax.codeblock]
+def markdown : PartCommand
+  | `(Lean.Doc.Syntax.codeblock| ``` $markdown:ident $args*| $txt ``` ) => do
+     let x ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo markdown
+     if x != by exact decl_name% then Elab.throwUnsupportedSyntax
+     for arg in args do
+       let h ← MessageData.hint m!"Remove it" #[""] (ref? := arg)
+       logErrorAt arg m!"No arguments expected{h}"
+     let some ast := MD4Lean.parse txt.getString
+       | throwError "Failed to parse body of markdown code block"
+     let mut currentHeaderLevels : Markdown.HeaderMapping := default
+     for block in ast.blocks do
+       currentHeaderLevels ← Markdown.addPartFromMarkdown block currentHeaderLevels
+     closeEnclosingSections currentHeaderLevels
+  | _ => Elab.throwUnsupportedSyntax