diff --git a/.gitignore b/.gitignore index 475c7bcb..c4841d7a 100644 --- a/.gitignore +++ b/.gitignore @@ -17,6 +17,10 @@ cypress/videos **/.lake +_out + +verso-server/*.js + # Editor directories and files .vscode/* !.vscode/extensions.json diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json index c9a1cbb7..c9a56e92 100644 --- a/Projects/MathlibDemo/lake-manifest.json +++ b/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", diff --git a/Projects/MathlibDemo/lean-toolchain b/Projects/MathlibDemo/lean-toolchain index 1efd3655..4c685fa0 100644 --- a/Projects/MathlibDemo/lean-toolchain +++ b/Projects/MathlibDemo/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0-rc3 +leanprover/lean4:v4.28.0 diff --git a/server/build.sh b/Projects/build.sh similarity index 100% rename from server/build.sh rename to Projects/build.sh diff --git a/Projects/mathlib-stable/build.sh b/Projects/mathlib-stable/build.sh new file mode 100755 index 00000000..255ae061 --- /dev/null +++ b/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 diff --git a/Projects/mathlib-stable/lake-manifest.json b/Projects/mathlib-stable/lake-manifest.json index ad0112d2..21c7a4c4 100644 --- a/Projects/mathlib-stable/lake-manifest.json +++ b/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"} diff --git a/Projects/mathlib-stable/lean-toolchain b/Projects/mathlib-stable/lean-toolchain index 9ad30404..4c685fa0 100644 --- a/Projects/mathlib-stable/lean-toolchain +++ b/Projects/mathlib-stable/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.28.0 diff --git a/Projects/verso-nightly/MakeVerso.lean b/Projects/verso-nightly/MakeVerso.lean new file mode 100644 index 00000000..915ccd30 --- /dev/null +++ b/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" diff --git a/Projects/verso-nightly/MakeVerso/VersoExample.lean b/Projects/verso-nightly/MakeVerso/VersoExample.lean new file mode 100644 index 00000000..0177ded5 --- /dev/null +++ b/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}" +``` diff --git a/Projects/verso-nightly/TheLeanFile.lean b/Projects/verso-nightly/TheLeanFile.lean new file mode 100644 index 00000000..d239abbd --- /dev/null +++ b/Projects/verso-nightly/TheLeanFile.lean @@ -0,0 +1,2 @@ +import VersoManual +#doc (Verso.Genre.Manual) "My Document" => Verso doc diff --git a/Projects/verso-nightly/build.sh b/Projects/verso-nightly/build.sh new file mode 100755 index 00000000..cabd3ac5 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Projects/verso-nightly/lake-manifest.json b/Projects/verso-nightly/lake-manifest.json new file mode 100644 index 00000000..dd17b050 --- /dev/null +++ b/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"} diff --git a/Projects/verso-nightly/lakefile.toml b/Projects/verso-nightly/lakefile.toml new file mode 100644 index 00000000..55f7e7ac --- /dev/null +++ b/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" + diff --git a/Projects/verso-nightly/lean-toolchain b/Projects/verso-nightly/lean-toolchain new file mode 100644 index 00000000..ac6ebec5 --- /dev/null +++ b/Projects/verso-nightly/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2026-02-16 diff --git a/client/src/App.tsx b/client/src/App.tsx index 42d60da3..282493eb 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -21,6 +21,8 @@ import { useWindowDimensions } from './utils/WindowWidth' // CSS import './css/App.css' import './css/Editor.css' +import TabView from './TabView' +import { LeanWebPlugin } from './config/docs' /** Returns true if the browser wants dark mode */ function isBrowserDefaultDark() { @@ -54,6 +56,7 @@ function App() { const [project, setProject] = useState(undefined) const [url, setUrl] = useState(null) const [codeFromUrl, setCodeFromUrl] = useState('') + const [tab, setTab] = useState(null) /** Monaco editor requires the code to be set manually. */ function setContent (code: string) { @@ -74,6 +77,8 @@ function App() { setContent(_code) } + if (args.tab) {setTab(args.tab)} + if (args.url) {setUrl(lookupUrl(decodeURIComponent(args.url)))} // if no project provided, use default @@ -310,25 +315,29 @@ function App() { if (!editor) { return } let _project = (project == 'MathlibDemo' ? null : project) + let _tab = (tab == 'info' ? null : tab) let args: { project: string | null url: string | null code: string | null codez: string | null + tab: string | null } if (code === "") { args = { project: _project, url: null, code: null, - codez: null + codez: null, + tab: _tab } } else if (url != null && code == codeFromUrl) { args = { project: _project, url: encodeURIComponent(url), code: null, - codez: null + codez: null, + tab: _tab } } else if (preferences.compress) { // LZ padds the string with trailing `=`, which mess up the argument parsing @@ -343,7 +352,8 @@ function App() { project: _project, url: null, code: null, - codez: compressed + codez: compressed, + tab: _tab } // } else { // args = { @@ -358,11 +368,12 @@ function App() { project: _project, url: null, code: fixedEncodeURIComponent(code), - codez: null + codez: null, + tab: _tab } } history.replaceState(undefined, undefined!, formatArgs(args)) - }, [editor, project, code, codeFromUrl]) + }, [editor, project, code, codeFromUrl, tab]) // Disable monaco context menu outside the editor useEffect(() => { @@ -429,13 +440,16 @@ 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/TabPlugins/VersoPreview.tsx b/client/src/TabPlugins/VersoPreview.tsx new file mode 100644 index 00000000..a6ebe841 --- /dev/null +++ b/client/src/TabPlugins/VersoPreview.tsx @@ -0,0 +1,95 @@ +import { useEffect, useRef, useState } from 'react' +import { LeanWebPlugin } from '../config/docs' +import { TabId } from '../TabView' + +interface VersoPreviewProps { + currentTab: 'info' | LeanWebPlugin + code: string + projectId: string +} + +function VersoPreview({ currentTab, code, projectId }: VersoPreviewProps) { + const [isLoading, setIsLoading] = useState(false) + const [previewedCode, setPreviewedCode] = useState(null) + const [hrefForIframe, setHrefForIframe] = useState(null) + const [output, setOutput] = useState([]) + const scrollerRef = useRef(null) + + const loadCode = () => { + setIsLoading(true) + setOutput([]) + + const read = new EventSource('/verso/api/stream') + read.onerror = (x) => console.log({ error: x }) + read.onmessage = ({ data }) => { + const line = JSON.parse(data) + setOutput((info) => [...info, line.contents]) + } + read.addEventListener('connect', (event) => { + const streamId = event.data + setOutput((info) => [...info, 'connected!']) + + fetch(`/verso/api/singlepage?stream=${streamId}`, { + method: 'POST', + headers: { + 'Content-Type': 'application/json', + }, + body: JSON.stringify({ projectId: projectId, fileContents: code }), + }) + .then((resp) => resp.json()) + .then((json) => { + setIsLoading(false) + if (!json.success) { + setOutput((info) => [...info, json.result ?? 'Unexpected response from server.']) + console.error(json) + return + } + setHrefForIframe(json.href) + setPreviewedCode(code) + }) + .catch((err) => { + setIsLoading(false) + setOutput((info) => [...info, 'Unexpected response from server.']) + console.error(err) + }) + .finally(() => read.close()) + }) + } + + const [lastTab, setLastTab] = useState(null) + useEffect(() => { + if (lastTab && lastTab === currentTab) return + setLastTab(currentTab) + if (currentTab !== 'versobox') return + if (code === previewedCode) return + if (isLoading) return + loadCode() + }, [currentTab, lastTab]) + + useEffect(() => { + scrollerRef.current.scrollTop = scrollerRef.current.scrollHeight + }, [output, hrefForIframe]) + + return ( +
+ +
+
+ {output.join('\n')} +
+
+ {hrefForIframe &&