feat: initial code example extraction

.github/workflows/ci.yml

@@ -12,7 +12,7 @@ jobs:
           - "leanprover/lean4:4.3.0"
           - "leanprover/lean4:4.4.0"
           - "leanprover/lean4:4.5.0"
-          - "leanprover/lean4:4.6.0-rc1"
+          - "leanprover/lean4:4.6.0"
     name: Build and test
     runs-on: ubuntu-latest
     steps:
@@ -46,6 +46,12 @@ jobs:
         run: |
           lake build
 
+      - name: Configure demo/test subproject
+        run: |
+          pushd demo
+          lake update
+          popd
+
       - name: Run tests
         run: |
           lake exe subverso-tests

Extract.lean

@@ -0,0 +1,24 @@
+import Lean
+import Subverso.Examples.Env
+
+open Lean
+open Subverso.Examples
+
+def main : (args : List String) → IO UInt32
+  | [mod, outFile] => do
+    try
+      initSearchPath (← findSysroot)
+      let env ← importModules #[{module := mod.toName, runtimeOnly := false}] {}
+      let modExamples := highlighted.getState env
+      let exJson := Json.mkObj <| modExamples.toList.map (fun p => {p with fst := p.fst.toString (escape := false)})
+      IO.println s!"Processed {modExamples.size} examples"
+      if let some p := (outFile : System.FilePath).parent then
+        IO.FS.createDirAll p
+      IO.FS.writeFile outFile (toString exJson ++ "\n")
+      return 0
+    catch e =>
+      IO.eprintln s!"error finding highlighted code: {toString e}"
+      return 2
+  | other => do
+    IO.eprintln s!"Didn't understand args: {other}"
+    pure 1

README.md

@@ -1,9 +1,67 @@
-# Subverso - Verso's Library for Subprocesses
+# SubVerso - Verso's Library for Subprocesses
 
