feat: configurable trace expansion

examples/anchor-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7",
+      "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/documented-package/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7",
+      "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7",
+      "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website-literate/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7",
+      "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7",
+   "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

src/verso-blog/VersoBlog.lean

@@ -690,15 +690,15 @@ where
   }
 
 open SubVerso.Highlighting in
-private def leanOutputBlock [bg : BlogGenre genre] (message : Highlighted.Message) (summarize := false) : Block genre :=
-  Block.other (bg.block_eq ▸ BlockExt.message summarize message) #[Block.code message.toString]
+private def leanOutputBlock [bg : BlogGenre genre] (message : Highlighted.Message) (summarize := false) (expandTraces : List Name := []) : Block genre :=
+  Block.other (bg.block_eq ▸ BlockExt.message summarize message expandTraces) #[Block.code message.toString]
 
 open SubVerso.Highlighting in
-private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Message) (plain : Bool) : Inline genre :=
+private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Message) (plain : Bool) (expandTraces : List Name := []) : Inline genre :=
   if plain then
     Inline.code message.toString
   else
-    Inline.other (bg.inline_eq ▸ InlineExt.message message) #[Inline.code message.toString]
+    Inline.other (bg.inline_eq ▸ InlineExt.message message expandTraces) #[Inline.code message.toString]
 
 @[code_block_expander leanOutput]
 def leanOutput : Doc.Elab.CodeBlockExpander
