From 9ba161006977854b25e18ab052c98b3211b5f691 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 16 Feb 2026 12:05:23 -0500 Subject: [PATCH 01/26] Add mathlib-stable/build.sh so local dev works This is unnecessary for our production setup, because we use some bespoke nix stuff instead of the builtin build.sh, but it's still good to be able to test all the built-in configs in local dev --- Projects/MathlibDemo/lake-manifest.json | 22 ++--- Projects/MathlibDemo/lean-toolchain | 2 +- Projects/mathlib-stable/build.sh | 8 ++ Projects/mathlib-stable/lake-manifest.json | 96 +++++++++++++--------- Projects/mathlib-stable/lean-toolchain | 2 +- package-lock.json | 36 ++++---- 6 files changed, 95 insertions(+), 71 deletions(-) create mode 100755 Projects/mathlib-stable/build.sh diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json index c9a1cbb7..d47b8a91 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": "df5c1e1b57202011acb349cd2f22fcd5cec09bc8", "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/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/package-lock.json b/package-lock.json index 60981121..a607e5fe 100644 --- a/package-lock.json +++ b/package-lock.json @@ -99,6 +99,7 @@ "integrity": "sha512-lWBYIrF7qK5+GjY5Uy+/hEgp8OJWOD/rpy74GplYRhEauvbHDeFB8t5hPOZxCZ0Oxf4Cc36tK51/l3ymJysrKw==", "dev": true, "license": "MIT", + "peer": true, "dependencies": { "@ampproject/remapping": "^2.2.0", "@babel/code-frame": "^7.26.2", @@ -415,6 +416,7 @@ "resolved": "https://registry.npmjs.org/@codemirror/view/-/view-6.36.4.tgz", "integrity": "sha512-ZQ0V5ovw/miKEXTvjgzRyjnrk9TwriUB1k4R5p7uNnHR9Hus+D1SXHGdJshijEzPFjU25xea/7nhIeSqYFKdbA==", "license": "MIT", + "peer": true, "dependencies": { "@codemirror/state": "^6.5.0", "style-mod": "^4.1.0", @@ -628,7 +630,6 @@ "resolved": "https://registry.npmjs.org/@codingame/monaco-vscode-languages-service-override/-/monaco-vscode-languages-service-override-8.0.4.tgz", "integrity": "sha512-GXd2fKQa96tNv0gFB3nT/yWUc+4pZM/2L8KcfOOuNRWEOjm9TbOWmNZyWGi2Abf4vAdLNKVtJBX1+SoDkwoQdw==", "license": "MIT", - "peer": true, "dependencies": { "@codingame/monaco-vscode-files-service-override": "8.0.4", "vscode": "npm:@codingame/monaco-vscode-api@8.0.4" @@ -648,7 +649,6 @@ "resolved": "https://registry.npmjs.org/@codingame/monaco-vscode-localization-service-override/-/monaco-vscode-localization-service-override-8.0.4.tgz", "integrity": "sha512-z/MGZXSW69y3pIxbXobRfoGadN82BSSO7tu3jkhJx3c3CpvULaDl5HLUKoXDwtG14/nEA/VCzI/MOHp/bXBKDQ==", "license": "MIT", - "peer": true, "dependencies": { "vscode": "npm:@codingame/monaco-vscode-api@8.0.4" } @@ -658,7 +658,6 @@ "resolved": "https://registry.npmjs.org/@codingame/monaco-vscode-model-service-override/-/monaco-vscode-model-service-override-8.0.4.tgz", "integrity": "sha512-oynV9SnSE1MfqtVjqDWy/xcmekmAVNzyoqTh6oH3B+Oy/nhPqI6X9yIA0I47u0ncs/wjj3dDVnXOEv2IqJXxZg==", "license": "MIT", - "peer": true, "dependencies": { "vscode": "npm:@codingame/monaco-vscode-api@8.0.4" } @@ -832,6 +831,7 @@ "resolved": "https://registry.npmjs.org/@emotion/react/-/react-11.14.0.tgz", "integrity": "sha512-O000MLDBDdk/EohJPFUqvnp4qnHeYkVP5B0xEG0D/L7cOKP9kefu2DXn8dj74cQfsEzUqh+sr1RzFqiL1o+PpA==", "license": "MIT", + "peer": true, "dependencies": { "@babel/runtime": "^7.18.3", "@emotion/babel-plugin": "^11.13.5", @@ -875,6 +875,7 @@ "resolved": "https://registry.npmjs.org/@emotion/styled/-/styled-11.14.0.tgz", "integrity": "sha512-XxfOnXFffatap2IyCeJyNov3kiDQWoR08gPUQxvbL7fxKryGBKUZUkG6Hz48DZwVrJSVh9sJboyV1Ds4OW6SgA==", "license": "MIT", + "peer": true, "dependencies": { "@babel/runtime": "^7.18.3", "@emotion/babel-plugin": "^11.13.5", @@ -2933,6 +2934,7 @@ "resolved": "https://registry.npmjs.org/@types/react/-/react-19.0.10.tgz", "integrity": "sha512-JuRQ9KXLEjaUNjTWpzuR231Z2WpIwczOkBEIvbHNCzQefFIT0L8IqE6NV6ULLyC1SI/i234JnDoMkfg+RjQj2g==", "license": "MIT", + "peer": true, "dependencies": { "csstype": "^3.0.2" } @@ -3110,6 +3112,7 @@ "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.14.1.tgz", "integrity": "sha512-OvQ/2pUDKmgfCg++xsTX1wGxfTaszcHVcTctW4UJB4hibJx2HXxxO5UmVgyjMa+ZDsiaf5wWLXYpRWMmBI0QHg==", "license": "MIT", + "peer": true, "bin": { "acorn": "bin/acorn" }, @@ -3716,6 +3719,7 @@ } ], "license": "MIT", + "peer": true, "dependencies": { "caniuse-lite": "^1.0.30001688", "electron-to-chromium": "^1.5.73", @@ -4383,6 +4387,7 @@ "dev": true, "hasInstallScript": true, "license": "MIT", + "peer": true, "dependencies": { "@cypress/request": "^3.0.6", "@cypress/xvfb": "^1.2.4", @@ -4735,6 +4740,7 @@ "integrity": "sha512-rRqJg/6gd538VHvR3PSrdRBb/1Vy2YfzHqzvbhGIQpDRKIa4FgV/54b5Q1xYSxOOwKvjXweS26E0Q+nAMwp2pQ==", "dev": true, "license": "MIT", + "peer": true, "dependencies": { "ansi-colors": "^4.1.1", "strip-ansi": "^6.0.1" @@ -4894,6 +4900,7 @@ "resolved": "https://registry.npmjs.org/eslint/-/eslint-9.21.0.tgz", "integrity": "sha512-KjeihdFqTPhOMXTt7StsDxriV4n66ueuF/jfPNC3j/lduHwr/ijDwJMsF+wyMJethgiKi5wniIE243vi07d3pg==", "license": "MIT", + "peer": true, "dependencies": { "@eslint-community/eslint-utils": "^4.2.0", "@eslint-community/regexpp": "^4.12.1", @@ -7806,6 +7813,7 @@ "resolved": "https://registry.npmjs.org/react/-/react-19.0.0.tgz", "integrity": "sha512-V8AVnmPIICiWpGfm6GLzCR/W5FXLchHop40W4nXBmdlEceh16rCN8O8LNWm5bh5XUX91fh7KpA+W0TgMKmgTpQ==", "license": "MIT", + "peer": true, "engines": { "node": ">=0.10.0" } @@ -7815,6 +7823,7 @@ "resolved": "https://registry.npmjs.org/react-dom/-/react-dom-19.0.0.tgz", "integrity": "sha512-4GV5sHFG0e/0AD4X+ySy6UJd3jVl1iNsNHdpad0qhABJ11twS3TTBnseqsKurKcsNqCEFeGL3uLpVChpIO3QfQ==", "license": "MIT", + "peer": true, "dependencies": { "scheduler": "^0.25.0" }, @@ -7992,6 +8001,7 @@ "integrity": "sha512-nF5XYqWWp9hx/LrpC8sZvvvmq0TeTjQgaZHYmAgwysT9nh8sWnZhBnM8ZyVbbJFIQBLwHDNoMqsBZBbUo4U8sQ==", "dev": true, "license": "MIT", + "peer": true, "dependencies": { "@types/estree": "1.0.6" }, @@ -8720,7 +8730,8 @@ "version": "2.8.1", "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.8.1.tgz", "integrity": "sha512-oJFu94HQb+KVduSUQL7wnpmqnfmLsOA/nAh6b6EH0wCEoK0/mPeXU6c3wKDV83MkOuHPRHtSXKKU99IBazS/2w==", - "license": "0BSD" + "license": "0BSD", + "peer": true }, "node_modules/tty-browserify": { "version": "0.0.1", @@ -8793,6 +8804,7 @@ "integrity": "sha512-aJn6wq13/afZp/jT9QZmwEjDqqvSGp1VT5GVg+f/t6/oVyrgXM6BY1h9BRh/O5p3PlUPAe+WuiEZOmb/49RqoQ==", "dev": true, "license": "Apache-2.0", + "peer": true, "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" @@ -8974,6 +8986,7 @@ "integrity": "sha512-7dPxoo+WsT/64rDcwoOjk76XHj+TqNTIvHKcuMQ1k4/SeHDaQt5GFAeLYzrimZrMpn/O6DtdI03WUjdxuPM0oQ==", "dev": true, "license": "MIT", + "peer": true, "dependencies": { "esbuild": "^0.25.0", "postcss": "^8.5.3", @@ -9381,21 +9394,6 @@ "dev": true, "license": "ISC" }, - "node_modules/yaml": { - "version": "2.7.0", - "resolved": "https://registry.npmjs.org/yaml/-/yaml-2.7.0.tgz", - "integrity": "sha512-+hSoy/QHluxmC9kCIJyL/uyFmLmc+e5CFR5Wa+bpIhIj85LVb9ZH2nVnqrHoSvKogwODv0ClqZkmiSSaIH5LTA==", - "dev": true, - "license": "ISC", - "optional": true, - "peer": true, - "bin": { - "yaml": "bin.mjs" - }, - "engines": { - "node": ">= 14" - } - }, "node_modules/yargs": { "version": "17.7.2", "resolved": "https://registry.npmjs.org/yargs/-/yargs-17.7.2.tgz", From f2c47674d8512a5fa28a9ccd02869bf5583d367d Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 16 Feb 2026 12:50:01 -0500 Subject: [PATCH 02/26] move the server to lsp-server suggestively introduces the idea of additional servers --- {server => Projects}/build.sh | 0 doc/Development.md | 2 +- {server => lsp-server}/bubblewrap.sh | 0 {server => lsp-server}/index.mjs | 0 package-lock.json | 2 +- package.json | 20 ++++++++++---------- 6 files changed, 12 insertions(+), 12 deletions(-) rename {server => Projects}/build.sh (100%) rename {server => lsp-server}/bubblewrap.sh (100%) rename {server => lsp-server}/index.mjs (100%) 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/doc/Development.md b/doc/Development.md index 3e8582e1..f04a35ff 100644 --- a/doc/Development.md +++ b/doc/Development.md @@ -9,7 +9,7 @@ Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repository, run: 1. `npm install`, to install dependencies -2. `npm run build:server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project) +2. `npm run build:projects`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project) 3. `npm start`, to start the server. The project can be accessed via http://localhost:3000. (Internally, websocket requests to `ws://localhost:3000/`websockets will be forwarded to a Lean server running on port 8080.) diff --git a/server/bubblewrap.sh b/lsp-server/bubblewrap.sh similarity index 100% rename from server/bubblewrap.sh rename to lsp-server/bubblewrap.sh diff --git a/server/index.mjs b/lsp-server/index.mjs similarity index 100% rename from server/index.mjs rename to lsp-server/index.mjs diff --git a/package-lock.json b/package-lock.json index a607e5fe..8e21368b 100644 --- a/package-lock.json +++ b/package-lock.json @@ -33,7 +33,7 @@ "ws": "^8.18.1" }, "bin": { - "server": "server/index.mjs" + "server": "lsp-server/index.mjs" }, "devDependencies": { "@codingame/esbuild-import-meta-url-plugin": "^1.0.3", diff --git a/package.json b/package.json index d5687961..d76a02f9 100644 --- a/package.json +++ b/package.json @@ -4,29 +4,29 @@ "version": "0.0.0", "type": "module", "bin": { - "server": "server/index.mjs" + "server": "lsp-server/index.mjs" }, "files": [ "client/dist", - "server" + "lsp-server" ], "scripts": { - "start": "concurrently -n server,client -c blue,green \"npm run start:server\" \"npm run start:client\"", - "start:server": "cd server && NODE_ENV=development nodemon ./index.mjs", + "start": "concurrently -n lsp-server,client -c blue,green \"npm run start:lsp-server\" \"npm run start:client\"", + "start:lsp-server": "cd lsp-server && NODE_ENV=development nodemon ./index.mjs", "start:client": "NODE_ENV=development vite --host", - "build": "npm run build:server && npm run build:client", - "build:server": "server/build.sh", + "build": "npm run build:projects && npm run build:client", + "build:projects": "Projects/build.sh", "build:client": "tsc -b && NODE_ENV=production vite build", - "production": "NODE_ENV=production node server/index.mjs", + "production": "NODE_ENV=production node lsp-server/index.mjs", "dev": "vite", "lint": "eslint . --ext ts,tsx --report-unused-disable-directives --max-warnings 0", "preview": "vite preview", "test:dev:bare": "wait-on \"http://localhost:8080\" \"http://localhost:3000\" && cypress run", - "test:dev": "concurrently -k -s first -n server,client,cypress -c blue,green,cyan \"npm run start:server\" \"npm run start:client\" \"npm run test:dev:bare\"", + "test:dev": "concurrently -k -s first -n lsp-server,client,cypress -c blue,green,cyan \"npm run start:lsp-server\" \"npm run start:client\" \"npm run test:dev:bare\"", "test:prod:bare": "wait-on \"http://localhost:3000\" && cypress run", - "test:prod": "concurrently -k -s first -n server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:bare\"", + "test:prod": "concurrently -k -s first -n lsp-server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:bare\"", "test:prod:windows:bare": "wait-on \"http://localhost:3000\" && CYPRESS_USER_AGENT_OS=\"Windows NT 10.0; Win64; x64\" cypress run --browser chromium", - "test:prod:windows": "concurrently -k -s first -n server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:windows:bare\"", + "test:prod:windows": "concurrently -k -s first -n lsp-server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:windows:bare\"", "test": "npm run test:dev" }, "dependencies": { From 490b6177867b320679004aea9bf30d97657de8ad Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 16 Feb 2026 15:28:17 -0500 Subject: [PATCH 03/26] create a verso nightly project that supports verso document creation --- .gitignore | 2 + Projects/verso-nightly/Main.lean | 10 + Projects/verso-nightly/TheLeanFile.lean | 5 + Projects/verso-nightly/build.sh | 8 + Projects/verso-nightly/lake-manifest.json | 45 ++ Projects/verso-nightly/lakefile.toml | 15 + Projects/verso-nightly/lean-toolchain | 1 + package-lock.json | 769 ++++++++++++++++++++++ package.json | 16 +- verso-server/app.ts | 65 ++ verso-server/exec.ts | 26 + verso-server/server.ts | 9 + verso-server/tsconfig.json | 23 + 13 files changed, 988 insertions(+), 6 deletions(-) create mode 100644 Projects/verso-nightly/Main.lean create mode 100644 Projects/verso-nightly/TheLeanFile.lean create mode 100755 Projects/verso-nightly/build.sh create mode 100644 Projects/verso-nightly/lake-manifest.json create mode 100644 Projects/verso-nightly/lakefile.toml create mode 100644 Projects/verso-nightly/lean-toolchain create mode 100644 verso-server/app.ts create mode 100644 verso-server/exec.ts create mode 100644 verso-server/server.ts create mode 100644 verso-server/tsconfig.json diff --git a/.gitignore b/.gitignore index 475c7bcb..2591cfb1 100644 --- a/.gitignore +++ b/.gitignore @@ -17,6 +17,8 @@ cypress/videos **/.lake +_out + # Editor directories and files .vscode/* !.vscode/extensions.json diff --git a/Projects/verso-nightly/Main.lean b/Projects/verso-nightly/Main.lean new file mode 100644 index 00000000..f6a82406 --- /dev/null +++ b/Projects/verso-nightly/Main.lean @@ -0,0 +1,10 @@ +import VersoManual +import TheLeanFile + +def config : Verso.Genre.Manual.RenderConfig where + emitTeX := false + emitHtmlSingle := .immediately + emitHtmlMulti := .no + htmlDepth := 2 + +def main := Verso.Genre.Manual.manualMain (%doc TheLeanFile) (config := config) diff --git a/Projects/verso-nightly/TheLeanFile.lean b/Projects/verso-nightly/TheLeanFile.lean new file mode 100644 index 00000000..21f189ce --- /dev/null +++ b/Projects/verso-nightly/TheLeanFile.lean @@ -0,0 +1,5 @@ +import VersoManual +open Verso Doc +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean +#doc (Manual) "Mydoc" => Would you like a doc?I'll give you a doc if you'd like. \ No newline at end of file diff --git a/Projects/verso-nightly/build.sh b/Projects/verso-nightly/build.sh new file mode 100755 index 00000000..974d6225 --- /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 \ 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..58ced4b9 --- /dev/null +++ b/Projects/verso-nightly/lakefile.toml @@ -0,0 +1,15 @@ +name = "verso-nightly" +version = "0.1.0" +defaultTargets = ["TheLeanFile", "mkdoc"] + +[[require]] +name = "verso" +git = "https://github.com/leanprover/verso" +rev = "nightly-testing" + +[[lean_lib]] +name = "TheLeanFile" + +[[lean_exe]] +name = "mkdoc" +root = "Main" 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/package-lock.json b/package-lock.json index 8e21368b..c1c3e3f0 100644 --- a/package-lock.json +++ b/package-lock.json @@ -37,6 +37,7 @@ }, "devDependencies": { "@codingame/esbuild-import-meta-url-plugin": "^1.0.3", + "@types/express": "^5.0.6", "@types/node": "^22.13.9", "@types/react": "^19.0.10", "@types/react-dom": "^19.0.4", @@ -44,6 +45,8 @@ "cypress": "^13.17.0", "cypress-iframe": "^1.0.1", "cypress-real-events": "^1.14.0", + "ts-node": "^10.9.2", + "tsx": "^4.21.0", "typescript": "^5.8.2", "vite": "^6.2.0", "vite-plugin-node-polyfills": "0.23.0", @@ -722,6 +725,30 @@ "node": ">=0.1.90" } }, + "node_modules/@cspotcode/source-map-support": { + "version": "0.8.1", + "resolved": "https://registry.npmjs.org/@cspotcode/source-map-support/-/source-map-support-0.8.1.tgz", + "integrity": "sha512-IchNf6dN4tHoMFIn/7OE8LWZ19Y6q/67Bmf6vnGREv8RSbBVb9LPJxEcnwrcwX6ixSvaiGoomAUvu4YSxXrVgw==", + "dev": true, + "license": "MIT", + "dependencies": { + "@jridgewell/trace-mapping": "0.3.9" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/@cspotcode/source-map-support/node_modules/@jridgewell/trace-mapping": { + "version": "0.3.9", + "resolved": "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.9.tgz", + "integrity": "sha512-3Belt6tdc8bPgAtbcmdtNJlirVoTmEb5e2gC94PnkwEW9jI6CAHUeoG85tjWP5WquqfavoMtMwiG4P926ZKKuQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "@jridgewell/resolve-uri": "^3.0.3", + "@jridgewell/sourcemap-codec": "^1.4.10" + } + }, "node_modules/@cypress/request": { "version": "3.0.8", "resolved": "https://registry.npmjs.org/@cypress/request/-/request-3.0.8.tgz", @@ -1278,6 +1305,23 @@ "node": ">=18" } }, + "node_modules/@esbuild/openharmony-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/openharmony-arm64/-/openharmony-arm64-0.27.3.tgz", + "integrity": "sha512-NinAEgr/etERPTsZJ7aEZQvvg/A6IsZG/LgZy+81wON2huV7SrK3e63dU0XhyZP4RKGyTm7aOgmQk0bGp0fy2g==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openharmony" + ], + "engines": { + "node": ">=18" + } + }, "node_modules/@esbuild/sunos-x64": { "version": "0.25.0", "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.25.0.tgz", @@ -2867,6 +2911,55 @@ "@swc/counter": "^0.1.3" } }, + "node_modules/@tsconfig/node10": { + "version": "1.0.12", + "resolved": "https://registry.npmjs.org/@tsconfig/node10/-/node10-1.0.12.tgz", + "integrity": "sha512-UCYBaeFvM11aU2y3YPZ//O5Rhj+xKyzy7mvcIoAjASbigy8mHMryP5cK7dgjlz2hWxh1g5pLw084E0a/wlUSFQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/@tsconfig/node12": { + "version": "1.0.11", + "resolved": "https://registry.npmjs.org/@tsconfig/node12/-/node12-1.0.11.tgz", + "integrity": "sha512-cqefuRsh12pWyGsIoBKJA9luFu3mRxCA+ORZvA4ktLSzIuCUtWVxGIuXigEwO5/ywWFMZ2QEGKWvkZG1zDMTag==", + "dev": true, + "license": "MIT" + }, + "node_modules/@tsconfig/node14": { + "version": "1.0.3", + "resolved": "https://registry.npmjs.org/@tsconfig/node14/-/node14-1.0.3.tgz", + "integrity": "sha512-ysT8mhdixWK6Hw3i1V2AeRqZ5WfXg1G43mqoYlM2nc6388Fq5jcXyr5mRsqViLx/GJYdoL0bfXD8nmF+Zn/Iow==", + "dev": true, + "license": "MIT" + }, + "node_modules/@tsconfig/node16": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/@tsconfig/node16/-/node16-1.0.4.tgz", + "integrity": "sha512-vxhUy4J8lyeyinH7Azl1pdd43GJhZH/tP2weN8TntQblOY+A0XbT8DJk1/oCPuOOyg/Ja757rG0CgHcWC8OfMA==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/body-parser": { + "version": "1.19.6", + "resolved": "https://registry.npmjs.org/@types/body-parser/-/body-parser-1.19.6.tgz", + "integrity": "sha512-HLFeCYgz89uk22N5Qg3dvGvsv46B8GLvKKo1zKG4NybA8U2DiEO3w9lqGg29t/tfLRJpJ6iQxnVw4OnB7MoM9g==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/connect": "*", + "@types/node": "*" + } + }, + "node_modules/@types/connect": { + "version": "3.4.38", + "resolved": "https://registry.npmjs.org/@types/connect/-/connect-3.4.38.tgz", + "integrity": "sha512-K6uROf1LD88uDQqJCktA4yzL1YYAK6NgfsI0v/mTgyPKWsX1CnJ0XPSDhViejru1GcRkLWb8RlzFYJRqGUbaug==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/node": "*" + } + }, "node_modules/@types/cypress": { "version": "1.1.6", "resolved": "https://registry.npmjs.org/@types/cypress/-/cypress-1.1.6.tgz", @@ -2885,12 +2978,44 @@ "integrity": "sha512-AYnb1nQyY49te+VRAVgmzfcgjYS91mY5P0TKUDCLEM+gNnA+3T6rWITXRLYCpahpqSQbN5cE+gHpnPyXjHWxcw==", "license": "MIT" }, + "node_modules/@types/express": { + "version": "5.0.6", + "resolved": "https://registry.npmjs.org/@types/express/-/express-5.0.6.tgz", + "integrity": "sha512-sKYVuV7Sv9fbPIt/442koC7+IIwK5olP1KWeD88e/idgoJqDm3JV/YUiPwkoKK92ylff2MGxSz1CSjsXelx0YA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/body-parser": "*", + "@types/express-serve-static-core": "^5.0.0", + "@types/serve-static": "^2" + } + }, + "node_modules/@types/express-serve-static-core": { + "version": "5.1.1", + "resolved": "https://registry.npmjs.org/@types/express-serve-static-core/-/express-serve-static-core-5.1.1.tgz", + "integrity": "sha512-v4zIMr/cX7/d2BpAEX3KNKL/JrT1s43s96lLvvdTmza1oEvDudCqK9aF/djc/SWgy8Yh0h30TZx5VpzqFCxk5A==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/node": "*", + "@types/qs": "*", + "@types/range-parser": "*", + "@types/send": "*" + } + }, "node_modules/@types/file-saver": { "version": "2.0.7", "resolved": "https://registry.npmjs.org/@types/file-saver/-/file-saver-2.0.7.tgz", "integrity": "sha512-dNKVfHd/jk0SkR/exKGj2ggkB45MAkzvWCaqLUUgkyjITkGNzH8H+yUwr+BLJUBjZOe9w8X3wgmXhZDRg1ED6A==", "license": "MIT" }, + "node_modules/@types/http-errors": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/@types/http-errors/-/http-errors-2.0.5.tgz", + "integrity": "sha512-r8Tayk8HJnX0FztbZN7oVqGccWgw98T/0neJphO91KkmOzug1KkofZURD4UaD5uH8AqcFLfdPErnBod0u71/qg==", + "dev": true, + "license": "MIT" + }, "node_modules/@types/json-schema": { "version": "7.0.15", "resolved": "https://registry.npmjs.org/@types/json-schema/-/json-schema-7.0.15.tgz", @@ -2913,6 +3038,7 @@ "integrity": "sha512-acBjXdRJ3A6Pb3tqnw9HZmyR3Fiol3aGxRCK1x3d+6CDAMjl7I649wpSd+yNURCjbOUGu9tqtLKnTGxmK6CyGw==", "dev": true, "license": "MIT", + "peer": true, "dependencies": { "undici-types": "~6.20.0" } @@ -2929,6 +3055,20 @@ "integrity": "sha512-gNMvNH49DJ7OJYv+KAKn0Xp45p8PLl6zo2YnvDIbTd4J6MER2BmWN49TG7n9LvkyihINxeKW8+3bfS2yDC9dzQ==", "license": "MIT" }, + "node_modules/@types/qs": { + "version": "6.14.0", + "resolved": "https://registry.npmjs.org/@types/qs/-/qs-6.14.0.tgz", + "integrity": "sha512-eOunJqu0K1923aExK6y8p6fsihYEn/BYuQ4g0CxAAgFc4b/ZLN4CrsRZ55srTdqoiLzU2B2evC+apEIxprEzkQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/range-parser": { + "version": "1.2.7", + "resolved": "https://registry.npmjs.org/@types/range-parser/-/range-parser-1.2.7.tgz", + "integrity": "sha512-hKormJbkJqzQGhziax5PItDUTMAM9uE2XXQmM37dyd4hVM+5aVl7oVxMVUiVQn2oCQFN/LKCZdvSM0pFRqbSmQ==", + "dev": true, + "license": "MIT" + }, "node_modules/@types/react": { "version": "19.0.10", "resolved": "https://registry.npmjs.org/@types/react/-/react-19.0.10.tgz", @@ -2958,6 +3098,27 @@ "@types/react": "*" } }, + "node_modules/@types/send": { + "version": "1.2.1", + "resolved": "https://registry.npmjs.org/@types/send/-/send-1.2.1.tgz", + "integrity": "sha512-arsCikDvlU99zl1g69TcAB3mzZPpxgw0UQnaHeC1Nwb015xp8bknZv5rIfri9xTOcMuaVgvabfIRA7PSZVuZIQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/node": "*" + } + }, + "node_modules/@types/serve-static": { + "version": "2.2.0", + "resolved": "https://registry.npmjs.org/@types/serve-static/-/serve-static-2.2.0.tgz", + "integrity": "sha512-8mam4H1NHLtu7nmtalF7eyBH14QyOASmcxHhSfEoRyr0nP/YdoesEtU+uSRvMe96TW/HPTtkoKqQLl53N7UXMQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/http-errors": "*", + "@types/node": "*" + } + }, "node_modules/@types/sinonjs__fake-timers": { "version": "8.1.1", "resolved": "https://registry.npmjs.org/@types/sinonjs__fake-timers/-/sinonjs__fake-timers-8.1.1.tgz", @@ -3129,6 +3290,19 @@ "acorn": "^6.0.0 || ^7.0.0 || ^8.0.0" } }, + "node_modules/acorn-walk": { + "version": "8.3.4", + "resolved": "https://registry.npmjs.org/acorn-walk/-/acorn-walk-8.3.4.tgz", + "integrity": "sha512-ueEepnujpqee2o5aIYnvHU6C0A42MNdsIDeqy5BydrkuC5R1ZuUFnm27EeFJGoEHJQgn3uleRvmTXaJgfXbt4g==", + "dev": true, + "license": "MIT", + "dependencies": { + "acorn": "^8.11.0" + }, + "engines": { + "node": ">=0.4.0" + } + }, "node_modules/aggregate-error": { "version": "3.1.0", "resolved": "https://registry.npmjs.org/aggregate-error/-/aggregate-error-3.1.0.tgz", @@ -3243,6 +3417,13 @@ ], "license": "MIT" }, + "node_modules/arg": { + "version": "4.1.3", + "resolved": "https://registry.npmjs.org/arg/-/arg-4.1.3.tgz", + "integrity": "sha512-58S9QDqG0Xx27YwPSt9fJxivjYl432YCwfDMfZ+71RAqUrZef7LrKQZ3LHLOwCS4FLNBplP533Zx895SeOCHvA==", + "dev": true, + "license": "MIT" + }, "node_modules/argparse": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/argparse/-/argparse-2.0.1.tgz", @@ -4595,6 +4776,16 @@ "npm": "1.2.8000 || >= 1.4.16" } }, + "node_modules/diff": { + "version": "4.0.4", + "resolved": "https://registry.npmjs.org/diff/-/diff-4.0.4.tgz", + "integrity": "sha512-X07nttJQkwkfKfvTPG/KSnE2OMdcUCao6+eXF3wmnIQRn2aPAHH3VxDbDOdegkd6JbPsXqShpvEOHfAT+nCNwQ==", + "dev": true, + "license": "BSD-3-Clause", + "engines": { + "node": ">=0.3.1" + } + }, "node_modules/diffie-hellman": { "version": "5.0.3", "resolved": "https://registry.npmjs.org/diffie-hellman/-/diffie-hellman-5.0.3.tgz", @@ -5627,6 +5818,19 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/get-tsconfig": { + "version": "4.13.6", + "resolved": "https://registry.npmjs.org/get-tsconfig/-/get-tsconfig-4.13.6.tgz", + "integrity": "sha512-shZT/QMiSHc/YBLxxOkMtgSid5HFoauqCE3/exfsEcwg1WkeqjG+V40yBbBrsD+jW2HDXcs28xOfcbm2jI8Ddw==", + "dev": true, + "license": "MIT", + "dependencies": { + "resolve-pkg-maps": "^1.0.0" + }, + "funding": { + "url": "https://github.com/privatenumber/get-tsconfig?sponsor=1" + } + }, "node_modules/getos": { "version": "3.2.1", "resolved": "https://registry.npmjs.org/getos/-/getos-3.2.1.tgz", @@ -6693,6 +6897,13 @@ "@jridgewell/sourcemap-codec": "^1.5.0" } }, + "node_modules/make-error": { + "version": "1.3.6", + "resolved": "https://registry.npmjs.org/make-error/-/make-error-1.3.6.tgz", + "integrity": "sha512-s8UhlNe7vPKomQhC1qFelMokr/Sc3AgNbso3n74mVPA5LTZwkB9NlXf4XPamLxJE8h0gh73rM94xvwRT2CVInw==", + "dev": true, + "license": "ISC" + }, "node_modules/math-intrinsics": { "version": "1.1.0", "resolved": "https://registry.npmjs.org/math-intrinsics/-/math-intrinsics-1.1.0.tgz", @@ -7952,6 +8163,16 @@ "node": ">=4" } }, + "node_modules/resolve-pkg-maps": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/resolve-pkg-maps/-/resolve-pkg-maps-1.0.0.tgz", + "integrity": "sha512-seS2Tj26TBVOC2NIc2rOe2y2ZO7efxITtLZcGSOnHHNOQ7CkiUBfw0Iw2ck6xkIhPwLhKNLS8BO+hEpngQlqzw==", + "dev": true, + "license": "MIT", + "funding": { + "url": "https://github.com/privatenumber/resolve-pkg-maps?sponsor=1" + } + }, "node_modules/restore-cursor": { "version": "3.1.0", "resolved": "https://registry.npmjs.org/restore-cursor/-/restore-cursor-3.1.0.tgz", @@ -8726,6 +8947,50 @@ "tree-kill": "cli.js" } }, + "node_modules/ts-node": { + "version": "10.9.2", + "resolved": "https://registry.npmjs.org/ts-node/-/ts-node-10.9.2.tgz", + "integrity": "sha512-f0FFpIdcHgn8zcPSbf1dRevwt047YMnaiJM3u2w2RewrB+fob/zePZcrOyQoLMMO7aBIddLcQIEK5dYjkLnGrQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "@cspotcode/source-map-support": "^0.8.0", + "@tsconfig/node10": "^1.0.7", + "@tsconfig/node12": "^1.0.7", + "@tsconfig/node14": "^1.0.0", + "@tsconfig/node16": "^1.0.2", + "acorn": "^8.4.1", + "acorn-walk": "^8.1.1", + "arg": "^4.1.0", + "create-require": "^1.1.0", + "diff": "^4.0.1", + "make-error": "^1.1.1", + "v8-compile-cache-lib": "^3.0.1", + "yn": "3.1.1" + }, + "bin": { + "ts-node": "dist/bin.js", + "ts-node-cwd": "dist/bin-cwd.js", + "ts-node-esm": "dist/bin-esm.js", + "ts-node-script": "dist/bin-script.js", + "ts-node-transpile-only": "dist/bin-transpile.js", + "ts-script": "dist/bin-script-deprecated.js" + }, + "peerDependencies": { + "@swc/core": ">=1.2.50", + "@swc/wasm": ">=1.2.50", + "@types/node": "*", + "typescript": ">=2.7" + }, + "peerDependenciesMeta": { + "@swc/core": { + "optional": true + }, + "@swc/wasm": { + "optional": true + } + } + }, "node_modules/tslib": { "version": "2.8.1", "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.8.1.tgz", @@ -8733,6 +8998,493 @@ "license": "0BSD", "peer": true }, + "node_modules/tsx": { + "version": "4.21.0", + "resolved": "https://registry.npmjs.org/tsx/-/tsx-4.21.0.tgz", + "integrity": "sha512-5C1sg4USs1lfG0GFb2RLXsdpXqBSEhAaA/0kPL01wxzpMqLILNxIxIOKiILz+cdg/pLnOUxFYOR5yhHU666wbw==", + "dev": true, + "license": "MIT", + "dependencies": { + "esbuild": "~0.27.0", + "get-tsconfig": "^4.7.5" + }, + "bin": { + "tsx": "dist/cli.mjs" + }, + "engines": { + "node": ">=18.0.0" + }, + "optionalDependencies": { + "fsevents": "~2.3.3" + } + }, + "node_modules/tsx/node_modules/@esbuild/aix-ppc64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.27.3.tgz", + "integrity": "sha512-9fJMTNFTWZMh5qwrBItuziu834eOCUcEqymSH7pY+zoMVEZg3gcPuBNxH1EvfVYe9h0x/Ptw8KBzv7qxb7l8dg==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "aix" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/android-arm": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.27.3.tgz", + "integrity": "sha512-i5D1hPY7GIQmXlXhs2w8AWHhenb00+GxjxRncS2ZM7YNVGNfaMxgzSGuO8o8SJzRc/oZwU2bcScvVERk03QhzA==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/android-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.27.3.tgz", + "integrity": "sha512-YdghPYUmj/FX2SYKJ0OZxf+iaKgMsKHVPF1MAq/P8WirnSpCStzKJFjOjzsW0QQ7oIAiccHdcqjbHmJxRb/dmg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/android-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.27.3.tgz", + "integrity": "sha512-IN/0BNTkHtk8lkOM8JWAYFg4ORxBkZQf9zXiEOfERX/CzxW3Vg1ewAhU7QSWQpVIzTW+b8Xy+lGzdYXV6UZObQ==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/darwin-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.27.3.tgz", + "integrity": "sha512-Re491k7ByTVRy0t3EKWajdLIr0gz2kKKfzafkth4Q8A5n1xTHrkqZgLLjFEHVD+AXdUGgQMq+Godfq45mGpCKg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/darwin-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.27.3.tgz", + "integrity": "sha512-vHk/hA7/1AckjGzRqi6wbo+jaShzRowYip6rt6q7VYEDX4LEy1pZfDpdxCBnGtl+A5zq8iXDcyuxwtv3hNtHFg==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/freebsd-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.27.3.tgz", + "integrity": "sha512-ipTYM2fjt3kQAYOvo6vcxJx3nBYAzPjgTCk7QEgZG8AUO3ydUhvelmhrbOheMnGOlaSFUoHXB6un+A7q4ygY9w==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/freebsd-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.27.3.tgz", + "integrity": "sha512-dDk0X87T7mI6U3K9VjWtHOXqwAMJBNN2r7bejDsc+j03SEjtD9HrOl8gVFByeM0aJksoUuUVU9TBaZa2rgj0oA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-arm": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.27.3.tgz", + "integrity": "sha512-s6nPv2QkSupJwLYyfS+gwdirm0ukyTFNl3KTgZEAiJDd+iHZcbTPPcWCcRYH+WlNbwChgH2QkE9NSlNrMT8Gfw==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.27.3.tgz", + "integrity": "sha512-sZOuFz/xWnZ4KH3YfFrKCf1WyPZHakVzTiqji3WDc0BCl2kBwiJLCXpzLzUBLgmp4veFZdvN5ChW4Eq/8Fc2Fg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-ia32": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.27.3.tgz", + "integrity": "sha512-yGlQYjdxtLdh0a3jHjuwOrxQjOZYD/C9PfdbgJJF3TIZWnm/tMd/RcNiLngiu4iwcBAOezdnSLAwQDPqTmtTYg==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-loong64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.27.3.tgz", + "integrity": "sha512-WO60Sn8ly3gtzhyjATDgieJNet/KqsDlX5nRC5Y3oTFcS1l0KWba+SEa9Ja1GfDqSF1z6hif/SkpQJbL63cgOA==", + "cpu": [ + "loong64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-mips64el": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.27.3.tgz", + "integrity": "sha512-APsymYA6sGcZ4pD6k+UxbDjOFSvPWyZhjaiPyl/f79xKxwTnrn5QUnXR5prvetuaSMsb4jgeHewIDCIWljrSxw==", + "cpu": [ + "mips64el" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-ppc64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.27.3.tgz", + "integrity": "sha512-eizBnTeBefojtDb9nSh4vvVQ3V9Qf9Df01PfawPcRzJH4gFSgrObw+LveUyDoKU3kxi5+9RJTCWlj4FjYXVPEA==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-riscv64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.27.3.tgz", + "integrity": "sha512-3Emwh0r5wmfm3ssTWRQSyVhbOHvqegUDRd0WhmXKX2mkHJe1SFCMJhagUleMq+Uci34wLSipf8Lagt4LlpRFWQ==", + "cpu": [ + "riscv64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-s390x": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.27.3.tgz", + "integrity": "sha512-pBHUx9LzXWBc7MFIEEL0yD/ZVtNgLytvx60gES28GcWMqil8ElCYR4kvbV2BDqsHOvVDRrOxGySBM9Fcv744hw==", + "cpu": [ + "s390x" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/linux-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.27.3.tgz", + "integrity": "sha512-Czi8yzXUWIQYAtL/2y6vogER8pvcsOsk5cpwL4Gk5nJqH5UZiVByIY8Eorm5R13gq+DQKYg0+JyQoytLQas4dA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/netbsd-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-arm64/-/netbsd-arm64-0.27.3.tgz", + "integrity": "sha512-sDpk0RgmTCR/5HguIZa9n9u+HVKf40fbEUt+iTzSnCaGvY9kFP0YKBWZtJaraonFnqef5SlJ8/TiPAxzyS+UoA==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/netbsd-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.27.3.tgz", + "integrity": "sha512-P14lFKJl/DdaE00LItAukUdZO5iqNH7+PjoBm+fLQjtxfcfFE20Xf5CrLsmZdq5LFFZzb5JMZ9grUwvtVYzjiA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/openbsd-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-arm64/-/openbsd-arm64-0.27.3.tgz", + "integrity": "sha512-AIcMP77AvirGbRl/UZFTq5hjXK+2wC7qFRGoHSDrZ5v5b8DK/GYpXW3CPRL53NkvDqb9D+alBiC/dV0Fb7eJcw==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/openbsd-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.27.3.tgz", + "integrity": "sha512-DnW2sRrBzA+YnE70LKqnM3P+z8vehfJWHXECbwBmH/CU51z6FiqTQTHFenPlHmo3a8UgpLyH3PT+87OViOh1AQ==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/sunos-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.27.3.tgz", + "integrity": "sha512-PanZ+nEz+eWoBJ8/f8HKxTTD172SKwdXebZ0ndd953gt1HRBbhMsaNqjTyYLGLPdoWHy4zLU7bDVJztF5f3BHA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "sunos" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-arm64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.27.3.tgz", + "integrity": "sha512-B2t59lWWYrbRDw/tjiWOuzSsFh1Y/E95ofKz7rIVYSQkUYBjfSgf6oeYPNWHToFRr2zx52JKApIcAS/D5TUBnA==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-ia32": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.27.3.tgz", + "integrity": "sha512-QLKSFeXNS8+tHW7tZpMtjlNb7HKau0QDpwm49u0vUp9y1WOF+PEzkU84y9GqYaAVW8aH8f3GcBck26jh54cX4Q==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/@esbuild/win32-x64": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.27.3.tgz", + "integrity": "sha512-4uJGhsxuptu3OcpVAzli+/gWusVGwZZHTlS63hh++ehExkVT8SgiEf7/uC/PclrPPkLhZqGgCTjd0VWLo6xMqA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/tsx/node_modules/esbuild": { + "version": "0.27.3", + "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.27.3.tgz", + "integrity": "sha512-8VwMnyGCONIs6cWue2IdpHxHnAjzxnw2Zr7MkVxB2vjmQ2ivqGFb4LEG3SMnv0Gb2F/G/2yA8zUaiL1gywDCCg==", + "dev": true, + "hasInstallScript": true, + "license": "MIT", + "bin": { + "esbuild": "bin/esbuild" + }, + "engines": { + "node": ">=18" + }, + "optionalDependencies": { + "@esbuild/aix-ppc64": "0.27.3", + "@esbuild/android-arm": "0.27.3", + "@esbuild/android-arm64": "0.27.3", + "@esbuild/android-x64": "0.27.3", + "@esbuild/darwin-arm64": "0.27.3", + "@esbuild/darwin-x64": "0.27.3", + "@esbuild/freebsd-arm64": "0.27.3", + "@esbuild/freebsd-x64": "0.27.3", + "@esbuild/linux-arm": "0.27.3", + "@esbuild/linux-arm64": "0.27.3", + "@esbuild/linux-ia32": "0.27.3", + "@esbuild/linux-loong64": "0.27.3", + "@esbuild/linux-mips64el": "0.27.3", + "@esbuild/linux-ppc64": "0.27.3", + "@esbuild/linux-riscv64": "0.27.3", + "@esbuild/linux-s390x": "0.27.3", + "@esbuild/linux-x64": "0.27.3", + "@esbuild/netbsd-arm64": "0.27.3", + "@esbuild/netbsd-x64": "0.27.3", + "@esbuild/openbsd-arm64": "0.27.3", + "@esbuild/openbsd-x64": "0.27.3", + "@esbuild/openharmony-arm64": "0.27.3", + "@esbuild/sunos-x64": "0.27.3", + "@esbuild/win32-arm64": "0.27.3", + "@esbuild/win32-ia32": "0.27.3", + "@esbuild/win32-x64": "0.27.3" + } + }, "node_modules/tty-browserify": { "version": "0.0.1", "resolved": "https://registry.npmjs.org/tty-browserify/-/tty-browserify-0.0.1.tgz", @@ -8956,6 +9708,13 @@ "uuid": "dist/bin/uuid" } }, + "node_modules/v8-compile-cache-lib": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/v8-compile-cache-lib/-/v8-compile-cache-lib-3.0.1.tgz", + "integrity": "sha512-wa7YjyUGfNZngI/vtK0UHAN+lgDCxBPCylVXGp0zu59Fz5aiGtNXaq3DhIov063MorB+VfufLh3JlF2KdTK3xg==", + "dev": true, + "license": "MIT" + }, "node_modules/vary": { "version": "1.1.2", "resolved": "https://registry.npmjs.org/vary/-/vary-1.1.2.tgz", @@ -9432,6 +10191,16 @@ "fd-slicer": "~1.1.0" } }, + "node_modules/yn": { + "version": "3.1.1", + "resolved": "https://registry.npmjs.org/yn/-/yn-3.1.1.tgz", + "integrity": "sha512-Ux4ygGWsu2c7isFWe8Yu1YluJmqVhxqK2cLXNQA5AcC3QfbGNpM7fu0Y8b/z16pXLnFxZYvWhd3fhBY9DLmC6Q==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=6" + } + }, "node_modules/yocto-queue": { "version": "0.1.0", "resolved": "https://registry.npmjs.org/yocto-queue/-/yocto-queue-0.1.0.tgz", diff --git a/package.json b/package.json index d76a02f9..8af5a735 100644 --- a/package.json +++ b/package.json @@ -11,9 +11,10 @@ "lsp-server" ], "scripts": { - "start": "concurrently -n lsp-server,client -c blue,green \"npm run start:lsp-server\" \"npm run start:client\"", + "start": "concurrently -n lsp-server,client,verso-server -c \"#619fff,#4db556,#d381e5\" \"npm run start:lsp-server\" \"npm run start:client\" \"npm run start:verso-server\"", "start:lsp-server": "cd lsp-server && NODE_ENV=development nodemon ./index.mjs", "start:client": "NODE_ENV=development vite --host", + "start:verso-server": "NODE_ENV=development nodemon ./verso-server/server.ts", "build": "npm run build:projects && npm run build:client", "build:projects": "Projects/build.sh", "build:client": "tsc -b && NODE_ENV=production vite build", @@ -22,11 +23,11 @@ "lint": "eslint . --ext ts,tsx --report-unused-disable-directives --max-warnings 0", "preview": "vite preview", "test:dev:bare": "wait-on \"http://localhost:8080\" \"http://localhost:3000\" && cypress run", - "test:dev": "concurrently -k -s first -n lsp-server,client,cypress -c blue,green,cyan \"npm run start:lsp-server\" \"npm run start:client\" \"npm run test:dev:bare\"", + "test:dev": "concurrently -k -s first -n lsp-server,client,cypress -c \"#619fff,#4db556,#d381e5,#91ab07\" \"npm run start:lsp-server\" \"npm run start:client\" \"npm run test:dev:bare\"", "test:prod:bare": "wait-on \"http://localhost:3000\" && cypress run", - "test:prod": "concurrently -k -s first -n lsp-server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:bare\"", + "test:prod": "concurrently -k -s first -n lsp-server,cypress -c #619fff,#4db556,#d381e5 \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:bare\"", "test:prod:windows:bare": "wait-on \"http://localhost:3000\" && CYPRESS_USER_AGENT_OS=\"Windows NT 10.0; Win64; x64\" cypress run --browser chromium", - "test:prod:windows": "concurrently -k -s first -n lsp-server,cypress -c blue,cyan \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:windows:bare\"", + "test:prod:windows": "concurrently -k -s first -n lsp-server,cypress -c \"#619fff,#4db556,#d381e5\" \"npm run build && PORT=3000 npm run production\" \"npm run test:prod:windows:bare\"", "test": "npm run test:dev" }, "dependencies": { @@ -56,6 +57,7 @@ }, "devDependencies": { "@codingame/esbuild-import-meta-url-plugin": "^1.0.3", + "@types/express": "^5.0.6", "@types/node": "^22.13.9", "@types/react": "^19.0.10", "@types/react-dom": "^19.0.4", @@ -63,6 +65,8 @@ "cypress": "^13.17.0", "cypress-iframe": "^1.0.1", "cypress-real-events": "^1.14.0", + "ts-node": "^10.9.2", + "tsx": "^4.21.0", "typescript": "^5.8.2", "vite": "^6.2.0", "vite-plugin-node-polyfills": "0.23.0", @@ -70,7 +74,7 @@ "vite-plugin-svgr": "^4.3.0", "wait-on": "^8.0.2" }, - "engines" : { - "node" : ">=22.0.0" + "engines": { + "node": ">=22.0.0" } } diff --git a/verso-server/app.ts b/verso-server/app.ts new file mode 100644 index 00000000..6f483bce --- /dev/null +++ b/verso-server/app.ts @@ -0,0 +1,65 @@ +import express from "express"; +import { z } from "zod"; +import { mkdir, mkdtemp } from "node:fs/promises"; +import { join } from "node:path"; +import { tmpdir } from "node:os"; +import { randomUUID } from "node:crypto"; +import { compileVerso } from "./exec.ts"; + +export const app = express(); +app.use(express.json()); + +const OUTPUT_ROOT_DIR = await mkdtemp(join(tmpdir(), "verso-output-")); + +const zBuildRequest = z.object({ + projectId: z.string().regex(/^[A-Za-z0-9][A-Za-z0-9.-]*$/), + fileContents: z.string(), +}); +app.post("/verso/api/singlepage", async (req, res) => { + function send(obj: unknown) { + const txt = JSON.stringify(obj); + console.log("sending " + txt); + res.write("data: " + txt + "\n\n"); + } + + const body = zBuildRequest.safeParse(req.body); + if (!body.success) { + res.status(400).send({ error: "Poorly-formed request" }); + } else { + // Stream responses + res.setHeader("Cache-Control", "no-cache"); + res.setHeader("Content-Type", "text/event-stream"); + res.setHeader("Access-Control-Allow-Origin", "*"); + res.setHeader("Connection", "keep-alive"); + res.flushHeaders(); + + const uniqueDirName = randomUUID(); + const resultDir = join(OUTPUT_ROOT_DIR, uniqueDirName); + mkdir(resultDir); + const subprocess = await compileVerso(body.data.projectId, body.data.fileContents, resultDir); + + subprocess.stdout.on("data", (data) => { + send({ stream: "stdout", contents: `${data}` }); + }); + subprocess.stderr.on("data", (data) => { + send({ stream: "stderr", contents: `${data}` }); + }); + let finished = false; + subprocess.on("error", (data) => { + finished = true; + send({ success: false, result: `${data}` }); + res.end(); + }); + subprocess.on("close", (data) => { + if (finished) return; + if (data === 0) { + send({ success: true, href: `/verso/view/${uniqueDirName}/html-single` }); + } else { + send({ success: false, result: `process returned non-zero exit code ${data}` }); + } + res.end(); + }); + } +}); + +app.use("/verso/view", express.static(OUTPUT_ROOT_DIR)); diff --git a/verso-server/exec.ts b/verso-server/exec.ts new file mode 100644 index 00000000..f167b9b7 --- /dev/null +++ b/verso-server/exec.ts @@ -0,0 +1,26 @@ +import { spawn } from "node:child_process"; +import type { PathLike } from "node:fs"; +import { writeFile } from "node:fs/promises"; +import { join } from "node:path"; + +const PROJ_PATH = process.env.PROJ_PATH || "Projects"; + +/** + * Spawn a process that, upon success, will put Verso output in the provided + * directory. + * + * @param projectId - the project key (e.g. `"verso-server"`) + * @param theLeanFileContents - text contents of a single-file Lean document + * @param outputDir - an existing directory where the output is expected to be placed + */ +export async function compileVerso( + projectId: string, + theLeanFileContents: string, + outputDir: string, +) { + const theLeanFileLoc = join(PROJ_PATH, projectId, "TheLeanFile.lean"); + await writeFile(theLeanFileLoc, theLeanFileContents); + return spawn("lake", ["--old", "exe", "mkdoc", "--output", outputDir], { + cwd: join(PROJ_PATH, projectId), + }); +} diff --git a/verso-server/server.ts b/verso-server/server.ts new file mode 100644 index 00000000..027ce1a9 --- /dev/null +++ b/verso-server/server.ts @@ -0,0 +1,9 @@ +// Run this script to launch the server. +/* eslint no-console: "off" */ + +import { app } from "./app.ts"; + +const PORT = parseInt(process.env.PORT || "8081"); +app.listen(PORT, () => { + console.log(`Verso compilation server is running on port ${PORT}`); +}); diff --git a/verso-server/tsconfig.json b/verso-server/tsconfig.json new file mode 100644 index 00000000..ac248261 --- /dev/null +++ b/verso-server/tsconfig.json @@ -0,0 +1,23 @@ +/* Visit https://www.typescriptlang.org/tsconfig/ to learn about this file */ +{ + "compilerOptions": { + /* Basic configuration */ + "lib": ["ES2024"], + "module": "node18", + "skipLibCheck": true, + + /* Support the use of type stripping in Node */ + "allowImportingTsExtensions": true, + "rewriteRelativeImportExtensions": true, + "erasableSyntaxOnly": true, + "verbatimModuleSyntax": true, + + /* Linting */ + "strict": true, + "forceConsistentCasingInFileNames": true, + "noFallthroughCasesInSwitch": true, + "noImplicitReturns": true, + "noUncheckedSideEffectImports": true + }, + "include": ["./**/*.ts"], +} From 024a0931ca31700217996f4e066928a447c3b3ef Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 16 Feb 2026 18:56:38 -0500 Subject: [PATCH 04/26] Support, in theory, bubblewrap execution --- .gitignore | 2 + Projects/MathlibDemo/lake-manifest.json | 2 +- Projects/verso-nightly/build.sh | 2 +- package.json | 4 +- verso-server/app.ts | 13 ++++--- verso-server/bubblewrap.sh | 31 +++++++++++++++ verso-server/exec.ts | 50 ++++++++++++++++++------- 7 files changed, 82 insertions(+), 22 deletions(-) create mode 100755 verso-server/bubblewrap.sh diff --git a/.gitignore b/.gitignore index 2591cfb1..c4841d7a 100644 --- a/.gitignore +++ b/.gitignore @@ -19,6 +19,8 @@ cypress/videos _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 d47b8a91..c9a56e92 100644 --- a/Projects/MathlibDemo/lake-manifest.json +++ b/Projects/MathlibDemo/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "df5c1e1b57202011acb349cd2f22fcd5cec09bc8", + "rev": "32fe3f9354729a268ba178d0b5ae06eca180c247", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/Projects/verso-nightly/build.sh b/Projects/verso-nightly/build.sh index 974d6225..cabd3ac5 100755 --- a/Projects/verso-nightly/build.sh +++ b/Projects/verso-nightly/build.sh @@ -5,4 +5,4 @@ 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 \ No newline at end of file +lake exe mkdoc --output /dev/null \ No newline at end of file diff --git a/package.json b/package.json index 8af5a735..b1b703aa 100644 --- a/package.json +++ b/package.json @@ -8,6 +8,7 @@ }, "files": [ "client/dist", + "verso-server", "lsp-server" ], "scripts": { @@ -15,9 +16,10 @@ "start:lsp-server": "cd lsp-server && NODE_ENV=development nodemon ./index.mjs", "start:client": "NODE_ENV=development vite --host", "start:verso-server": "NODE_ENV=development nodemon ./verso-server/server.ts", - "build": "npm run build:projects && npm run build:client", + "build": "npm run build:projects && npm run build:client && npm run build:verso-server", "build:projects": "Projects/build.sh", "build:client": "tsc -b && NODE_ENV=production vite build", + "build:verso-server": "cd verso-server && tsc", "production": "NODE_ENV=production node lsp-server/index.mjs", "dev": "vite", "lint": "eslint . --ext ts,tsx --report-unused-disable-directives --max-warnings 0", diff --git a/verso-server/app.ts b/verso-server/app.ts index 6f483bce..b5c988ca 100644 --- a/verso-server/app.ts +++ b/verso-server/app.ts @@ -2,15 +2,12 @@ import express from "express"; import { z } from "zod"; import { mkdir, mkdtemp } from "node:fs/promises"; import { join } from "node:path"; -import { tmpdir } from "node:os"; import { randomUUID } from "node:crypto"; -import { compileVerso } from "./exec.ts"; +import { compileVerso, OUTPUT_ROOT_DIR } from "./exec.ts"; export const app = express(); app.use(express.json()); -const OUTPUT_ROOT_DIR = await mkdtemp(join(tmpdir(), "verso-output-")); - const zBuildRequest = z.object({ projectId: z.string().regex(/^[A-Za-z0-9][A-Za-z0-9.-]*$/), fileContents: z.string(), @@ -36,7 +33,10 @@ app.post("/verso/api/singlepage", async (req, res) => { const uniqueDirName = randomUUID(); const resultDir = join(OUTPUT_ROOT_DIR, uniqueDirName); mkdir(resultDir); - const subprocess = await compileVerso(body.data.projectId, body.data.fileContents, resultDir); + const [resultPath, subprocess] = await compileVerso( + body.data.projectId, + body.data.fileContents, + ); subprocess.stdout.on("data", (data) => { send({ stream: "stdout", contents: `${data}` }); @@ -53,7 +53,7 @@ app.post("/verso/api/singlepage", async (req, res) => { subprocess.on("close", (data) => { if (finished) return; if (data === 0) { - send({ success: true, href: `/verso/view/${uniqueDirName}/html-single` }); + send({ success: true, href: `/verso/view/${resultPath}/html-single` }); } else { send({ success: false, result: `process returned non-zero exit code ${data}` }); } @@ -62,4 +62,5 @@ app.post("/verso/api/singlepage", async (req, res) => { } }); +console.log(`Serving static files from ${OUTPUT_ROOT_DIR}`) app.use("/verso/view", express.static(OUTPUT_ROOT_DIR)); diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh new file mode 100755 index 00000000..0eaa87f8 --- /dev/null +++ b/verso-server/bubblewrap.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +ulimit -t 120 + +# Resolve symlinks +INPUT_DIR="$(realpath "$1")" +shift +WORK_DIR="$(realpath "$1")" +shift +OUTPUT_DIR="$(realpath "$1")" +shift + +LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" + +GIT_PATH=$(dirname $(realpath $(which git))) +DIRNAME_PATH=$(dirname $(realpath $(which dirname))) + +exec bwrap \ + --ro-bind /nix /nix \ + --ro-bind "$LEAN_ROOT" /lean \ + --dev /dev \ + --tmpfs /tmp \ + --proc /proc \ + --clearenv \ + --setenv PATH "$GIT_PATH:$DIRNAME_PATH" \ + --overlay-src /home/versobox/test/lean4web/Projects/verso-nightly \ + --overlay $PROJECT $OVERLAY_WORKDIR /project \ + --unshare-all \ + --die-with-parent \ + --chdir /project \ + /lean/bin/lake --old --keep-toolchain exe mkdoc diff --git a/verso-server/exec.ts b/verso-server/exec.ts index f167b9b7..b5a7eb63 100644 --- a/verso-server/exec.ts +++ b/verso-server/exec.ts @@ -1,26 +1,50 @@ -import { spawn } from "node:child_process"; -import type { PathLike } from "node:fs"; -import { writeFile } from "node:fs/promises"; +import { spawn, type ChildProcessWithoutNullStreams } from "node:child_process"; +import { randomUUID } from "node:crypto"; +import { mkdir, mkdtemp, writeFile } from "node:fs/promises"; +import { tmpdir } from "node:os"; import { join } from "node:path"; -const PROJ_PATH = process.env.PROJ_PATH || "Projects"; +const IS_DEV = process.env.NODE_ENV === "development"; +const PROJ_ROOT = process.env.PROJ_ROOT || "Projects"; +export const OUTPUT_ROOT_DIR = await mkdtemp(join(tmpdir(), "verso-output-")); + /** * Spawn a process that, upon success, will put Verso output in the provided * directory. - * + * * @param projectId - the project key (e.g. `"verso-server"`) * @param theLeanFileContents - text contents of a single-file Lean document - * @param outputDir - an existing directory where the output is expected to be placed + * @returns [outDir, process] - a process and where it's writing its files */ export async function compileVerso( projectId: string, theLeanFileContents: string, - outputDir: string, -) { - const theLeanFileLoc = join(PROJ_PATH, projectId, "TheLeanFile.lean"); - await writeFile(theLeanFileLoc, theLeanFileContents); - return spawn("lake", ["--old", "exe", "mkdoc", "--output", outputDir], { - cwd: join(PROJ_PATH, projectId), - }); +): Promise<[string, ChildProcessWithoutNullStreams]> { + const outputDirName = randomUUID(); + const outputDir = join(OUTPUT_ROOT_DIR, outputDirName); + await mkdir(outputDir); + const projDir = join(PROJ_ROOT, projectId); + + if (IS_DEV) { + const theLeanFileLoc = join(projDir, "TheLeanFile.lean"); + await mkdir(join(outputDir, "_out")); + await writeFile(theLeanFileLoc, theLeanFileContents); + return [ + join(outputDirName, "_out"), + spawn("lake", ["--old", "exe", "mkdoc", "--output", join(outputDir, "_out")], { + cwd: projDir, + }), + ]; + } else { + const workDirName = randomUUID(); + const workDir = join(OUTPUT_ROOT_DIR, outputDirName); + await mkdir(workDir); + return [ + join(outputDirName, "_out"), + spawn(join(import.meta.dirname, "bubblewrap.sh"), [projDir, workDir, outputDir], { + cwd: projDir, + }), + ]; + } } From 6e19a41d2d17ef93dca9aef3f479617c273101e1 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 09:07:01 -0500 Subject: [PATCH 05/26] build-without-projects target --- package.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/package.json b/package.json index b1b703aa..6936c8d9 100644 --- a/package.json +++ b/package.json @@ -16,7 +16,8 @@ "start:lsp-server": "cd lsp-server && NODE_ENV=development nodemon ./index.mjs", "start:client": "NODE_ENV=development vite --host", "start:verso-server": "NODE_ENV=development nodemon ./verso-server/server.ts", - "build": "npm run build:projects && npm run build:client && npm run build:verso-server", + "build-without-projects": "npm run build:client && npm run build:verso-server", + "build": "npm run build:projects && npm run build-without-projects", "build:projects": "Projects/build.sh", "build:client": "tsc -b && NODE_ENV=production vite build", "build:verso-server": "cd verso-server && tsc", From 7abb66d619df3c1e26369a809b7f78d41909417f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 10:45:18 -0500 Subject: [PATCH 06/26] workdir bug --- Projects/verso-nightly/TheLeanFile.lean | 12 +++++++++++- verso-server/exec.ts | 2 +- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/Projects/verso-nightly/TheLeanFile.lean b/Projects/verso-nightly/TheLeanFile.lean index 21f189ce..71bb9232 100644 --- a/Projects/verso-nightly/TheLeanFile.lean +++ b/Projects/verso-nightly/TheLeanFile.lean @@ -2,4 +2,14 @@ import VersoManual open Verso Doc open Verso.Genre Manual open Verso.Genre.Manual.InlineLean -#doc (Manual) "Mydoc" => Would you like a doc?I'll give you a doc if you'd like. \ No newline at end of file + +set_option doc.verso true + +/-- +Example using lean docstrings, enabling us +to explain that this is a {Lean.Doc.name}`Nat` +equivalent to {Lean.Doc.lean}`Nat.zero.succ.succ.succ`. +-/ +def x := 4 + +#doc (Manual) "Mydoc" => Would you like a doc?I'll give you a doc if you'd like. diff --git a/verso-server/exec.ts b/verso-server/exec.ts index b5a7eb63..006eb20b 100644 --- a/verso-server/exec.ts +++ b/verso-server/exec.ts @@ -38,7 +38,7 @@ export async function compileVerso( ]; } else { const workDirName = randomUUID(); - const workDir = join(OUTPUT_ROOT_DIR, outputDirName); + const workDir = join(OUTPUT_ROOT_DIR, workDirName); await mkdir(workDir); return [ join(outputDirName, "_out"), From 42747bb7727cb8cc5f79176cdefdb7d494170dd7 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 10:47:40 -0500 Subject: [PATCH 07/26] lean file loc in place --- verso-server/exec.ts | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/verso-server/exec.ts b/verso-server/exec.ts index 006eb20b..faced556 100644 --- a/verso-server/exec.ts +++ b/verso-server/exec.ts @@ -8,7 +8,6 @@ const IS_DEV = process.env.NODE_ENV === "development"; const PROJ_ROOT = process.env.PROJ_ROOT || "Projects"; export const OUTPUT_ROOT_DIR = await mkdtemp(join(tmpdir(), "verso-output-")); - /** * Spawn a process that, upon success, will put Verso output in the provided * directory. @@ -25,11 +24,11 @@ export async function compileVerso( const outputDir = join(OUTPUT_ROOT_DIR, outputDirName); await mkdir(outputDir); const projDir = join(PROJ_ROOT, projectId); + const theLeanFileLoc = join(projDir, "TheLeanFile.lean"); + await mkdir(join(outputDir, "_out")); + await writeFile(theLeanFileLoc, theLeanFileContents); if (IS_DEV) { - const theLeanFileLoc = join(projDir, "TheLeanFile.lean"); - await mkdir(join(outputDir, "_out")); - await writeFile(theLeanFileLoc, theLeanFileContents); return [ join(outputDirName, "_out"), spawn("lake", ["--old", "exe", "mkdoc", "--output", join(outputDir, "_out")], { From 22c9f63e4e1bb176232d0be9ff3706c59987c442 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 12:40:19 -0500 Subject: [PATCH 08/26] Back to full path --- verso-server/bubblewrap.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index 0eaa87f8..fcb012b5 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -12,8 +12,8 @@ shift LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" -GIT_PATH=$(dirname $(realpath $(which git))) -DIRNAME_PATH=$(dirname $(realpath $(which dirname))) +# GIT_PATH=$(dirname $(realpath $(which git))) +# DIRNAME_PATH=$(dirname $(realpath $(which dirname))) exec bwrap \ --ro-bind /nix /nix \ @@ -22,9 +22,9 @@ exec bwrap \ --tmpfs /tmp \ --proc /proc \ --clearenv \ - --setenv PATH "$GIT_PATH:$DIRNAME_PATH" \ + --setenv PATH "$PATH" \ --overlay-src /home/versobox/test/lean4web/Projects/verso-nightly \ - --overlay $PROJECT $OVERLAY_WORKDIR /project \ + --overlay "$PROJECT" "$OVERLAY_WORKDIR" /project \ --unshare-all \ --die-with-parent \ --chdir /project \ From 56b29a5c78c14c487df863cbaf75fba37d1ad36c Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 12:51:38 -0500 Subject: [PATCH 09/26] tweak script --- verso-server/bubblewrap.sh | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index fcb012b5..e8d7e60c 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -12,19 +12,27 @@ shift LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" -# GIT_PATH=$(dirname $(realpath $(which git))) -# DIRNAME_PATH=$(dirname $(realpath $(which dirname))) +GIT_PATH=$(dirname $(realpath $(which git))) +DIRNAME_PATH=$(dirname $(realpath $(which dirname))) +echo "git path $GIT_PATH" +echo "dirname path $DIRNAME_PATH" +eco "lean root $LEAN_ROOT" exec bwrap \ --ro-bind /nix /nix \ + --ro-bind /run /run \ --ro-bind "$LEAN_ROOT" /lean \ + \ --dev /dev \ --tmpfs /tmp \ --proc /proc \ + \ --clearenv \ --setenv PATH "$PATH" \ - --overlay-src /home/versobox/test/lean4web/Projects/verso-nightly \ - --overlay "$PROJECT" "$OVERLAY_WORKDIR" /project \ + \ + --overlay-src "$INPUT_DIR" \ + --overlay "$OUTPUT_DIR" "$WORK_DIR" /project \ + \ --unshare-all \ --die-with-parent \ --chdir /project \ From 38ca0736f1e3942094db7eedc04b04baeebfd9fc Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:03:10 -0500 Subject: [PATCH 10/26] x-accel-buffering no --- verso-server/app.ts | 2 ++ 1 file changed, 2 insertions(+) diff --git a/verso-server/app.ts b/verso-server/app.ts index b5c988ca..0940c1f4 100644 --- a/verso-server/app.ts +++ b/verso-server/app.ts @@ -28,6 +28,8 @@ app.post("/verso/api/singlepage", async (req, res) => { res.setHeader("Content-Type", "text/event-stream"); res.setHeader("Access-Control-Allow-Origin", "*"); res.setHeader("Connection", "keep-alive"); + // https://stackoverflow.com/questions/13672743/eventsource-server-sent-events-through-nginx/33414096#33414096 + res.setHeader("X-Accel-Buffering", "no"); res.flushHeaders(); const uniqueDirName = randomUUID(); From 11f7f60db1e99a84e6ba30a5c0deb711d1a4f6f9 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:16:57 -0500 Subject: [PATCH 11/26] Remove mysterious failing which commands for path construction --- verso-server/bubblewrap.sh | 6 ------ 1 file changed, 6 deletions(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index e8d7e60c..1b264bea 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -12,12 +12,6 @@ shift LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" -GIT_PATH=$(dirname $(realpath $(which git))) -DIRNAME_PATH=$(dirname $(realpath $(which dirname))) -echo "git path $GIT_PATH" -echo "dirname path $DIRNAME_PATH" -eco "lean root $LEAN_ROOT" - exec bwrap \ --ro-bind /nix /nix \ --ro-bind /run /run \ From 5eb3e904cde6e8117360e3c61515b43e81eccb9f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:21:23 -0500 Subject: [PATCH 12/26] add back mysterious failure --- verso-server/bubblewrap.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index 1b264bea..e8d7e60c 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -12,6 +12,12 @@ shift LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" +GIT_PATH=$(dirname $(realpath $(which git))) +DIRNAME_PATH=$(dirname $(realpath $(which dirname))) +echo "git path $GIT_PATH" +echo "dirname path $DIRNAME_PATH" +eco "lean root $LEAN_ROOT" + exec bwrap \ --ro-bind /nix /nix \ --ro-bind /run /run \ From 483d3d4314ee0c26f2a5698b89101b6086e80989 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:23:47 -0500 Subject: [PATCH 13/26] typo --- verso-server/bubblewrap.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index e8d7e60c..7e043931 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -16,7 +16,7 @@ GIT_PATH=$(dirname $(realpath $(which git))) DIRNAME_PATH=$(dirname $(realpath $(which dirname))) echo "git path $GIT_PATH" echo "dirname path $DIRNAME_PATH" -eco "lean root $LEAN_ROOT" +echo "lean root $LEAN_ROOT" exec bwrap \ --ro-bind /nix /nix \ From 72b399e7073fc39eecf9e2199e874b5b31d90143 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:27:01 -0500 Subject: [PATCH 14/26] test restricted path --- verso-server/bubblewrap.sh | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index 7e043931..abca85f4 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -20,15 +20,13 @@ echo "lean root $LEAN_ROOT" exec bwrap \ --ro-bind /nix /nix \ - --ro-bind /run /run \ - --ro-bind "$LEAN_ROOT" /lean \ \ --dev /dev \ --tmpfs /tmp \ --proc /proc \ \ --clearenv \ - --setenv PATH "$PATH" \ + --setenv PATH "$GIT_PATH:$DIRNAME_PATH" \ \ --overlay-src "$INPUT_DIR" \ --overlay "$OUTPUT_DIR" "$WORK_DIR" /project \ @@ -36,4 +34,4 @@ exec bwrap \ --unshare-all \ --die-with-parent \ --chdir /project \ - /lean/bin/lake --old --keep-toolchain exe mkdoc + $LEAN_ROOT/bin/lake --old --keep-toolchain exe mkdoc From 73af074349410c4d75c05cbe7f824b3b218b8a7f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:30:00 -0500 Subject: [PATCH 15/26] Split up lines into messages --- verso-server/app.ts | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/verso-server/app.ts b/verso-server/app.ts index 0940c1f4..bfc0dbe2 100644 --- a/verso-server/app.ts +++ b/verso-server/app.ts @@ -41,10 +41,14 @@ app.post("/verso/api/singlepage", async (req, res) => { ); subprocess.stdout.on("data", (data) => { - send({ stream: "stdout", contents: `${data}` }); + for (const line of `${data}`.split("\n")) { + send({ stream: "stdout", contents: line }); + } }); subprocess.stderr.on("data", (data) => { - send({ stream: "stderr", contents: `${data}` }); + for (const line of `${data}`.split("\n")) { + send({ stream: "stderr", contents: line }); + } }); let finished = false; subprocess.on("error", (data) => { @@ -64,5 +68,5 @@ app.post("/verso/api/singlepage", async (req, res) => { } }); -console.log(`Serving static files from ${OUTPUT_ROOT_DIR}`) +console.log(`Serving static files from ${OUTPUT_ROOT_DIR}`); app.use("/verso/view", express.static(OUTPUT_ROOT_DIR)); From 8f893de967f5d12651e25bd8451ac81cfd52b211 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:33:51 -0500 Subject: [PATCH 16/26] Now explain why we're doing /lean/bin/lake --- verso-server/bubblewrap.sh | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index abca85f4..6f0ac9fb 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -10,6 +10,9 @@ shift OUTPUT_DIR="$(realpath "$1")" shift +# The LEAN_ROOT will be a path in `/home/$USER/.elan`, and we don't +# want the container to know anything about the `/home`, so +# we'll bind this directory to `/lean` LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" GIT_PATH=$(dirname $(realpath $(which git))) @@ -20,6 +23,7 @@ echo "lean root $LEAN_ROOT" exec bwrap \ --ro-bind /nix /nix \ + --ro-bind "$LEAN_ROOT" /lean \ \ --dev /dev \ --tmpfs /tmp \ @@ -34,4 +38,4 @@ exec bwrap \ --unshare-all \ --die-with-parent \ --chdir /project \ - $LEAN_ROOT/bin/lake --old --keep-toolchain exe mkdoc + /lean/bin/lake --old --keep-toolchain exe mkdoc From 8066ab4c715217b3e40917fac70a8ab6b311cdab Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:37:41 -0500 Subject: [PATCH 17/26] Trim before splitting --- verso-server/app.ts | 4 ++-- verso-server/bubblewrap.sh | 4 ---- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/verso-server/app.ts b/verso-server/app.ts index bfc0dbe2..05ea35e6 100644 --- a/verso-server/app.ts +++ b/verso-server/app.ts @@ -41,12 +41,12 @@ app.post("/verso/api/singlepage", async (req, res) => { ); subprocess.stdout.on("data", (data) => { - for (const line of `${data}`.split("\n")) { + for (const line of `${data}`.trim().split("\n")) { send({ stream: "stdout", contents: line }); } }); subprocess.stderr.on("data", (data) => { - for (const line of `${data}`.split("\n")) { + for (const line of `${data}`.trim().split("\n")) { send({ stream: "stderr", contents: line }); } }); diff --git a/verso-server/bubblewrap.sh b/verso-server/bubblewrap.sh index 6f0ac9fb..78ba90bb 100755 --- a/verso-server/bubblewrap.sh +++ b/verso-server/bubblewrap.sh @@ -14,12 +14,8 @@ shift # want the container to know anything about the `/home`, so # we'll bind this directory to `/lean` LEAN_ROOT="$(cd $INPUT_DIR && lean --print-prefix)" - GIT_PATH=$(dirname $(realpath $(which git))) DIRNAME_PATH=$(dirname $(realpath $(which dirname))) -echo "git path $GIT_PATH" -echo "dirname path $DIRNAME_PATH" -echo "lean root $LEAN_ROOT" exec bwrap \ --ro-bind /nix /nix \ From 24f21358520127acbaf18765e54f91d5b60103ef Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 13:38:08 -0500 Subject: [PATCH 18/26] Trim error as well --- verso-server/app.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verso-server/app.ts b/verso-server/app.ts index 05ea35e6..7b04fdf9 100644 --- a/verso-server/app.ts +++ b/verso-server/app.ts @@ -53,7 +53,7 @@ app.post("/verso/api/singlepage", async (req, res) => { let finished = false; subprocess.on("error", (data) => { finished = true; - send({ success: false, result: `${data}` }); + send({ success: false, result: `${data}`.trim() }); res.end(); }); subprocess.on("close", (data) => { From 0bc261e66ad54f6aa88ad465d54a9807eb3528d1 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 14:38:00 -0500 Subject: [PATCH 19/26] Add verso to dropdown --- client/src/config/config.tsx | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/client/src/config/config.tsx b/client/src/config/config.tsx index ac9d929a..2829db2f 100644 --- a/client/src/config/config.tsx +++ b/client/src/config/config.tsx @@ -18,7 +18,9 @@ const lean4webConfig : LeanWebConfig = { { "folder": "mathlib-v4.24.0", "name": "Mathlib v4.24.0"}, { "folder": "lean-nightly", - "name": "Lean Nightly (without mathlib)"} + "name": "Lean Nightly (without mathlib)"}, + { "folder": "verso-nightly", + "name": "Verso Nightly"} ], "serverCountry": 'Finland', "contactDetails": null, From d73a96ddd701ab14bb2558f0c41a4e2dc9af2e10 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 14:49:47 -0500 Subject: [PATCH 20/26] Add a leanc arg to speed compilation --- Projects/verso-nightly/lakefile.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/Projects/verso-nightly/lakefile.toml b/Projects/verso-nightly/lakefile.toml index 58ced4b9..f812c6b7 100644 --- a/Projects/verso-nightly/lakefile.toml +++ b/Projects/verso-nightly/lakefile.toml @@ -1,5 +1,6 @@ name = "verso-nightly" version = "0.1.0" +moreLeancArgs = ["-O0"] defaultTargets = ["TheLeanFile", "mkdoc"] [[require]] From 456427e1107ecc563bfd6b2b7979cdbb4ebaca29 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 17 Feb 2026 20:46:03 -0500 Subject: [PATCH 21/26] Updated Verso preview with streaming feedback --- Projects/verso-nightly/TheLeanFile.lean | 10 +- .../TheLeanFile/VersoExample.lean | 24 +++ client/src/App.tsx | 16 +- client/src/TabPlugins/VersoPreview.tsx | 94 +++++++++++ client/src/TabView.tsx | 119 ++++++++++++++ client/src/config/config.tsx | 8 +- client/src/config/docs.tsx | 9 +- client/src/css/Editor.css | 2 + client/src/css/TabView.css | 60 +++++++ verso-server/app.ts | 146 ++++++++++-------- vite.config.ts | 3 + 11 files changed, 412 insertions(+), 79 deletions(-) create mode 100644 Projects/verso-nightly/TheLeanFile/VersoExample.lean create mode 100644 client/src/TabPlugins/VersoPreview.tsx create mode 100644 client/src/TabView.tsx create mode 100644 client/src/css/TabView.css diff --git a/Projects/verso-nightly/TheLeanFile.lean b/Projects/verso-nightly/TheLeanFile.lean index 71bb9232..35711397 100644 --- a/Projects/verso-nightly/TheLeanFile.lean +++ b/Projects/verso-nightly/TheLeanFile.lean @@ -3,13 +3,7 @@ open Verso Doc open Verso.Genre Manual open Verso.Genre.Manual.InlineLean -set_option doc.verso true -/-- -Example using lean docstrings, enabling us -to explain that this is a {Lean.Doc.name}`Nat` -equivalent to {Lean.Doc.lean}`Nat.zero.succ.succ.succ`. --/ -def x := 4 +#doc (Manual) "Mydoc" => Would you like a dddoc? -#doc (Manual) "Mydoc" => Would you like a doc?I'll give you a doc if you'd like. +I'll give you a doc iddf you'd like diff --git a/Projects/verso-nightly/TheLeanFile/VersoExample.lean b/Projects/verso-nightly/TheLeanFile/VersoExample.lean new file mode 100644 index 00000000..0177ded5 --- /dev/null +++ b/Projects/verso-nightly/TheLeanFile/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/client/src/App.tsx b/client/src/App.tsx index 42d60da3..da35d2b0 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -21,6 +21,7 @@ import { useWindowDimensions } from './utils/WindowWidth' // CSS import './css/App.css' import './css/Editor.css' +import TabView from './TabView' /** Returns true if the browser wants dark mode */ function isBrowserDefaultDark() { @@ -429,13 +430,14 @@ 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..fc00cdc4 --- /dev/null +++ b/client/src/TabPlugins/VersoPreview.tsx @@ -0,0 +1,94 @@ +import { useEffect, useRef, useState } from 'react' +import { LeanWebPlugin } from '../config/docs' + +interface VersoPreviewProps { + currentTab: 'info' | LeanWebPlugin + isUsingMobile: boolean + code: string + projectId: string +} + +function VersoPreview({ currentTab, isUsingMobile, code, projectId }: VersoPreviewProps) { + const [isLoading, setIsLoading] = useState(false) + const [previewedProject, setPreviewedProject] = useState(null) + const [previewedCode, setPreviewedCode] = useState(null) + const [hrefForIframe, setHrefForIframe] = useState(null) + const [output, setOutput] = useState([]) + const scrollerRef = useRef(null) + + const loadCode = () => { + setIsLoading(true) + setOutput(['connecting...']) + + 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) + setPreviewedProject(projectId) + }) + .catch((err) => { + setIsLoading(false) + setOutput((info) => [...info, 'Unexpected response from server.']) + console.error(err) + }) + .finally(() => read.close()) + }) + } + + const [lastTab, setLastTab] = useState(currentTab) + useEffect(() => { + if (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]) + + return ( +
+ +
+
+ {output.join('\n')} +
+
+ {hrefForIframe &&