-Subverso is a support library that allows a
+SubVerso is a support library that allows a
 [Verso](https://github.com/leanprover/verso) document to describe Lean
 code written in multiple versions of Lean. Verso itself may be tied to
 new Lean versions, because it makes use of new compiler features. This
 library will maintain broader compatibility with various Lean versions.
 
+## Versions and Compatibility
+
+SubVerso's CI currently validates it on every Lean release since
+4.3.0, along with whatever version or snapshot is currently targeted
+by Verso itself.
+
+There should be no expectations of compatibility between different
+versions of SubVerso, however - the specifics of its data formats is
+an implementation detail, not a public API. Please use SubVerso itself
+to read and write the data.
+
+## Features
+
+### Code Examples
+
+Presently, SubVerso supports the extraction of highlighting
+information from code. There may be a many-to-many relationship
+between Lean modules and documents that describe them. In these cases,
+using SubVerso's examples library to indicate examples to be shown in
+the text can be useful.
+
+This feature may also be useful for other applications that require
+careful presentation of Lean code.
+
+To use this feature, first add a dependency on `subverso` to your
+Lakefile:
+
+```
+require subverso from git "[email protected]:leanprover/subverso.git"
+```
+
+Then, in the modules that contain code examples to be used in
+documentation, add the following to the imports list:
+```
+import SubVerso.Examples
+```
+and open the namespace within which the new (scoped) operators are defined:
+```
+open SubVerso.Examples
+```
+
+This library defines two new pieces of syntax. Wrapping a sequence of
+commands in `%example NAME` and `%end` causes their data to be saved
+under the key `NAME`. Any `%ex{NAME2}{T}` expressions within the
+command are additionally saved under the key `NAME2`, with the `%ex`
+annotation removed from the highlighted code.
+
+For instance, if the module to be highlighted contains:
+```
+%example F
+def f (n : Nat) : Nat := %ex{plus23}{$ex{N}{n} + 23}
+
+#eval f 5
+%end
+```
+then three pieces of highlighted code are saved, named `F` (the whole
+block), `plus23` (which contains `n + 23`), and `N` (which contains
+`n`).
 

Tests.lean

@@ -1,3 +1,28 @@
 import Subverso.Highlighting
+import Subverso.Examples
+import Subverso.Examples.Env
+import Lean
 
-def main : IO UInt32 := pure 0
+open Subverso.Examples (loadExamples Example)
+open Lean.FromJson (fromJson?)
+
+def assert (what : String) (cond : Unit -> Bool) : IO Unit := do
+  if !(cond ()) then
+    throw <| .userError what
+
+
+def main : IO UInt32 := do
+  IO.println "Checking that the test project generates at least some deserializable JSON"
+  let examples ← loadExamples "demo"
+  assert "Examples are non-empty" fun () => !examples.isEmpty
+  let _exs : List (List (String × Example)) ← examples.toList.mapM fun (n, ex) => do
+    let mut out := []
+    match ex.getObj? with
+    | .error err => throw <| IO.userError <| s!"Expected object for {n}: " ++ err
+    | .ok val =>
+      for ⟨k, v⟩ in val.toArray do
+        match Lean.FromJson.fromJson? v with
+        | .error err => throw <| IO.userError <| s!"Failed to deserialize {n}: " ++ err
+        | .ok val => out := (k, val) :: out
+      pure out
+  pure 0

demo/.gitignore

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

demo/Demo.lean

@@ -0,0 +1,11 @@
+-- This module serves as the root of the `Demo` library.
+-- Import modules here that should be built as part of the library.
+import «Demo».Basic
+
+import Subverso.Examples
+
+open Subverso.Examples
+
+%example xdef
+def f (x : Nat) := %ex{add}{33 + %ex{X}{x}}
+%end

demo/Demo/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

demo/Main.lean

@@ -0,0 +1,4 @@
+import «Demo»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

demo/lakefile.lean

@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+require subverso from ".."
+
+package «demo» where
+  -- add package configuration options here
+
+lean_lib «Demo» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «demo» where
+  root := `Main

demo/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2024-02-26

lakefile.lean

@@ -15,3 +15,49 @@ lean_lib SubversoExamples where
 @[default_target]
 lean_exe «subverso-tests» where
   root := `Tests
+
+@[default_target]
+lean_exe «subverso-extract» where
+  root := `Extract
+
+module_facet examples mod : FilePath := do
+  let ws ← getWorkspace
+  let some extract ← findLeanExe? `«subverso-extract»
+    | error "The subverso-extract executable was not found"
+
+  let exeJob ← extract.exe.fetch
+  let modJob ← mod.leanArts.fetch
+
+  let buildDir := ws.root.buildDir
+  let hlFile := mod.filePath (buildDir / "examples") "json"
+
+  exeJob.bindAsync fun exeFile exeTrace =>
+    modJob.bindSync fun () modTrace => do
+      let depTrace := mixTrace exeTrace modTrace
+      let trace ← buildFileUnlessUpToDate hlFile depTrace do
+        logStep s!"Exporting highlighted example JSON for '{mod.name}'"
+        proc {
+          cmd := exeFile.toString
+          args := #[mod.name.toString, hlFile.toString]
+          env := ← getAugmentedEnv
+        }
+      pure (hlFile, trace)
+
+library_facet examples lib : FilePath := do
+  let ws ← getWorkspace
+  let mods ← lib.modules.fetch
+  let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `examples)
+  let buildDir := ws.root.buildDir
+  let hlDir := buildDir / "examples"
+  moduleJobs.bindSync fun () trace => do
+    pure (hlDir, trace)
+
+package_facet examples pkg : FilePath := do
+  let ws ← getWorkspace
+  let libs := pkg.leanLibs
+  let libJobs ← BuildJob.mixArray <| ← libs.mapM (fetch <| ·.facet `examples)
+  let buildDir := ws.root.buildDir
+  let hlDir := buildDir / "examples"
+  libJobs.bindSync fun () trace => do
+    logStep s!"Highlighted code written to '{hlDir}'"
+    pure (hlDir, trace)

src/examples/Subverso/Examples.lean