@@ -728,7 +728,7 @@ def leanOutput : Doc.Elab.CodeBlockExpander
                     withOptions (·.set `pp.tagAppFns true) do
                       SubVerso.Highlighting.highlightMessage m
                   finally setEnv myEnv
-                ``(Block.other (Blog.BlockExt.message false $(quote m')) #[Block.code $(quote str.getString)])
+                ``(Block.other (Blog.BlockExt.message false $(quote m') ([] : List Lean.Name)) #[Block.code $(quote str.getString)])
             return #[content]
         pure messages
       | .inr msgs =>
@@ -855,7 +855,7 @@ instance [bg : BlogGenre genre] : ExternalCode genre where
     Inline.other (bg.inline_eq ▸ InlineExt.highlightedCode { cfg with contextName := `verso } hl) #[]
   leanBlock hl cfg :=
     Block.other (bg.block_eq ▸ BlockExt.highlightedCode { cfg with contextName := `verso } hl) #[]
-  leanOutputInline message plain :=
-    leanOutputInline message plain
-  leanOutputBlock message (summarize := false) :=
-    leanOutputBlock message (summarize := summarize)
+  leanOutputInline message plain (expandTraces := []) :=
+    leanOutputInline message plain (expandTraces := expandTraces)
+  leanOutputBlock message (summarize := false) (expandTraces : List Name := []) :=
+    leanOutputBlock message (summarize := summarize) (expandTraces := expandTraces)

src/verso-blog/VersoBlog/Basic.lean

@@ -36,7 +36,7 @@ deriving Repr
 
 inductive BlockExt where
   | highlightedCode (opts : CodeOpts) (highlighted : Highlighted)
-  | message (summarize : Bool) (msg : Highlighted.Message)
+  | message (summarize : Bool) (msg : Highlighted.Message) (expandTraces : List Lean.Name)
   | lexedText (content : LexedText)
   | htmlDiv (classes : String)
   | htmlWrapper (tag : String) (attributes : Array (String × String))
@@ -46,7 +46,7 @@ inductive BlockExt where
 
 inductive InlineExt where
   | highlightedCode (opts : CodeOpts) (highlighted : Highlighted)
-  | message (msg : Highlighted.Message)
+  | message (msg : Highlighted.Message) (expandTraces : List Lean.Name)
   | lexedText (content : LexedText)
   | customHighlight (highlighted : Highlighted)
   | label (name : Lean.Name)

src/verso-blog/VersoBlog/Template.lean

@@ -149,8 +149,8 @@ def blockHtml (g : Genre)
   | .highlightedCode { contextName, showProofStates } hls, _contents =>
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
     hls.blockHtml (toString contextName) (g := g)
-  | .message summarize msg, _contents => do
-    return {{<pre class=s!"lean-output hl lean {msg.severity.class}">{{← msg.toHtml (g := g)}}</pre>}}
+  | .message summarize msg expandTraces, _contents => do
+    return {{<pre class=s!"lean-output hl lean {msg.severity.class}">{{← msg.toHtml (expandTraces := expandTraces) (g := g)}}</pre>}}
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
@@ -180,8 +180,8 @@ def inlineHtml (g : Genre) [bg : BlogGenre g]
   | .highlightedCode { contextName, showProofStates } hls, _contents =>
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
     hls.inlineHtml (some <| toString contextName) (g := g)
-  | .message msg, _contents => do
-    return {{<code class="lean-output hl lean">{{← msg.toHtml (g := g)}}</code>}}
+  | .message msg expandTraces, _contents => do
+    return {{<code class="lean-output hl lean">{{← msg.toHtml expandTraces (g := g)}}</code>}}
   | .lexedText content, _contents => do
     pure {{ <code class=s!"lexed {content.name}"> {{ content.toHtml }} </code> }}
   | .customHighlight hls, _contents => do

src/verso-manual/VersoManual/ExternalLean.lean

@@ -123,8 +123,8 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where
               codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD false }) <|
             hl.inlineHtml (g := Manual) "examples"
 
-block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) where
-  data := ToJson.toJson (message, summarize)
+block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) (expandTraces : List Name := []) where
+  data := ToJson.toJson (message, summarize, expandTraces)
   traverse _ _ _ := do
     pure none
   toTeX :=
@@ -142,12 +142,12 @@ block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bo
       | .error err =>
         HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err
         pure .empty
-      | .ok ((msg, summarize) : Highlighted.Message × Bool) =>
-        msg.blockHtml summarize (g := Manual)
+      | .ok ((msg, summarize, expandTraces) : Highlighted.Message × Bool × List Name) =>
+        msg.blockHtml summarize expandTraces (g := Manual)
 
 
-inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) where
-  data := ToJson.toJson (message, plain)
+inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) (expandTraces : List Name) where
+  data := ToJson.toJson (message, plain, expandTraces)
   traverse _ _ _ := do
     pure none
   toTeX :=
@@ -165,16 +165,16 @@ inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool
       | .error err =>
         HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err
         pure .empty
-      | .ok ((txt, plain) : Highlighted.Message × Bool) =>
+      | .ok ((txt, plain, expandTraces) : Highlighted.Message × Bool × List Name) =>
         let plainHtml := {{<code>{{txt.toString}}</code>}}
         if plain then pure plainHtml
-        else txt.toHtml (g := Manual)
+        else txt.toHtml expandTraces (g := Manual)
 
 open Verso.Code.External
 
 instance : ExternalCode Manual where
   leanInline hl cfg := Inline.other (Inline.lean hl cfg) #[]
   leanBlock hl cfg := Block.other (Block.lean hl cfg) #[]
-  leanOutputInline message plain := Inline.other (Inline.leanOutput message plain) #[]
-  leanOutputBlock message (summarize : Bool := false) :=
-    Block.other (Block.leanOutput message (summarize := summarize)) #[]
+  leanOutputInline message plain (expandTraces : List Name := []) := Inline.other (Inline.leanOutput message plain (expandTraces := expandTraces)) #[]
+  leanOutputBlock message (summarize : Bool := false) (expandTraces : List Name := []) :=
+    Block.other (Block.leanOutput message (summarize := summarize) (expandTraces := expandTraces)) #[]

src/verso-manual/VersoManual/Glossary.lean

@@ -44,6 +44,7 @@ private partial def normString (term : String) : String := Id.run do
   let mut str := term.toLower
   if str.endsWith "ies" then str := str.dropRight 3 ++ "y"
   if str.endsWith "s" then str := str.dropRight 1
+  str := str.replace "‑" "-"
   String.intercalate " " (str.split (fun c => c.isWhitespace || c == '-') |>.filter (!·.isEmpty))
 
 

src/verso-manual/VersoManual/InlineLean.lean

@@ -597,8 +597,8 @@ block_extension Block.leanOutput where
       | .error err =>
         HtmlT.logError <| "Couldn't deserialize Lean output while rendering HTML: " ++ err ++ "\n" ++ toString data
         pure .empty
-      | .ok ((msg, summarize) : Highlighted.Message × Bool) =>
-        msg.blockHtml summarize (g := Manual)
+      | .ok ((msg, summarize, expandTraces) : Highlighted.Message × Bool × List Name) =>
+        msg.blockHtml summarize (expandTraces := expandTraces) (g := Manual)
 
 
 structure LeanOutputConfig where
@@ -609,19 +609,24 @@ structure LeanOutputConfig where
   whitespace : WhitespaceMode
   normalizeMetas : Bool
   allowDiff : Nat
+  expandTraces : List Name := []
 
 section
 variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
 
-def LeanOutputConfig.parser  : ArgParse m LeanOutputConfig :=
+partial def many (p : ArgParse m α) : ArgParse m (List α) :=
+  ((· :: ·) <$> p <*> many p) <|> pure []
+
+def LeanOutputConfig.parser : ArgParse m LeanOutputConfig :=
   LeanOutputConfig.mk <$>
     .positional `name output <*>
     ((·.getD true) <$> .named `show .bool true) <*>
     .named `severity .messageSeverity true <*>
     ((·.getD false) <$> .named `summarize .bool true) <*>
     ((·.getD .exact) <$> .named `whitespace .whitespaceMode true) <*>
     .namedD `normalizeMetas .bool true <*>
-    .namedD `allowDiff .nat 0
+    .namedD `allowDiff .nat 0 <*>
+    many (.named `expandTrace .name false)
 where
   output : ValDesc m Ident := {
     description := "output name",
@@ -643,8 +648,6 @@ def leanOutput : CodeBlockExpander
  | args, str => do
     let config ← LeanOutputConfig.parser.run args
 
-    let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
-
     PointOfInterest.save (← getRef) (config.name.getId.toString)
       (kind := Lsp.SymbolKind.file)
       (selectionRange := config.name)
@@ -657,9 +660,12 @@ def leanOutput : CodeBlockExpander
         normalizeMetavars str.getString
       else str.getString
 
+    let mut texts : Array (Highlighted.Span.Kind × String) := #[]
+
     if config.allowDiff == 0 then
       for msg in msgs do
-        let txt := msg.toString
+        let txt := msg.toString (expandTraces := config.expandTraces)
+        texts := texts.push (msg.severity, txt)
         let actual :=
           if config.normalizeMetas then
             normalizeMetavars txt
@@ -669,7 +675,7 @@ def leanOutput : CodeBlockExpander
             if s != msg.severity.toSeverity then
               throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr msg.severity.toSeverity}"
           if config.show then
-            let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize))} #[Block.code $(quote str.getString)])
+            let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)])
             return #[content]
           else return #[]
     else
