Allow Verso preview in lean4web for correctly configured projects

.gitignore

@@ -16,6 +16,7 @@ cypress/screenshots
 cypress/videos
 
 **/.lake
+**/_out
 
 # Editor directories and files
 .vscode/*
@@ -27,3 +28,4 @@ cypress/videos
 *.njsproj
 *.sln
 *.sw?
+

Projects/verso-demo/Main.lean

@@ -0,0 +1,6 @@
+import VersoManual
+import VersoDemo
+
+open Verso.Genre Manual
+
+def main := manualMain (%doc VersoDemo) (options := ["--with-html-single"])

Projects/verso-demo/VersoDemo.lean

@@ -0,0 +1,28 @@
+import VersoManual
+import VersoDemo.IntegralApprox
+import VersoDemo.Cantor
+import VersoDemo.DFADiagram
+
+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-demo/VersoDemo/Cantor.lean

@@ -0,0 +1,31 @@
+import VersoManual
+open Verso Genre Manual InlineLean
+
+#doc (Manual) "Cantor's Diagonal Argument" =>
+
+The type of all predicates over a type is that type's _powerset_. Elements of one of these subsets satisfy the predicate:
+```lean
+def Set (α : Type u) : Type u :=
+  α → Prop
+
+instance : Membership α (Set α) where
+  mem xs x := xs x
+```
+
+A function $`f` is surjective if each element of the range is covered by an element of the domain:
+```lean
+def Surjective (f : α → β) :=
+  ∀ y, ∃ x, f x = y
+```
+
+Given a function $`f ∈ S → \mathcal{P}(S)`, Cantor's diagonal argument involves the diagonal set $`\{x ∈ S \mid x \not\in f(x)\}`. The {tactic}`grind` tactic takes care of many reasoning steps:
+```lean
+theorem cantor (f : S → Set S) : ¬ Surjective f := by
+  intro h
+  have ⟨x, p⟩ := h (fun x : S => x ∉ f x)
+  have : x ∈ f x ↔ x ∉ f x := by
+    constructor <;>
+    simp [Membership.mem] at * <;>
+    grind
+  grind
+```

Projects/verso-demo/VersoDemo/DFADiagram.lean

@@ -0,0 +1,117 @@
+import VersoManual
+open Verso Genre Manual InlineLean
+
+#doc (Manual) "DFA Language Equivalence" =>
+
+Coinductive predicates naturally capture bisimulation-like notions, like showing that these two DFAs have equivalent languages:
+
+:::row (align := "top")
+```diagram (cssScale := "0.1") +inline
+open Illuminate in
+let cfg : StateDiagramConfig := {}
+cfg.start 0 |>.atop
+(cfg.accept 0 "ok") |>.atop
+(cfg.state 1 "fail") |>.atop
+(cfg.loop 0 "a") |>.atop
+(cfg.loop 1 "a, b") |>.atop
+(cfg.edge 0 1 "b")
+```
+
+```diagram (cssScale := "0.1") +inline
+open Illuminate in
+let cfg : StateDiagramConfig := {}
+cfg.start 0 |>.atop
+(cfg.accept 0 "start") |>.atop
+(cfg.accept 1 "ok") |>.atop
+(cfg.state 2 "fail") |>.atop
+(cfg.arc 0 1 "a" 30) |>.atop
+(cfg.arc 1 0 "a" (-30)) |>.atop
+(cfg.edge 1 2 "b") |>.atop
+(cfg.arc 0 2 "b" (-140)) |>.atop
+(cfg.loop 2 "a, b")
+```
+:::
+
+# Defining DFAs
+
+:::leanSection
+```lean -show
+variable {Q : Type} {A : Type} {q₀ : Q}
+```
+A deterministic finite automaton is given by a set of states {lean}`Q`, an alphabet {lean}`A`, a start state {lean}`q₀` in {lean}`Q`, a subset of {lean}`Q` that indicates which states are accepting states, and a transition function that takes a state and an element of the alphabet to a new state:
+:::
+
+```lean
+structure DFA (Q : Type) (A : Type) : Type where
+  q₀ : Q
+  δ : Q → A → Q
+  accepting : Q → Bool
+```
+
+Two automata over the same alphabet have equivalent languages from a given pair of states when they agree as to whether these states are accepting and they furthermore have equivalent languages from all successor states according to their transition functions:
+```lean
+def languageEquivalent (M : DFA Q A) (M' : DFA Q' A)
+    (q : Q) (q' : Q') : Prop :=
+  M.accepting q = M'.accepting q' ∧
+    ∀ (a : A), languageEquivalent M M' (M.δ q a) (M'.δ q' a)
+coinductive_fixpoint
+```
+
+The coinduction principle captures the standard notion of bisimulation of deterministic automata:
+```signature
+languageEquivalent.coinduct {Q A Q' : Type}
+  (M : DFA Q A) (M' : DFA Q' A) (pred : Q → Q' → Prop) :
+  (∀ (q : Q) (q' : Q'), pred q q' →
+    M.accepting q = M'.accepting q' ∧
+    ∀ (a : A), pred (M.δ q a) (M'.δ q' a)) →
+  ∀ (q : Q) (q' : Q'), pred q q' →
+    languageEquivalent M M' q q'
+```
+
+# Encoding the Example
+
+The DFAs above can be represented using the following definitions:
+```lean
+inductive Alphabet where | a | b
+
+inductive Q1 where | ok | fail
+
+def loop : DFA Q1 Alphabet where
+  q₀ := .ok
+  δ
+    | .ok, .a => .ok
+    | _, _ => .fail
+  accepting
+    | .ok => True
+    | _ => False
+
+inductive Q2 where | start | ok | fail
+
+def cycle : DFA Q2 Alphabet where
+  q₀ := .start
+  δ
+    | .start, .a => .ok
+    | .ok, .a => .start
+    | _, _ => .fail
+  accepting
+    | .start | .ok => True
+    | .fail => False
+```
+
+# Proving Equivalence
+
+To prove that our two examples are equivalent, the first step is to define a relation that captures their equivalent states.
+Then, coinduction lifts the demonstration that they actually are equivalent in this relation to language equivalence:
+```lean
+theorem loop_equiv_cycle :
+    languageEquivalent loop cycle loop.q₀ cycle.q₀ := by
+  let r : Q1 → Q2 → Prop
+  | .ok, .start
+  | .ok, .ok
+  | .fail, .fail => True
+  | _, _ => False
+  apply languageEquivalent.coinduct (pred := r)
+  . simp only [loop, cycle] <;>
+    grind
+  . simp [r, loop, cycle]
+```

Projects/verso-demo/VersoDemo/IntegralApprox.lean

@@ -0,0 +1,55 @@
+import VersoManual
+open Verso Genre Manual InlineLean
+
+#doc (Manual) "Approximating an Integral" =>
+
+The area under $`\sin x` from $`0` to $`k` can be calculated exactly:
+
+$$`\int_0^k \sin x \,dx = 1 - \cos k`
+
+This means that we can exactly compute the area under $`\sin x` from $`0` to $`1.5` like this:
+
+```lean (name := eval1)
+#eval 1 - Float.cos 1.5
+```
+```leanOutput eval1
+0.929263
+```
+
+But we can approximate this integral with a (left) [Riemann sum](https://en.wikipedia.org/wiki/Riemann_sum).
+If we say we want to break the interval from $`0` to $`k` into $`n` different rectangles, then we can define the left riemann sum as
+
+$$`\sum_{i=0}^{n - 1} \sin x \times dx`
+
+Where $`dx = {k \over n}` and $`x = i \times dx`, which we can then express in Lean like this:
+
+```lean
+def leftSum k n (f : (x dx : Float) → Float) :=
+  List.range n |>.foldl (init := 0) (fun (sum : Float) i =>
+    let dx := k / n.toFloat
+    let x := i.toFloat * dx
+    sum + f x dx)
+
+def integralApprox (k : Float) (n : Nat) : Float :=
+  leftSum k n (fun x dx => Float.sin x * dx)
+```
+
+The error in calculating the area under $`\sin x` from $`0` to $`1.5` with 6 rectangles is about $`0.13`.
+
+```lean (name := eval2)
+#eval (1 - Float.cos 1.5) - integralApprox 1.5 6
+```
+```leanOutput eval2
+0.129532
+```
+
+The error dramatically decreases as we increase the number of rectangles from $`2^0 = 1` to $`2^8 = 256`:
+
+```lean (name := eval3)
+#eval List.range 9 |>.map (fun m => Float.abs
+  ((1 - Float.cos 1.5)
+    - (integralApprox 1.5 (Nat.pow 2 m))))
+```
+```leanOutput eval3
+[0.929263, 0.418034, 0.197946, 0.096239, 0.047438, 0.023549, 0.011732, 0.005855, 0.002925]
+```

Projects/verso-demo/lake-manifest.json

@@ -0,0 +1,56 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/verso",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "4dcbbbc79d41b313af3ab32e9ddb9cf57571427e",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "versobox-shim",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "20b8493528eed2fac9827ce18d41c475f0e1c50a",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "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": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "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": "0bd508e8362f56d4a05cbf63614d4c97db954041",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "«verso-demo»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

Projects/verso-demo/lakefile.toml

@@ -0,0 +1,18 @@
+name = "verso-demo"
+reservoir = false
+defaultTargets = ["VersoDemo"]
+
+[leanOptions]
+pp.unicode.fun = true
+
+[[require]]
+name = "verso"
+scope = "leanprover"
+rev = "versobox-shim"
+
+[[lean_lib]]
+name = "VersoDemo"
+
+[[lean_exe]]
+name = "generate-doc"
+root = "Main"

Projects/verso-demo/lean-toolchain

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

Projects/verso-demo/leanweb-config.json

@@ -0,0 +1,13 @@
+{
+  "name": "_LeanVers_ with Verso",
+  "hidden": false,
+  "verso": true,
+  "examples": [
+    {
+      "file": "VersoDemo/IntegralApprox.lean",
+      "name": "Verso Math and Programming"
+    },
+    { "file": "VersoDemo/Cantor.lean", "name": "Verso Proof States" },
+    { "file": "VersoDemo/DFADiagram.lean", "name": "Verso Diagrams" }
+  ]
+}

client/package.json

@@ -11,33 +11,35 @@
     "@emotion/styled": "^11.14.1",
     "@fortawesome/free-solid-svg-icons": "^7.1.0",
     "@fortawesome/react-fontawesome": "^3.1.1",
+    "@leanprover/infoview-api": "^0.7.0",
     "@mui/material": "^7.3.5",
     "@tailwindcss/vite": "^4.1.18",
     "@tanstack/query-core": "^5.90.14",
     "@uiw/react-codemirror": "^4.25.3",
     "file-saver": "^2.0.5",
+    "jotai": "^2.16.1",
     "jotai-location": "^0.6.2",
     "jotai-react": "^0.0.0",
     "jotai-tanstack-query": "^0.11.0",
-    "jotai": "^2.16.1",
     "lean4monaco": "^1.1.11",
     "lz-string": "^1.5.0",
+    "react": "^19.2.0",
     "react-dom": "^19.2.0",
     "react-split": "^2.0.14",
-    "react": "^19.2.0",
     "tailwindcss": "^4.1.18",
     "vscode-ws-jsonrpc": "^3.5.0"
   },
   "devDependencies": {
     "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
     "@types/file-saver": "^2.0.7",
-    "@types/react-dom": "^19.2.3",
     "@types/react": "^19.2.7",
+    "@types/react-dom": "^19.2.3",
+    "@types/vscode": "^1.89.0",
     "@vitejs/plugin-react-swc": "^4.2.2",
     "typescript": "^5.9.3",
+    "vite": "^7.2.4",
     "vite-plugin-node-polyfills": "0.24.0",
     "vite-plugin-static-copy": "^3.1.4",
-    "vite-plugin-svgr": "^4.5.0",
-    "vite": "^7.2.4"
+    "vite-plugin-svgr": "^4.5.0"
   }
 }