@@ -0,0 +1,148 @@
+import Subverso.Highlighting
+import Subverso.Examples.Env
+import Lean.Environment
+
+namespace Subverso.Examples
+
+open Subverso Highlighting
+
+open Lean Elab Command Term
+
+scoped syntax "%ex" "{" ident (" : " term)? "}" "{" term "}" : term
+scoped syntax "%ex" "{" ident "}" "{" tactic "}" : tactic
+scoped syntax "%ex" "{" ident "}" "{" doElem "}" : doElem
+
+
+class MonadMessageState (m : Type → Type v) where
+  getMessages : m MessageLog
+  setMessages : MessageLog → m Unit
+
+instance : MonadMessageState TermElabM where
+  getMessages := do return (← getThe Core.State).messages
+  setMessages msgs := modifyThe Core.State ({· with messages := msgs})
+
+instance : MonadMessageState CommandElabM where
+  getMessages := do return (← get).messages
+  setMessages msgs := modify ({· with messages := msgs})
+
+open MonadMessageState in
+def savingNewMessages [Monad m] [MonadFinally m] [MonadMessageState m]
+    (act : m α) : m (α × MessageLog) := do
+  let startMessages ← getMessages
+  let mut endMessages := .empty
+  setMessages .empty
+  let res ← try
+    let res ← act
+    endMessages ← getMessages
+    pure res
+  finally
+    setMessages (startMessages ++ endMessages)
+  pure (res, endMessages)
+
+scoped syntax "%example" ident command command* "%end" : command
+
+example : TermElabM Unit := logError "foo"
+
+partial def extractExamples (stx : Syntax) : StateT (NameMap Syntax) Id Syntax := do
+  if let `(term|%ex { $n:ident }{ $tm:term }) := stx then
+    let next ← extractExamples tm
+    -- Save the erased version in case there's nested examples
+    modify fun st => st.insert n.getId next
+    pure next
+  else
+    match stx with
+    | .node info kind args => pure <| .node info kind (← args.mapM extractExamples)
+    | _ => pure stx
+
+elab_rules : command
+  | `(%example $name:ident $cmd $cmds* %end) => do
+    let allCommands := #[cmd] ++ cmds
+    let (allCommands, termExamples) := allCommands.mapM extractExamples .empty
+    let ((), newMessages) ← savingNewMessages (allCommands.forM elabCommand)
+    let trees ← getInfoTrees
+    let hl ← allCommands.mapM fun c => liftTermElabM (highlight c newMessages.toList.toArray trees)
+    let freshMsgs ← newMessages.toList.mapM fun m => do pure (m.severity, ← m.toString)
+    let .original leading startPos _ _ := allCommands[0]!.getHeadInfo
+      | throwErrorAt allCommands[0]! "Failed to get source position"
+    let .original _ _ trailing stopPos := allCommands.back.getTailInfo
+      | throwErrorAt allCommands.back "Failed to get source position"
+    let text ← getFileMap
+    let str := text.source.extract leading.startPos trailing.stopPos
+    modifyEnv fun ρ => highlighted.addEntry ρ (name.getId, {highlighted := hl, original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
+    for (name, term) in termExamples do
+      let hl ← liftTermElabM (highlight term newMessages.toList.toArray trees)
+      let .original leading startPos _ _ := term.getHeadInfo
+        | throwErrorAt term "Failed to get source position"
+      let .original _ _ trailing stopPos := term.getTailInfo
+        | throwErrorAt term "Failed to get source position"
+      let str := text.source.extract leading.startPos trailing.stopPos
+      modifyEnv fun ρ => highlighted.addEntry ρ (name, {highlighted := #[hl], original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
+
+scoped syntax "%dump" ident : command
+
+elab_rules : command
+  | `(%dump%$kw $name:ident) => do
+    let st := highlighted.getState (← getEnv)
+    if let some json := st.find? name.getId then
+      logInfoAt kw m!"{toString json}"
+    else
+      throwErrorAt name "No highlighting found for '{name}'"
+
+open System in
+partial def loadExamples (leanProject : FilePath) : IO (NameMap Json) := do
+  -- Validate that the path is really a Lean project
+  let lakefile := leanProject / "lakefile.lean"
+  if !(← lakefile.pathExists) then
+    throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project"
+  -- Build the facet
+  let res ← IO.Process.output {
+    cmd := "lake"
+    args := #["build", ":examples"]
+    cwd := leanProject
+  }
+  if res.exitCode != 0 then
+    throw <| .userError <|
+      "Build process failed." ++
+      decorateOut "stdout" res.stdout ++
+      decorateOut "stderr" res.stderr
+  let hlDir := leanProject / ".lake" / "build" / "examples"
+  collectExamples .anonymous hlDir
+where
+  decorateOut (name : String) (out : String) : String :=
+    if out.isEmpty then "" else s!"\n{name}:\n{out}\n"
+  collectExamples (name : Name) (dir : FilePath) : IO (NameMap Json) := do
+    let contents ← dir.readDir
+    let mut out := {}
+    for f in contents do
+      match (← f.path.metadata).type with
+      | .dir =>
+        let sub ← collectExamples (.str name f.fileName) f.path
+        out := out.mergeBy (fun _ _ j2 => j2) sub
+      | .file =>
+        if f.path.extension == some "json" then
+          if let some mod := f.path.fileStem then
+            let name' : Name := .str name mod
+            let contents := Json.parse (← IO.FS.readFile f.path)
+            match contents with
+            | .error err => throw <| .userError s!"Couldn't parse {f.path} as JSON: {err}"
+            | .ok val =>
+              out := out.insert name' val
+      | _ => pure ()
+    return out
+
+
+%example test3
+def wxyz (n : Nat) := 1 + 3 + n
+#check wxyz
+def xyz (n : Nat) := 1 + %ex{test2}{3 + n}
+%end
+
+--%process_highlights
+
+-- %example test
+-- #eval 5
+-- %end
+
+-- %dump test
+%dump test2
+%dump test3