@@ -693,22 +699,21 @@ def leanOutput : CodeBlockExpander
 
         Log.logSilentInfo m!"Diff is {d} lines:\n{d'}"
         if config.show then
-          let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize))} #[Block.code $(quote str.getString)])
+          let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)])
           return #[content]
         else return #[]
 
-    let suggs : Array (Nat × Meta.Hint.Suggestion) := msgs.toArray.map fun msg =>
-      let strMsg := msg.toString
-      ((diffSize config.whitespace strMsg str.getString).1, {
-        suggestion := withNl msg.toString,
-        preInfo? := some s!"{sevStr msg.severity.toSeverity}: "
+    let suggs : Array (Nat × Meta.Hint.Suggestion) := texts.map fun (sev, msg) =>
+      ((diffSize config.whitespace msg str.getString).1, {
+        suggestion := withNl msg,
+        preInfo? := some s!"{sevStr sev.toSeverity}: "
       })
     let suggs : Array Meta.Hint.Suggestion := suggs.qsort (fun x y => x.1 < y.1) |>.map (·.2)
 
     let hintMsg := if suggs.size > 1 then m!"Replace with one of the actual messages:" else m!"Replace with the actual message:"
     let hint ← hintAt str hintMsg suggs
 
-    throwErrorAt str (m!"Didn't match - got: {indentD (toMessageData <| msgs.map (Std.Format.text ·.toString))}\nbut expected:{indentD (toMessageData str.getString)}" ++ hint)
+    throwErrorAt str (m!"Didn't match - got: {indentD (toMessageData <| texts.map (Std.Format.text ·.2))}\nbut expected:{indentD (toMessageData str.getString)}" ++ hint)
 where
   sevStr : MessageSeverity → String
     | .error => "error"

src/verso/Verso/Code/External.lean

@@ -58,9 +58,9 @@ class ExternalCode (genre : Genre) where
   An inline element for rendering Lean messages. `plain` should suppress the annotation of the
   output with its message severity.
   -/
-  leanOutputInline (message : Highlighted.Message) (plain : Bool) : Inline genre
+  leanOutputInline (message : Highlighted.Message) (plain : Bool) (expandTraces : List Lean.Name := []) : Inline genre
   /-- A block element for rendering Lean messages. -/
-  leanOutputBlock (message : Highlighted.Message) (summarize : Bool := false) : Block genre
+  leanOutputBlock (message : Highlighted.Message) (summarize : Bool := false) (expandTraces : List Lean.Name := []) : Block genre
 
 open ExternalCode
 
@@ -150,9 +150,16 @@ structure MessageContext extends CodeContext where
   The desired severity of the message.
   -/
   severity : WithSyntax MessageSeverity
+  /--
+  Traces classes to show expanded by default
+  -/
+  expandTraces : List Lean.Name
+
+private partial def many (p : ArgParse m α) : ArgParse m (List α) :=
+  (· :: ·) <$> p <*> many p <|> pure []
 
 instance : FromArgs MessageContext m where
-  fromArgs := (fun s x => MessageContext.mk x s) <$> .positional' `severity <*> fromArgs
+  fromArgs := (fun s ts x => MessageContext.mk x s ts) <$> .positional' `severity <*> many (.named `expandTrace .name false) <*> fromArgs
 
 /--
 A specification of which module to look in to find a quoted name, potentially made more specific with
@@ -572,15 +579,15 @@ Requires that the genre have an `ExternalCode` instance.
 @[code_block_expander moduleOut]
 def moduleOut : CodeBlockExpander
   | args, str => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOut") <| do
-    let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args
+    let {module := moduleName, anchor?, severity, expandTraces, showProofStates := _, defSite := _} ← parseThe MessageContext args
 
     withAnchored moduleName anchor? fun hl => do
       let infos : Array _ := allInfo hl
 
       for (msg, _) in infos do
-        if messagesMatch msg.toString str.getString then
+        if messagesMatch (msg.toString (expandTraces := expandTraces)) str.getString then
           if msg.severity == .ofSeverity severity.1 then
-            return #[← ``(leanOutputBlock $(quote msg))]
+            return #[← ``(leanOutputBlock $(quote msg) (expandTraces := $(quote expandTraces)))]
           else
           let wanted ← severityName msg.severity.toSeverity
             throwError "Mismatched severity. Expected '{repr severity.1}', got '{wanted}'.{← severityHint wanted severity.2}"
@@ -628,15 +635,15 @@ def moduleOutRole : RoleExpander
   | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOutRole") <| do
     let str? ← oneCodeStr? inls
 
-    let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args
+    let {module := moduleName, anchor?, expandTraces, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args
 
     withAnchored moduleName anchor? fun hl => do
       let infos := allInfo hl
       if let some str := str? then
         for (msg, _) in infos do
-          if messagesMatch msg.toString str.getString then
+          if messagesMatch (msg.toString (expandTraces := expandTraces)) str.getString then
             if msg.severity == .ofSeverity severity.1 then
-              return #[← ``(leanOutputInline $(quote msg) true)]
+              return #[← ``(leanOutputInline $(quote msg) true (expandTraces := $(quote expandTraces)))]
             else
               let wanted ← severityName msg.severity.toSeverity
               throwError "Mismatched severity. Expected '{repr severity.1}', got '{wanted}'.{← severityHint wanted severity.2}"