feat: live links for uses of example directive

Main.lean

@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 import Manual
 import Manual.Meta
 import VersoManual
+import Manual.ExtractExamples
 
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
@@ -32,7 +33,7 @@ def staticCss := {{
   }}
 
 def main :=
-  manualMain (%doc Manual) (config := config)
+  manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples])
 where
   config := Config.addSearch <| Config.addKaTeX {
     extraFiles := [("static", "static")],

Manual/ExtractExamples.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jason Reed
+-/
+
+import Manual.Meta.Example
+import VersoManual
+open Lean
+open Verso Doc Multi
+open Verso.Genre Manual
+open Std (HashMap)
+
+/--
+A monad for traversing all example directives in a document, and
+extracting them into individual files in a directory structured as the
+document is structured. In the `Array (Array String × String)`, the
+first string is the path to the example file we're writing, and the
+second is the body of the example.
+-/
+abbrev ExtractM := ReaderT (Array String) (StateT (Array (Array String × String)) IO)
+
+partial def extractExamples (_mode : Mode) (logError : String → IO Unit) (cfg : Manual.Config) (_state : TraverseState) (text : Part Manual) : IO Unit := do
+
+  let code := (← part text |>.run #[] |>.run #[]).snd
+  let dest := cfg.destination / "extracted-examples"
+  for (ctx, content) in code do
+
+    let filename := ctx.map (Slug.toString ∘ String.sluggify)
+      |>.foldl (init := dest) (· / ·)
+      |>.withExtension "lean"
+    filename.parent.forM IO.FS.createDirAll
+    IO.FS.writeFile filename content
+
+where
+  part : Part Manual → ExtractM Unit
+    | .mk _ titleString _ intro subParts => withReader (·.push titleString) do
+      for b in intro do block b
+      for p in subParts do part p
+  block : Block Manual → ExtractM Unit
+    | .other which contents => do
+      if which.name == `Manual.example then
+        match FromJson.fromJson? which.data (α := Manual.ExampleBlockJson) with
+        | .error e => logError s!"Error deserializing example data: {e}"
+        | .ok (descrString, _, _, _, liveText) =>
+          let context ← read
+          let some txt := liveText
+            | return ()
+          modify fun saved =>
+            saved.push (context.push descrString, txt)
+      for b in contents do block b
+    | .concat bs | .blockquote bs =>
+      for b in bs do block b
+    | .ol _ lis | .ul lis =>
+      for li in lis do
+        for b in li.contents do block b
+    | .dl dis =>
+      for di in dis do
+        for b in di.desc do block b
+    | .para .. | .code .. => pure ()

Manual/Meta/Example.lean

@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 
 import VersoManual
 import Manual.Meta.Figure
+import Manual.Meta.LzCompress
 import Lean.Elab.InfoTree.Types
 
 open Verso Doc Elab
@@ -17,11 +18,15 @@ open Lean Elab
 
 namespace Manual
 
-def Block.example (descriptionString : String) (name : Option String) (opened : Bool) : Block where
+def Block.example (descriptionString : String) (name : Option String) (opened : Bool) (liveText : Option String := none) : Block where
+  -- FIXME: This should be a double-backtickable name
   name := `Manual.example
-  data := ToJson.toJson (descriptionString, name, opened, (none : Option Tag))
+  data := ToJson.toJson (descriptionString, name, opened, (none : Option Tag), liveText)
   properties := .empty |>.insert `Verso.Genre.Manual.exampleDefContext descriptionString
 
+/-- The type of the Json stored with Block.example -/
+abbrev ExampleBlockJson := String × Option String × Bool × Option Tag × Option String
+
 structure ExampleConfig where
   description : FileMap × TSyntaxArray `inline
   /-- Name for refs -/
@@ -58,10 +63,27 @@ def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α  → m β)
 
 def isLeanBlock : TSyntax `block → CoreM Bool
   | `(block|```$nameStx:ident $_args*|$_contents:str```) => do
-    let name ← realizeGlobalConstNoOverloadWithInfo nameStx
+    let name ← realizeGlobalConstNoOverload nameStx
     return name == ``Verso.Genre.Manual.InlineLean.lean
   | _ => pure false
 
+inductive LeanBlockContent where
+ | content : String → LeanBlockContent
+ | elabWithoutKeep : LeanBlockContent
+ | nonLeanBlock : LeanBlockContent
+
+def getLeanBlockContents? : TSyntax `block → DocElabM (LeanBlockContent)
+  | `(block|```$nameStx:ident $args*|$contents:str```) => do
+    let name ← realizeGlobalConstNoOverload nameStx
+    if name != ``Verso.Genre.Manual.InlineLean.lean then
+      return .nonLeanBlock
+    let args ← Verso.Doc.Elab.parseArgs args
+    let args ← parseThe InlineLean.LeanBlockConfig args
+    if !args.keep || args.error then
+      return .elabWithoutKeep
+    pure <| .content (contents.getString)
+  | _ => pure .nonLeanBlock
+
 /--
 Elaborates all Lean blocks first, enabling local forward references
 -/
@@ -73,6 +95,14 @@ def leanFirst : DirectiveExpander
     -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them
     prioritizedElab (isLeanBlock ·) elabBlock contents
 
+/-- Turn a list of lean blocks into one string with the appropriate amount of whitespace -/
+def renderExampleContent (exampleBlocks : List String) : String :=
+  "\n\n".intercalate <| exampleBlocks.map (·.trim)
+
+/-- info: "a\n\nb\n\nc" -/
+#guard_msgs in
+#eval renderExampleContent ["\n  \na\n", "\n b", "c  "]
+
 /-- A domain for named examples -/
 def examples : Domain := {}
 
@@ -89,31 +119,44 @@ def «example» : DirectiveExpander
       (selectionRange := mkNullNode cfg.description.2)
       (kind := Lsp.SymbolKind.interface)
       (detail? := some "Example")
+
+    let accumulate (b : TSyntax `block) : StateT (List String) DocElabM Bool := do
+      match ← getLeanBlockContents? b with
+      | LeanBlockContent.elabWithoutKeep => pure true
+      | LeanBlockContent.nonLeanBlock => pure false
+      | LeanBlockContent.content x =>
+        modify (· ++ [x])
+        pure true
+
     -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them
-    let blocks ←
-      if cfg.keep then
-        prioritizedElab (isLeanBlock ·) elabBlock contents
-      else
-        withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents
+    -- Also accumulate text of lean blocks.
+    let exampleCode := prioritizedElab accumulate (elabBlock ·) contents
+      |>.run []
+    let (blocks, acc) ←
+      if cfg.keep then exampleCode
+      else withoutModifyingEnv <| exampleCode
+    let liveLinkContent := if acc = [] then none else some (renderExampleContent acc)
     -- Examples are represented using the first block to hold the description. Storing it in the JSON
     -- entails repeated (de)serialization.
-    pure #[← ``(Block.other (Block.example $(quote descriptionString) $(quote cfg.tag) (opened := $(quote cfg.opened)))
+    pure #[← ``(Block.other (Block.example $(quote descriptionString) $(quote cfg.tag) (opened := $(quote cfg.opened)) $(quote liveLinkContent))
                 #[Block.para #[$description,*], $blocks,*])]
 
 @[block_extension «example»]
 def example.descr : BlockDescr where
   traverse id data contents := do
-    match FromJson.fromJson? data (α := String × Option String × Bool × Option Tag) with
+    match FromJson.fromJson? data (α := ExampleBlockJson) with
     | .error e => logError s!"Error deserializing example tag: {e}"; pure none
-    | .ok (descrString, none, _, _) => do
+    | .ok (descrString, none, _, _, _) => do
       modify (·.saveDomainObject ``examples descrString id)
       pure none
-    | .ok (descrString, some x, opened, none) =>
+    | .ok (descrString, some x, opened, none, liveText) =>
       modify (·.saveDomainObject ``examples descrString id)
       let path ← (·.path) <$> read
       let tag ← Verso.Genre.Manual.externalTag id path x
-      pure <| some <| Block.other {Block.example descrString none false with id := some id, data := toJson (some x, opened, some tag)} contents
-    | .ok (descrString, some _, _, some _) =>
+      pure <| some <| Block.other {Block.example descrString none false liveText with
+        id := some id,
+        data := toJson (some x, opened, some tag)} contents -- Is this line reachable?
+    | .ok (descrString, some _, _, some _, liveText) =>
       modify (·.saveDomainObject ``examples descrString id)
       pure none
   toTeX :=
@@ -130,21 +173,37 @@ def example.descr : BlockDescr where
       else
         let .para description := blocks[0]
           | HtmlT.logError "Malformed example - description not paragraph"; pure .empty
-        let (descrString, opened) ←
-          match FromJson.fromJson? data (α := String × Option String × Bool × Option Tag) with
-          | .error e => HtmlT.logError s!"Error deserializing example data: {e}"; pure ("", false)
-          | .ok (descrString, _, opened, _) => pure (descrString, opened)
+        let (descrString, opened, liveText) ←
+          match FromJson.fromJson? data (α := ExampleBlockJson) with
+          | .error e => HtmlT.logError s!"Error deserializing example data {data}: {e}"; pure ("", false, none)
+          | .ok (descrString, _, opened, _, liveText) => pure (descrString, opened, liveText)
         let xref ← HtmlT.state
         let ctxt ← HtmlT.context
         let mut attrs := xref.htmlId id
         if opened then
           attrs := attrs.push ("open", "")
         withReader (fun ρ => { ρ with definitionIds := xref.definitionIds ctxt, codeOptions.definitionsAsTargets := true}) do
+          let liveLink := match liveText with
+          | .none => Output.Html.empty
+          | .some content =>
+            let href := "https://live.lean-lang.org/#codez=" ++ lzCompress content
+            {{ <div class="live-link"><a target="_blank" href={{href}}>"Live ↪"</a></div> }}
+          -- TODO(https://github.com/leanprover/verso/issues/569):
+          -- We compute but do not yet add the liveLink inside
+          -- the div.example-content below. That is, we consider this
+          -- "feature-flagged off".
+          --
+          -- We should actually add the link when mechanisms are in place to
+          -- ensure that
+          -- * all reference manual examples yield correct code
+          --   that can be run in a fresh copy of lean
+          -- * we don't produce stale links
           pure {{
             <details class="example" {{attrs}}>
               <summary class="description">{{← description.mapM goI}}</summary>
               <div class="example-content">
                 {{← blocks.extract 1 blocks.size |>.mapM goB}}
+                -- {{liveLink}}
               </div>
             </details>
           }}
@@ -214,6 +273,7 @@ r#".example {
 }
 .example-content {
   padding: 0 var(--verso--box-padding) var(--verso--box-padding);
+  position: relative;
 }
 .example-content > :first-child {
   margin-top: 0;
@@ -224,6 +284,20 @@ r#".example {
 .example .hl.lean.block {
   overflow-x: auto;
 }
+.live-link {
+  font-family: var(--verso-structure-font-family);
+  position: absolute;
+  bottom: 0px;
+  right: 0px;
+  padding: 0.5rem;
+  border-top: 1px solid #98B2C0;
+  border-left: 1px solid #98B2C0;
+  border-top-left-radius: 0.5rem;
+}
+.live-link a {
+  text-decoration: none;
+  color: var(--lean-blue);
+}
 "#
   ]