Verso compliation server (& design that supports additional similar plugins)#6
Open
robsimmons wants to merge 26 commits intoleanprover:nixosfrom
Open
Verso compliation server (& design that supports additional similar plugins)#6robsimmons wants to merge 26 commits intoleanprover:nixosfrom
robsimmons wants to merge 26 commits intoleanprover:nixosfrom
Conversation
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
suggestively introduces the idea of additional servers
robsimmons
commented
Feb 17, 2026
Author
There was a problem hiding this comment.
This should have already been in place, but we didn't notice because all the build.sh stuff is duplicated in the nix configration — mathlib-stable is broken in local development workflows because this doesn't exist.
robsimmons
commented
Feb 17, 2026
Comment on lines
+16
to
+18
| "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", | ||
| "start:verso-server": "NODE_ENV=development nodemon ./verso-server/server.ts", |
Author
There was a problem hiding this comment.
"server" is ambiguous with multiple services running — what we called "server" is properly the server for the LSP connection
robsimmons
commented
Feb 17, 2026
| "build": "npm run build:server && npm run build:client", | ||
| "build:server": "server/build.sh", | ||
| "start:verso-server": "NODE_ENV=development nodemon ./verso-server/server.ts", | ||
| "build-without-projects": "npm run build:client && npm run build:verso-server", |
Author
There was a problem hiding this comment.
Our Nix setup does something different for build:projects, so there needed to be a new target for "build without build:projects"
* Switch away from exe-based html rendering * remove main, switch to SSE * Comments, change bubblewrap command * Cleaning up execution * Prettier update
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR renames the "server" aspect of the live app to "lsp-server" and creates a separate server, "verso-server", that utilizes the same file checkouts as lean4web. This service is accessed through a new optional tab in the React component; the design would support additional plug-in tabs for other purposes, including comparator-style double checking or trusted delaboration.