[demo] Plugin design

.gitignore

@@ -17,6 +17,10 @@ cypress/videos
 
 **/.lake
 
+_out
+
+verso-server/*.js
+
 # Editor directories and files
 .vscode/*
 !.vscode/extensions.json

Projects/MathlibDemo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bfd79bd53242ce07c2f41264531699b721cd209d",
+   "rev": "32fe3f9354729a268ba178d0b5ae06eca180c247",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1603151ac0db4e822908e18094f16acc250acaff",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.62",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c3a19fa17982c5c1413fea335f371869b8b12e1d",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e1d2994e0acdee2f0c03c9d84d28a5df34aa0020",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5e6a77528fb6cace1f0adf2563e4e1bc1da541ae",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "a0abd472348dd725adbb26732e79b26e7e220913",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "MathlibDemo",

Projects/MathlibDemo/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0-rc3
+leanprover/lean4:v4.28.0

Projects/mathlib-stable/build.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+# See ../MathlibDemo/build.sh
+cd $(dirname $0)
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/stable/lean-toolchain -o lean-toolchain
+lake update -R
+lake build
+lake build Batteries

Projects/mathlib-stable/lake-manifest.json

@@ -1,77 +1,95 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "scope": "",
+   "rev": "bb4673611f3fc40318e250422015a5cf122c9ca4",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "stable",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
-   "name": "Qq",
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
-   "name": "aesop",
+   "scope": "leanprover-community",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "scope": "leanprover-community",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
-   "name": "importGraph",
+   "scope": "leanprover-community",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "971ecd03805fe1026721e65f53ef163132abb75c",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "stable",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hhu-adam/lean4web-tools.git",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "8be7734dfa9a686d3a1329651e2a1a690e1123b6",
-   "name": "webeditor",
+   "scope": "leanprover",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "v4.28.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "mathlibStable",
  "lakeDir": ".lake"}

Projects/mathlib-stable/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.28.0

Projects/verso-nightly/MakeVerso.lean

@@ -0,0 +1,42 @@
+import TheLeanFile
+import Lean
+import Verso.Doc
+import VersoManual
+import VersoBlog
+
+open Lean Elab.Term
+
+#eval show TermElabM _ from do
+  let env ← getEnv
+
+  match env.constants.find? (Verso.Doc.docName `TheLeanFile) with
+  | .none =>
+    throwError "The lean file provided does not contain a Verso document"
+
+  | .some (.defnInfo doc) =>
+    let destination := (← IO.getEnv "VERSO_OUTPUT_PATH").map (⟨·⟩)
+      |>.getD ((← IO.currentDir).join "_out")
+    Verso.FS.ensureDir destination
+
+    let extensionImpls := by exact extension_impls%
+    let numErrs ← IO.mkRef 0
+    let logError := fun err => do
+      println! s!"Error while creating document: {err}"
+      numErrs.set ((← numErrs.get) + 1)
+    let renderConfig : Verso.Genre.Manual.RenderConfig := { destination }
+
+    -- We would like to write this:
+    -- let part := TheLeanFile.«the canonical document object name»
+    -- But that presumes the identifier exists, and we want this file to
+    -- elaborate successfully even if the import does not contain the files
+    -- we expect it to. Therefore, we run this instead:
+    let part ← Meta.evalExpr (Verso.Doc.VersoDoc Verso.Genre.Manual)
+      (mkApp (mkConst ``Verso.Doc.VersoDoc [])
+      (mkConst ``Verso.Genre.Manual []))
+      (doc.value)
+
+    let (text, traversalState) ← Verso.Genre.Manual.traverseHtmlSingle logError renderConfig part.toPart extensionImpls
+    Verso.Genre.Manual.emitXrefsJson (destination.join "html-single") traversalState
+    Verso.Genre.Manual.emitHtmlSingle logError renderConfig text traversalState extensionImpls
+  | .some _ =>
+    throwError "Document does not contain an expected definition"

Projects/verso-nightly/MakeVerso/VersoExample.lean

@@ -0,0 +1,24 @@
+import VersoManual
+open Verso Doc
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+
+#doc (Manual) "My Document" =>
+
+This is a Verso document.
+
+It can include inline math, like this: $`x + 4 = -3`.
+
+It can also include block math, like
+$$`\int_\mathsf{this}^\mathtt{orthis} \mathit{or{\ldots}maybe{\ldots}this}`
+
+We also support inline lean, like this: {lean}`Nat.add_assoc`.
+
+We also support block lean, like this:
+
+```lean
+/-- The name we will be greeting -/
+def theName := "Jimothy"
+
+#eval s!"Hello {theName}"
+```

Projects/verso-nightly/TheLeanFile.lean

@@ -0,0 +1,2 @@
+import VersoManual
+#doc (Verso.Genre.Manual) "My Document" => Verso doc

Projects/verso-nightly/build.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+# See ../MathlibDemo/build.sh, this is the same principle but for verso/nightly-testing
+cd $(dirname $0)
+curl -L https://raw.githubusercontent.com/leanprover/verso/nightly-testing/lean-toolchain -o lean-toolchain
+lake update -R
+lake build
+lake exe mkdoc --output /dev/null

Projects/verso-nightly/lake-manifest.json

@@ -0,0 +1,45 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/verso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3acc4cac70687728914505097174511748f4ec0e",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7e097e9a076d5fbe48aa39aceee871af0d011101",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4539e605ff834c35ecc0bcd0b7daec69163fd9f0",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "«verso-nightly»",
+ "lakeDir": ".lake"}

Projects/verso-nightly/lakefile.toml

@@ -0,0 +1,16 @@
+name = "verso-nightly"
+version = "0.1.0"
+moreLeancArgs = ["-O0"]
+defaultTargets = ["TheLeanFile", "MakeVerso"]
+
+[[require]]
+name = "verso"
+git = "https://github.com/leanprover/verso"
+rev = "nightly-testing"
+
+[[lean_lib]]
+name = "TheLeanFile"
+
+[[lean_lib]]
+name = "MakeVerso"
+

Projects/verso-nightly/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2026-02-16