feat: port to SubVerso

The compiler interaction and source highlighting features of Verso are
now extracted to a library that can be used with many different Lean
versions. It provides tools for writing Lean projects that use
multiple toolchains and including examples from them in the same text.

This provides an alternative to inline code blocks for more
complicated cases.

examples/website-examples/.gitignore

@@ -0,0 +1 @@
+/.lake

examples/website-examples/Examples.lean

@@ -0,0 +1,33 @@
+import Examples.Basic
+
+import SubVerso.Examples
+open SubVerso.Examples
+
+%example basic
+def t : Tree Nat := .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+
+example := t.flip
+
+#eval t.flip
+
+#check Tree.flip
+%end
+
+%example proof
+theorem Tree.flip_flip_id (t : Tree α) : t.flip.flip = t := by
+  induction t with
+  | leaf => rfl
+  | branch l v r ih1 ih2 =>
+    simp only [flip]
+    rw [ih1]
+    rw [ih2]
+%end
+
+%example oldterm
+-- The old syntax:
+def foo (n k : Nat) : Nat :=
+  if n < k then
+    1 + foo (n + 1) k
+  else 0
+termination_by foo n k => k - n
+%end

examples/website-examples/Examples/Basic.lean

@@ -0,0 +1,14 @@
+import SubVerso.Examples
+open SubVerso.Examples
+
+%example Tree
+inductive Tree (α : Type u) : Type u where
+  | leaf
+  | branch (left : Tree α) (val : α) (right : Tree α)
+%end
+
+%example Tree.flip
+def Tree.flip : Tree α → Tree α
+  | .leaf => .leaf
+  | .branch l v r => %ex{flopped}{.branch r.flip v l.flip}
+%end

examples/website-examples/lake-manifest.json

@@ -0,0 +1,14 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/subverso.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "8c578ebd38645c9ac0d64ce6a6958b7975cf8ca6",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "examples",
+ "lakeDir": ".lake"}

examples/website-examples/lakefile.lean

@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+require subverso from git "https://github.com/leanprover/subverso.git"@"main"
+
+package «examples» where
+  -- add package configuration options here
+
+@[default_target]
+lean_lib «Examples» where
+  -- add library configuration options here

examples/website-examples/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0

examples/website/DemoSite.lean

@@ -3,3 +3,4 @@ import DemoSite.About
 import DemoSite.Blog
 import DemoSite.Blog.FirstPost
 import DemoSite.Blog.Conditionals
+import DemoSite.Blog.Subprojects

examples/website/DemoSite/Blog/Subprojects.lean

@@ -0,0 +1,38 @@
+import Verso.Genre.Blog
+import DemoSite.Categories
+open Verso Genre Blog
+open DemoSite
+
+set_option pp.rawOnError true
+
+#doc (Post) "Examples from Subprojects" =>
+
+%%%
+authors := ["Fictional Author", "Another Fictional Author"]
+date := {year := 2024, month := 3, day := 5}
+categories := [examples, other]
+%%%
+
+This post demonstrates mixing highlighted examples from multiple Lean versions.
+
+{leanExampleProject examples "examples/website-examples"}
+
+# Foo
+
+Here's a tree:
+
+{leanCommand examples Examples.Basic.Tree}
+
+They can be flipped around:
+
+{leanCommand examples Examples.Basic.Tree.flip}
+
+And subterms can be included: {leanTerm examples}`Examples.Basic.Tree.flip.flopped`.
+
+We can even prove things about them:
+
+{leanCommand examples Examples.proof}
+
+And use old syntax:
+
+{leanCommand examples Examples.oldterm}

examples/website/DemoSiteMain.lean

@@ -56,6 +56,7 @@ def demoSite : Site := site DemoSite.Front /
   static "static" ← "examples/website/static_files"
   "about" DemoSite.About
   "blog" DemoSite.Blog with
+    DemoSite.Blog.Subprojects
     DemoSite.Blog.Conditionals
     DemoSite.Blog.FirstPost
 

examples/website/static_files/style.css

