diff --git a/.gitignore b/.gitignore index 475c7bcb..22149372 100644 --- a/.gitignore +++ b/.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? + diff --git a/Projects/verso-demo/Main.lean b/Projects/verso-demo/Main.lean new file mode 100644 index 00000000..d00fdcbf --- /dev/null +++ b/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"]) diff --git a/Projects/verso-demo/VersoDemo.lean b/Projects/verso-demo/VersoDemo.lean new file mode 100644 index 00000000..db6c7fb9 --- /dev/null +++ b/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}" +``` diff --git a/Projects/verso-demo/VersoDemo/Cantor.lean b/Projects/verso-demo/VersoDemo/Cantor.lean new file mode 100644 index 00000000..fa13293b --- /dev/null +++ b/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 +``` diff --git a/Projects/verso-demo/VersoDemo/DFADiagram.lean b/Projects/verso-demo/VersoDemo/DFADiagram.lean new file mode 100644 index 00000000..1dc4d538 --- /dev/null +++ b/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] +``` diff --git a/Projects/verso-demo/VersoDemo/IntegralApprox.lean b/Projects/verso-demo/VersoDemo/IntegralApprox.lean new file mode 100644 index 00000000..1a1db43b --- /dev/null +++ b/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] +``` diff --git a/Projects/verso-demo/lake-manifest.json b/Projects/verso-demo/lake-manifest.json new file mode 100644 index 00000000..5306c0d5 --- /dev/null +++ b/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} diff --git a/Projects/verso-demo/lakefile.toml b/Projects/verso-demo/lakefile.toml new file mode 100644 index 00000000..b32e75ef --- /dev/null +++ b/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" diff --git a/Projects/verso-demo/lean-toolchain b/Projects/verso-demo/lean-toolchain new file mode 100644 index 00000000..18640c8b --- /dev/null +++ b/Projects/verso-demo/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.31.0 diff --git a/Projects/verso-demo/leanweb-config.json b/Projects/verso-demo/leanweb-config.json new file mode 100644 index 00000000..581e94e0 --- /dev/null +++ b/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" } + ] +} diff --git a/client/package.json b/client/package.json index 2081009d..27fb49d5 100644 --- a/client/package.json +++ b/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" } } diff --git a/client/src/App.tsx b/client/src/App.tsx index 48612314..fb81c166 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,8 +1,6 @@ import './css/App.css' import './css/Editor.css' -import { faCode } from '@fortawesome/free-solid-svg-icons' -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import CodeMirror, { EditorView } from '@uiw/react-codemirror' import { useAtom } from 'jotai/react' import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco' @@ -11,8 +9,8 @@ import * as path from 'path' import { useCallback, useEffect, useRef, useState } from 'react' import Split from 'react-split' -import LeanLogo from './assets/logo.svg' import { codeAtom } from './editor/code-atoms' +import InfoPane from './InfoPane' import { Menu } from './navigation/Navigation' import { mobileAtom, settingsAtom } from './settings/settings-atoms' import { lightThemes } from './settings/settings-types' @@ -303,17 +301,21 @@ function App() {
-

- You are in the plain text editor -
-
- Go back to the Monaco Editor (click ) for the infoview - to update! -

