diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f8c6c89..c41af77 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,7 +34,7 @@ jobs: run: npx vsce package - name: Package LSP server - run: cp server/out/main.js "fstar-language-server-$(jq -r .version package.json).js" + run: cp lspserver/out/main.js "fstar-language-server-$(jq -r .version package.json).js" - name: Upload artifact uses: actions/upload-artifact@v4 diff --git a/DESIGN.md b/DESIGN.md index 157261a..3de3d71 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -3,7 +3,7 @@ The diagram below presents a high-level overview of the design of this extension. ``` - Client Server F* processes + Extension LSP Server F* processes vscode-languageclient/node vscode-languageserver/node Native F* ___________ .---------. events .---------------. .---------------. |_fstar.exe_|_ @@ -14,12 +14,12 @@ The diagram below presents a high-level overview of the design of this extension ## Workflow -* The editor starts the client on an initialization event +* The editor starts the extension on an initialization event -* The client launches a language server, implemented in server.ts, executing on the nodejs server runtime. - The client and server interact using Language Server Protocol (LSP). +* The extension launches a language server, implemented in server.ts, executing on the nodejs server runtime. + The extension and server interact using Language Server Protocol (LSP). -* For each F* document opened by the editor, the server launches multiple fstar.exe processes. +* For each F* document opened by the editor, the LSP server launches multiple fstar.exe processes. F* implements its own IDE protocol, designed first for use by F*'s emacs mode, fstar-mode.el. We reuse that protocol to communicate between server.ts and fstar.exe, communicating using JSON-formatted IDE messages over stdin/stdout. @@ -106,19 +106,7 @@ requests to check fragments of the document whose position is at `p` or beyond. ## Events from server.ts to extension.ts In addition to standard LSP diagnostics, hover events, definitions, completions etc., -we have the following four custom messages send from server.ts to client.ts - -* `fstar-vscode-extension/statusStarted`: A message to show which fragment of the document - is currently being processed by `fstar_ide`, used to show hourglass icons. - -* `fstar-vscode-extension/statusOk`: A message to show which fragment of the document was checked, - either fully checked or lax checked, showing either checkmarks or question marks - in the gutter. - -* `fstar-vscode-extension/statusClear`: A message to clear all gutter icons. - -* `fstar-vscode-extension/statusFailed`: A message to indicate that checking has failed on a fragment, - which causes the extension to clear any hourglass icons that remain. +we have custom messages, see `fstarLspExtensions.ts` for details. # Publishing an extension @@ -126,6 +114,5 @@ The extension is automatically published by CI if you push a release: 1. `npx vsce package minor` to bump the version and create a release tag. 2. `git push --follow-tags` to push the release. - If you want to build the extension for local testing, you can create a `.vsix` using `npx vsce package`. diff --git a/client/src/fstarLspExtensions.ts b/client/src/fstarLspExtensions.ts deleted file mode 120000 index 5d8fbf8..0000000 --- a/client/src/fstarLspExtensions.ts +++ /dev/null @@ -1 +0,0 @@ -../../server/src/fstarLspExtensions.ts \ No newline at end of file diff --git a/eslint.config.mjs b/eslint.config.mjs index 4ef3030..2910531 100644 --- a/eslint.config.mjs +++ b/eslint.config.mjs @@ -9,7 +9,7 @@ export default tseslint.config( languageOptions: { parserOptions: { projectService: { - allowDefaultProject: ['server/tests/*.ts', '*.mjs'], + allowDefaultProject: ['lspserver/tests/*.ts', '*.mjs'], defaultProject: 'tsconfig.json', }, // @ts-expect-error expected diff --git a/client/package-lock.json b/extension/package-lock.json similarity index 99% rename from client/package-lock.json rename to extension/package-lock.json index 0ccc867..2266203 100644 --- a/client/package-lock.json +++ b/extension/package-lock.json @@ -1,11 +1,11 @@ { - "name": "fstar-vscode-assistant-client", + "name": "fstar-vscode-extension", "version": "0.0.2", "lockfileVersion": 2, "requires": true, "packages": { "": { - "name": "fstar-vscode-assistant-client", + "name": "fstar-vscode-extension", "version": "0.0.2", "license": "MIT", "dependencies": { diff --git a/client/package.json b/extension/package.json similarity index 94% rename from client/package.json rename to extension/package.json index b62012a..131ce62 100644 --- a/client/package.json +++ b/extension/package.json @@ -1,5 +1,5 @@ { - "name": "fstar-vscode-assistant-client", + "name": "fstar-vscode-extension", "description": "VSCode part of fstar-vscode-assistant", "author": "Microsoft Corporation", "license": "MIT", diff --git a/client/src/binaryeditors.ts b/extension/src/binaryeditors.ts similarity index 100% rename from client/src/binaryeditors.ts rename to extension/src/binaryeditors.ts diff --git a/client/src/extension.ts b/extension/src/extension.ts similarity index 96% rename from client/src/extension.ts rename to extension/src/extension.ts index 3759a15..27ef881 100644 --- a/client/src/extension.ts +++ b/extension/src/extension.ts @@ -135,7 +135,7 @@ function updateDecorations() { export async function activate(context: ExtensionContext) { // The server is implemented in node const serverModule = context.asAbsolutePath( - path.join('server', 'out', 'main.js') + path.join('lspserver', 'out', 'main.js') ); // If the extension is launched in debug mode then the debug server options are used diff --git a/extension/src/fstarLspExtensions.ts b/extension/src/fstarLspExtensions.ts new file mode 120000 index 0000000..e049575 --- /dev/null +++ b/extension/src/fstarLspExtensions.ts @@ -0,0 +1 @@ +../../lspserver/src/fstarLspExtensions.ts \ No newline at end of file diff --git a/client/tsconfig.json b/extension/tsconfig.json similarity index 100% rename from client/tsconfig.json rename to extension/tsconfig.json diff --git a/server/package-lock.json b/lspserver/package-lock.json similarity index 99% rename from server/package-lock.json rename to lspserver/package-lock.json index dba1fe8..67266fc 100644 --- a/server/package-lock.json +++ b/lspserver/package-lock.json @@ -1,11 +1,11 @@ { - "name": "fstar-vscode-assistant-server", + "name": "fstar-lspserver", "version": "0.0.2", "lockfileVersion": 2, "requires": true, "packages": { "": { - "name": "fstar-vscode-assistant-server", + "name": "fstar-lspserver", "version": "0.0.2", "license": "MIT", "dependencies": { diff --git a/server/package.json b/lspserver/package.json similarity index 95% rename from server/package.json rename to lspserver/package.json index ac3575a..32130b6 100644 --- a/server/package.json +++ b/lspserver/package.json @@ -1,5 +1,5 @@ { - "name": "fstar-vscode-assistant-server", + "name": "fstar-lspserver", "description": "Server side of fstar-vscode-assistant.", "version": "0.0.2", "author": "Microsoft Corporation", diff --git a/server/src/fstar.ts b/lspserver/src/fstar.ts similarity index 100% rename from server/src/fstar.ts rename to lspserver/src/fstar.ts diff --git a/server/src/fstarLspExtensions.ts b/lspserver/src/fstarLspExtensions.ts similarity index 100% rename from server/src/fstarLspExtensions.ts rename to lspserver/src/fstarLspExtensions.ts diff --git a/server/src/fstar_connection.ts b/lspserver/src/fstar_connection.ts similarity index 100% rename from server/src/fstar_connection.ts rename to lspserver/src/fstar_connection.ts diff --git a/server/src/fstar_messages.ts b/lspserver/src/fstar_messages.ts similarity index 100% rename from server/src/fstar_messages.ts rename to lspserver/src/fstar_messages.ts diff --git a/server/src/main.ts b/lspserver/src/main.ts similarity index 100% rename from server/src/main.ts rename to lspserver/src/main.ts diff --git a/server/src/server.ts b/lspserver/src/server.ts similarity index 100% rename from server/src/server.ts rename to lspserver/src/server.ts diff --git a/server/src/settings.ts b/lspserver/src/settings.ts similarity index 100% rename from server/src/settings.ts rename to lspserver/src/settings.ts diff --git a/server/src/signals.ts b/lspserver/src/signals.ts similarity index 100% rename from server/src/signals.ts rename to lspserver/src/signals.ts diff --git a/server/src/utils.ts b/lspserver/src/utils.ts similarity index 100% rename from server/src/utils.ts rename to lspserver/src/utils.ts diff --git a/server/tests/fstar_connection.test.ts b/lspserver/tests/fstar_connection.test.ts similarity index 100% rename from server/tests/fstar_connection.test.ts rename to lspserver/tests/fstar_connection.test.ts diff --git a/server/tsconfig.json b/lspserver/tsconfig.json similarity index 100% rename from server/tsconfig.json rename to lspserver/tsconfig.json diff --git a/package.json b/package.json index e9b4fb2..74ae3a2 100644 --- a/package.json +++ b/package.json @@ -17,7 +17,7 @@ "engines": { "vscode": "^1.75.0" }, - "main": "./client/out/extension", + "main": "./extension/out/extension", "contributes": { "languages": [ { @@ -162,11 +162,11 @@ }, "scripts": { "vscode:prepublish": "npm run compile", - "compile": "(cd client && npm run compile) && (cd server && npm run compile)", + "compile": "(cd extension && npm run compile) && (cd lspserver && npm run compile)", "watch": "npm run compile", - "lint": "tsc --noEmit -p server/tsconfig.json && tsc --noEmit -p client/tsconfig.json && eslint", - "postinstall": "cd client && npm install && cd ../server && npm install && cd ..", - "test": "cd server && npm test" + "lint": "tsc --noEmit -p lspserver/tsconfig.json && tsc --noEmit -p extension/tsconfig.json && eslint", + "postinstall": "(cd extension && npm install) && (cd lspserver && npm install)", + "test": "cd lspserver && npm test" }, "devDependencies": { "@eslint/js": "^9.12.0", diff --git a/tsconfig.json b/tsconfig.json index f6e3155..60f1df3 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -17,7 +17,7 @@ ".vscode-test" ], "references": [ - { "path": "./client" }, - { "path": "./server" } + { "path": "./extension" }, + { "path": "./lspserver" } ] } \ No newline at end of file