@@ -43,7 +43,7 @@ pre {
     font-family: monospace;
 }
 
-p, pre {
+p, pre, code.block {
     line-height: 1.25;
 }
 
@@ -81,7 +81,7 @@ header {
     margin-bottom: 1.5em;
 }
 
-.main p, .main pre {
+.main p, .main pre, .main code.block {
   margin-bottom: 0.5em;
 }
 
@@ -146,6 +146,13 @@ ul.categories li:has( + li)::after {
     content: ", ";
 }
 
+/**************************/
+
+code {
+    font-family: monospace;
+}
+
+/**************************/
 
 .lexed.json .brace {
     color: #0000aa;

lake-manifest.json

@@ -1,5 +1,14 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover/subverso.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "8c578ebd38645c9ac0d64ce6a6958b7975cf8ca6",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "verso",
  "lakeDir": ".lake"}

lakefile.lean

@@ -1,6 +1,8 @@
 import Lake
 open Lake DSL
 
+require subverso from git "https://github.com/leanprover/subverso.git"@"main"
+
 package verso where
   -- add package configuration options here
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-02-26
+leanprover/lean4:v4.7.0-rc1

src/verso-blog/Verso/Genre/Blog.lean

@@ -1,13 +1,15 @@
+import SubVerso.Highlighting
+import SubVerso.Examples
+
 import Verso.Genre.Blog.Basic
 import Verso.Genre.Blog.Generate
-import Verso.Genre.Blog.Highlighted
-import Verso.Genre.Blog.HighlightCode
 import Verso.Genre.Blog.Site
 import Verso.Genre.Blog.Site.Syntax
 import Verso.Genre.Blog.Template
 import Verso.Genre.Blog.Theme
 import Verso.Doc.Lsp
 import Verso.Doc.Suggestion
+import Verso.Hover
 open Verso.Output Html
 open Lean (RBMap)
 
@@ -16,6 +18,8 @@ namespace Verso.Genre.Blog
 open Lean Elab
 open Verso Doc Elab
 
+open SubVerso.Examples (loadExamples Example)
+
 
 @[role_expander htmlSpan]
 def htmlSpan : RoleExpander
@@ -79,6 +83,11 @@ def page_link : RoleExpander
 
 structure ExampleContext where
   contexts : NameMap (Command.State × Parser.ModuleParserState) := {}
+  /-- Subprojects loaded from other Lean versions (using SubVerso). The outer layer of `NameMap`
+  maps the assigned name to the project, and the inner layer maps the project's own example names to
+  example information.
+  -/
+  subprojects : NameMap (NameMap Example) := {}
 deriving Inhabited
 
 initialize exampleContextExt : EnvExtension ExampleContext ← registerEnvExtension (pure {})
@@ -164,6 +173,78 @@ where
       pure (some vals[0])
     else throwError "Duplicate values for '{key}'"
 
+open System in
+@[block_role_expander leanExampleProject]
+def leanExampleProject : BlockRoleExpander
+  | #[.anon (.name name), .anon (.str projectDir)], #[] => do
+    if exampleContextExt.getState (← getEnv) |>.subprojects |>.contains name.getId then
+      throwError "Subproject '{name}' already defined in this module"
+    let path : FilePath := ⟨projectDir⟩
+    if path.isAbsolute then
+      throwError "Expected a relative path, got {path}"
+    let loadedExamples ← loadExamples path
+    let mut savedExamples := {}
+    for (mod, modExamples) in loadedExamples.toList do
+      for (exName, ex) in modExamples.toList do
+        savedExamples := savedExamples.insert (mod ++ exName) ex
+    modifyEnv fun env => exampleContextExt.modifyState env fun s => {s with
+      subprojects := s.subprojects.insert name.getId savedExamples
+    }
+    Verso.Hover.addCustomHover (← getRef) <| "Contains:\n" ++ String.join (savedExamples.toList.map (s!" * `{toString ·.fst}`\n"))
+    pure #[]
+  | _, more =>
+    if h : more.size > 0 then
+      throwErrorAt more[0] "Unexpected contents"
+    else
+      throwError "Unexpected arguments"
+where
+  getModExamples (mod : Name) (json : Json) : DocElabM (NameMap Example) := do
+    let .ok exs := json.getObj?
+      | throwError "Not an object: '{json}'"
+    let mut found := {}
+    for ⟨name, exJson⟩ in exs.toArray do
+      match FromJson.fromJson? exJson with
+      | .error err =>
+        throwError "Error deserializing example '{name}' in '{mod}': {err}\nfrom:\n{json}"
+      | .ok ex => found := found.insert (mod ++ name.toName) ex
+    pure found
+
+@[block_role_expander leanCommand]
+def leanCommand : BlockRoleExpander
+  | #[.anon (.name project), .anon (.name exampleName)], #[] => do
+    let some projectExamples := exampleContextExt.getState (← getEnv) |>.subprojects |>.find? project.getId
+      | throwErrorAt project "Subproject '{project}' not loaded"
+    Verso.Hover.addCustomHover project <| "Contains:\n" ++ String.join (projectExamples.toList.map (s!" * `{toString ·.fst}`\n"))
+    let some {highlighted := hls, original := str, ..} := projectExamples.find? exampleName.getId
+      | throwErrorAt exampleName "Example '{exampleName}' not found - options are {projectExamples.toList.map (·.fst)}"
+    Verso.Hover.addCustomHover exampleName s!"```lean\n{str}\n```"
+    pure #[← ``(Block.other (Blog.BlockExt.highlightedCode $(quote project.getId) (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Block.code none #[] 0 $(quote str)])]
+  | _, more =>
+    if h : more.size > 0 then
+      throwErrorAt more[0] "Unexpected contents"
+    else
+      throwError "Unexpected arguments"
+
+@[role_expander leanTerm]
+def leanTerm : RoleExpander
+  | #[.anon (.name project)], #[arg] => do
+    let `(inline|code{ $name:str }) := arg
+      | throwErrorAt arg "Expected code literal with the example name"
+    let exampleName := name.getString.toName
+    let subprojects := exampleContextExt.getState (← getEnv) |>.subprojects
+    let some projectExamples := subprojects |>.find? project.getId
+      | throwErrorAt project "Subproject '{project}' not loaded"
+    Verso.Hover.addCustomHover project <| "Contains:\n" ++ String.join (projectExamples.toList.map (s!" * `{toString ·.fst}`\n"))
+    let some {highlighted := hls, original := str, ..} := projectExamples.find? exampleName
+      | throwErrorAt name "Example '{exampleName}' not found - options are {projectExamples.toList.map (·.fst)}"
+    Verso.Hover.addCustomHover arg s!"```lean\n{str}\n```"
+    pure #[← ``(Inline.other (Blog.InlineExt.highlightedCode $(quote project.getId) (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Inline.code $(quote str)])]
+  | _, more =>
+    if h : more.size > 0 then
+      throwErrorAt more[0] "Unexpected contents"
+    else
+      throwError "Unexpected arguments"
+
 @[code_block_expander leanInit]
 def leanInit : CodeBlockExpander
   | args , str => do
@@ -192,7 +273,7 @@ where
   configureCommandState (env : Environment) (msg : MessageLog) : Command.State :=
     { Command.mkState env msg with infoState := { enabled := true } }
 
-open Verso.Genre.Highlighted in
+open SubVerso.Highlighting Highlighted in
 @[code_block_expander lean]
 def lean : CodeBlockExpander
   | args, str => do
@@ -233,7 +314,7 @@ def lean : CodeBlockExpander
       setInfoState s.commandState.infoState
       setEnv s.commandState.env
       for cmd in s.commands do
-        hls := hls ++ (← highlight cmd s.commandState.messages.msgs.toArray)
+        hls := hls ++ (← highlight cmd s.commandState.messages.msgs.toArray s.commandState.infoState.trees)
     finally
       setInfoState infoSt
       setEnv env