+
diff --git a/client/src/InfoPane.tsx b/client/src/InfoPane.tsx new file mode 100644 index 00000000..0bf515c2 --- /dev/null +++ b/client/src/InfoPane.tsx @@ -0,0 +1,212 @@ +import './css/InfoPane.css' + +import { faCode } from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { isRpcError, RpcErrorCode } from '@leanprover/infoview-api' +import { LeanClient, LeanMonaco } from 'lean4monaco' +import { RefObject, useEffect, useState } from 'react' + +interface InfoPaneProps { + infoviewRef: RefObject + codeMirror: boolean + isVerso: boolean + leanMonaco: LeanMonaco | undefined +} + +const TABS = ['Infoview', 'Verso'] as const + +/** + * Upon detecting a Verso document has finished elaborating, we will + * immediately request the HTML document the first time. The next request will + * be delayed by DEBOUNCE_MS milliseconds. + */ +const DEBOUNCE_MS = 1_000 + +type GetVersoContentsResult = { success: string } | { errors: string[] } | 'noDoc' +type VersoState = GetVersoContentsResult | 'loading' | 'noRpc' + +async function getVersoContents(client: LeanClient, uri: string): Promise { + const { sessionId } = await client.sendRequest('$/lean/rpc/connect', { uri }) + const result = await client.sendRequest('$/lean/rpc/call', { + textDocument: { uri }, + position: { line: 0, character: 0 }, + sessionId, + method: 'Verso.getLiveDocument', + params: {}, + }) + return result +} + +/** + * Wraps the useEffect handler that controls Verso RPCs. + */ +function useVersoRPC( + leanMonaco: LeanMonaco | undefined, + isVerso: boolean, + setVersoState: (srcDoc: VersoState) => void, +) { + useEffect(() => { + if (!leanMonaco?.clientProvider) return + if (!isVerso) return + + // There's only going to be one client and two subscriptions, but the API is + // set up for many and it's easier to go along with that design + const subscriptions: { dispose: () => void }[] = [] + + let currentDocumentVersion = -1 + let currentVersionHasRpcRequest = false + let versionDebounceTimer: ReturnType | undefined = undefined + + const report = async (client: LeanClient, uri: string) => { + const documentVersionBeforeRpc = currentDocumentVersion + currentVersionHasRpcRequest = true + + try { + const result = await getVersoContents(client, uri) + if (currentDocumentVersion !== documentVersionBeforeRpc) { + console.log('ignoring stale RPC response', result) + return + } + setVersoState(result) + } catch (e) { + if (isRpcError(e) && e.code === RpcErrorCode.RpcNeedsReconnect) { + return + } else if (isRpcError(e) && e.code === RpcErrorCode.MethodNotFound) { + setVersoState('noRpc') + } else { + console.warn('There was an error collecting verso content:', e) + } + } + } + + const register = (client: LeanClient) => { + console.log('CLIENT: ', client) + + subscriptions.push( + client.didChange(({ textDocument }) => { + currentVersionHasRpcRequest = false + currentDocumentVersion = textDocument.version + }), + ) + subscriptions.push( + client.progressChanged(([uri, processing]) => { + if (processing.length > 0) return // partial progress only + if (currentVersionHasRpcRequest) return // there are usually duplicate signals + if (versionDebounceTimer === undefined) { + void report(client, uri) + versionDebounceTimer = setTimeout(() => { + versionDebounceTimer = undefined + }, DEBOUNCE_MS) + } else { + clearTimeout(versionDebounceTimer) + versionDebounceTimer = setTimeout(() => { + versionDebounceTimer = undefined + void report(client, uri) + }, DEBOUNCE_MS) + } + }), + ) + } + + // realistically, there's one client ever + // but we add the watcher to "all clients" (all one of them in lean4web) + leanMonaco.clientProvider.getClients().forEach(register) + // and to all future clients (there won't be any of them in lean4web) + subscriptions.push(leanMonaco.clientProvider.clientAdded(register)) + + return () => { + clearTimeout(versionDebounceTimer) + subscriptions.forEach((d) => d.dispose()) + } + }, [leanMonaco, isVerso, setVersoState]) +} + +export default function InfoPane({ codeMirror, infoviewRef, isVerso, leanMonaco }: InfoPaneProps) { + const [tab, setTab] = useState<(typeof TABS)[number]>(isVerso ? 'Verso' : 'Infoview') + const [versoState, setVersoState] = useState('loading') + useVersoRPC(leanMonaco, isVerso, setVersoState) + + return ( +
+ {isVerso && ( +
+ {TABS.map((label) => ( + + ))} +
+ )} + + {isVerso && + tab === 'Verso' && + (versoState === 'loading' ? ( +
+

Loading...

+
+ ) : versoState === 'noRpc' ? ( +
+

+ This Lean file does not import VersoManual, so it's not possible to read out a Lean + document. +

+

+ Switch to the Infoview tab (or a different project) to work on a normal Lean + development. +

+
+ ) : versoState === 'noDoc' ? ( +
+

+ Verso did not find a VersoManual document in this Lean file. This may be because + you're missing a #doc command, or it + may be because a Lean type error prevented the document from loading correctly. +

+

Switching to the Infoview tab may help you diagnose the problem.

+
+ ) : 'success' in versoState ? ( +