feat: structured messages

examples/anchor-examples/lake-manifest.json

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

examples/documented-package/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
+      "rev": "93548b1153035f72290bf855d28dd11b3d853ff8",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/documented-package/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["Zippers"]
 [[require]]
 name = "subverso"
 git = "https://github.com/leanprover/subverso"
-rev = "main"
+rev = "structured-output"
 
 [[lean_lib]]
 name = "Zippers"

examples/website-examples/lake-manifest.json

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

examples/website-literate/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
+      "rev": "93548b1153035f72290bf855d28dd11b3d853ff8",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website/DemoSite/Blog/Conditionals.lean

@@ -35,7 +35,7 @@ Here are some examples:
 ```
 
 
-```lean demo (error := true)
+```lean demo (error := true) (name := fst)
 example := if true then 1 else 2
 example := if True then 1 else 2
 example : Int := if True then 1 else 2
@@ -44,6 +44,13 @@ example : 2 < 5 := by
   constructor
 ```
 
+Here's the error:
+```leanOutput fst
+unsolved goals
+case a.a
+⊢ (Nat.succ 2).le 3
+```
+
 ```lean demo
 /-- A recursive function -/
 def slowId : Nat → Nat
@@ -212,4 +219,44 @@ example := %more_info(25)
 
 The info gets stacked up, with the greatest severity highlighting the range in question.
 
+Here's some hoverable info:
+```lean demo (error := true) (name := typeErr)
+example : Nat := "Not a number"
+```
+```leanOutput typeErr
+type mismatch
+  "Not a number"
+has type
+  String : Type
+but is expected to have type
+  Nat : Type
+```
+
+
+Here's some traces:
+```lean demo (error := true) (name := traces)
+set_option trace.compiler.ir.result true in
+def f' (xs : List Nat) := xs.foldl (init := 0) (· + ·)
+
+set_option diagnostics true in
+example : (123123190283102938019238098 * 1234124).toString.length > 14 := by
+  simp
+```
+```leanOutput traces
+[diag] Diagnostics
+  [reduction] unfolded reducible declarations (max: 34, num: 1):
+    [reduction] outParam ↦ 34
+  [type_class] used instances (max: 54, num: 1):
+    [type_class] USize.instOfNat ↦ 54
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+```
+
+Here's a check:
+```lean demo (name := check)
+#check fun x => [x]
+```
+```leanOutput check
+fun x => [x] : ?m.18581 → List ?m.18581
+```
+
 Thank you for looking at my test/demo post.

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
+   "rev": "93548b1153035f72290bf855d28dd11b3d853ff8",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

src/verso-blog/VersoBlog.lean

@@ -183,7 +183,7 @@ deriving Inhabited
 initialize exampleContextExt : EnvExtension ExampleContext ← registerEnvExtension (pure {})
 
 structure ExampleMessages where
-  messages : NameSuffixMap (MessageLog ⊕ List (MessageSeverity × String)) := {}
+  messages : NameSuffixMap ((Environment × MessageLog) ⊕ List (MessageSeverity × String)) := {}
 deriving Inhabited
 
 initialize messageContextExt : EnvExtension ExampleMessages ← registerEnvExtension (pure {})
@@ -401,9 +401,10 @@ def leanInit : CodeBlockExpander
       throwErrorAt header "Modules not yet supported here"
     for imp in header.raw[2].getArgs do
       logErrorAt imp "Imports not yet supported here"
-    let opts := Options.empty -- .setBool `trace.Elab.info true
+    let opts := Options.empty.setBool `pp.tagAppFns true
     if header.raw[1].isNone then -- if the "prelude" option was not set, use the current env
-      let commandState := configureCommandState (←getEnv) {}
+      let commandState := configureCommandState (← getEnv) {}
+      let commandState := { commandState with scopes := [{ header := "", opts := pp.tagAppFns.set {} true }] }
       modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState  state)}
     else
       if header.raw[2].getArgs.isEmpty then
@@ -413,6 +414,7 @@ def leanInit : CodeBlockExpander
             logMessage msg
           liftM (m := IO) (throw <| IO.userError "Errors during import; aborting")
         let commandState := configureCommandState env {}
+        let commandState := { commandState with scopes := [{ header := "", opts := pp.tagAppFns.set {} true }] }
         modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState state)}
     if config.show.getD false then
       pure #[← ``(Block.code $(quote str.getString))] -- TODO highlighting hack
@@ -468,7 +470,7 @@ def lean : CodeBlockExpander
       }
     if let some infoName := config.name then
       modifyEnv fun env => messageContextExt.modifyState env fun st => {st with
-        messages := st.messages.insert infoName (.inl s.commandState.messages)
+        messages := st.messages.insert infoName (.inl (s.commandState.env, s.commandState.messages))
       }
     withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Highlighting syntax") do
       let mut hls := Highlighted.empty
@@ -686,32 +688,16 @@ where
       | other => throwError "Expected whitespace mode, got {repr other}"
   }
 
-private def leanOutputBlock [bg : BlogGenre genre] (severity : MessageSeverity) (message : String) (summarize : Bool := false) : Block genre :=
-  if summarize then
-    let lines := message.splitOn "\n"
-    let pre := lines.take 3
-    let post := String.join (lines.drop 3 |>.intersperse "\n")
-    let preHtml : Html := pre.map (fun (l : String) => {{<code>{{l}}</code>}})
-    Block.other (bg.block_eq ▸ BlockExt.htmlDetails (sevStr severity) preHtml) #[Block.code post]
-  else
-    Block.other (bg.block_eq ▸ BlockExt.htmlDiv (sevStr severity)) #[Block.code message]
-where
-  sevStr : MessageSeverity → String
-    | .error => "error"
-    | .information => "information"
-    | .warning => "warning"
+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 leanOutputInline [bg : BlogGenre genre] (severity : MessageSeverity) (message : String) (plain : Bool) : Inline genre :=
+open SubVerso.Highlighting in
+private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Message) (plain : Bool) : Inline genre :=
   if plain then
-    Inline.code message
+    Inline.code message.toString
   else
-    Inline.other (bg.inline_eq ▸ InlineExt.htmlSpan (sevStr severity)) #[Inline.code message]
-where
-  sevStr : MessageSeverity → String
-    | .error => "error"
-    | .information => "information"
-    | .warning => "warning"
-
+    Inline.other (bg.inline_eq ▸ InlineExt.message message) #[Inline.code message.toString]
 
 @[code_block_expander leanOutput]
 def leanOutput : Doc.Elab.CodeBlockExpander
@@ -720,7 +706,7 @@ def leanOutput : Doc.Elab.CodeBlockExpander
 
     let (_, savedInfo) ← messageContextExt.getState (← getEnv) |>.messages |>.getOrSuggest config.name
     let messages ← match savedInfo with
-      | .inl log =>
+      | .inl (env, log) =>
         let messages ← liftM <| log.toArray.mapM contents
         for m in log.toArray do
           if mostlyEqual config.whitespace str.getString (← contents m) then
@@ -734,7 +720,14 @@ def leanOutput : Doc.Elab.CodeBlockExpander
                 let preHtml : Html := pre.map (fun (l : String) => {{<code>{{l}}</code>}})
                 ``(Block.other (Blog.BlockExt.htmlDetails $(quote (sevStr m.severity)) $(quote preHtml)) #[Block.code $(quote post)])
               else
-                ``(Block.other (Blog.BlockExt.htmlDiv $(quote (sevStr m.severity))) #[Block.code $(quote str.getString)])
+                let myEnv ← getEnv
+                let m' ←
+                  try
+                    setEnv env
+                    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)])
             return #[content]
         pure messages
       | .inr msgs =>
@@ -859,7 +852,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 severity message plain :=
-    leanOutputInline severity message plain
-  leanOutputBlock severity message (summarize := false) :=
-    leanOutputBlock severity message (summarize := summarize)
+  leanOutputInline message plain :=
+    leanOutputInline message plain
+  leanOutputBlock message (summarize := false) :=
+    leanOutputBlock message (summarize := summarize)

src/verso-blog/VersoBlog/Basic.lean

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

src/verso-blog/VersoBlog/LiterateLeanPage.lean

@@ -327,7 +327,7 @@ where getString : Highlighted → m String
   | .token ⟨_, txt⟩ => pure txt
 end
 
-def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × String)
+def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × Highlighted.MessageContents Highlighted)
   | .span msgs x =>
     msgs[0]? <|> getFirstMessage x
   | .point k m => pure (k, m)

src/verso-blog/VersoBlog/Template.lean

@@ -148,6 +148,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="lean-output hl lean">{{← msg.toHtml (g := g)}}</pre>}}
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
@@ -177,6 +179,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>}}
   | .lexedText content, _contents => do
     pure {{ <code class=s!"lexed {content.name}"> {{ content.toHtml }} </code> }}
   | .customHighlight hls, _contents => do

src/verso-blog/VersoBlog/Traverse.lean

@@ -41,7 +41,7 @@ def addJsFile (filename contents : String) : TraverseM Unit := do
   modify fun s => s.addJsFile filename contents
 
 def genreBlock (g : Genre) [bg : BlogGenre g] : Blog.BlockExt → Array (Block g) → Blog.TraverseM (Option (Block g))
-    | .highlightedCode .., _contents => do
+    | .highlightedCode .., _contents | .message .., _contents => do
       modify fun st => {st with
         stylesheets := st.stylesheets.insert highlightingStyle,
         scripts := st.scripts.insert highlightingJs
@@ -64,7 +64,7 @@ def genreBlock (g : Genre) [bg : BlogGenre g] : Blog.BlockExt → Array (Block g
     | _, _ => pure none
 
 def genreInline (g : Genre) [bg : BlogGenre g] : Blog.InlineExt → Array (Inline g) → Blog.TraverseM (Option (Inline g))
-    | .highlightedCode .., _contents | .customHighlight .., _contents => do
+    | .highlightedCode .., _contents | .customHighlight .., _contents | .message .., _contents => do
       modify fun st => {st with
         stylesheets := st.stylesheets.insert highlightingStyle,
         scripts := st.scripts.insert highlightingJs

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 (severity : MessageSeverity) (message : String) (summarize : Bool := false) where
-  data := ToJson.toJson (severity, message, summarize)
+block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) where
+  data := ToJson.toJson (message, summarize)
   traverse _ _ _ := do
     pure none
   toTeX :=
@@ -142,14 +142,12 @@ block_extension Block.leanOutput (severity : MessageSeverity) (message : String)
       | .error err =>
         HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err
         pure .empty
-      | .ok ((sev, txt, summarize) : MessageSeverity × String × Bool) =>
-        let wrap html :=
-          if summarize then {{<details><summary>"Expand..."</summary>{{html}}</details>}}
-          else html
-        pure <| wrap {{<div class={{sev.class}}><pre>{{txt}}</pre></div>}}
+      | .ok ((msg, summarize) : Highlighted.Message × Bool) =>
+        msg.blockHtml summarize (g := Manual)
 
-inline_extension Inline.leanOutput (severity : MessageSeverity) (message : String) (plain : Bool) where
-  data := ToJson.toJson (severity, message, plain)
+
+inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) where
+  data := ToJson.toJson (message, plain)
   traverse _ _ _ := do
     pure none
   toTeX :=
@@ -167,16 +165,16 @@ inline_extension Inline.leanOutput (severity : MessageSeverity) (message : Strin
       | .error err =>
         HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err
         pure .empty
-      | .ok ((sev, txt, plain) : MessageSeverity × String × Bool) =>
-        let plainHtml := {{<code>{{txt}}</code>}}
+      | .ok ((txt, plain) : Highlighted.Message × Bool) =>
+        let plainHtml := {{<code>{{txt.toString}}</code>}}
         if plain then pure plainHtml
-        else pure {{<span class={{sev.class}}>{{plainHtml}}</span>}}
+        else txt.toHtml (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 severity message plain := Inline.other (Inline.leanOutput severity message plain) #[]
-  leanOutputBlock severity message (summarize : Bool := false) :=
-    Block.other (Block.leanOutput severity message (summarize := summarize)) #[]
+  leanOutputInline message plain := Inline.other (Inline.leanOutput message plain) #[]
+  leanOutputBlock message (summarize : Bool := false) :=
+    Block.other (Block.leanOutput message (summarize := summarize)) #[]