From d1134340d8fced07e4ed14ef8d77d694975920c5 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Thu, 12 Oct 2023 11:40:53 +0300 Subject: [PATCH] Initial support for TLAPS. --- package-lock.json | 69 +++++++++++++++++++++++++---- package.json | 23 ++++++++++ src/main.ts | 13 ++++++ src/tlaps.ts | 109 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 205 insertions(+), 9 deletions(-) create mode 100644 src/tlaps.ts diff --git a/package-lock.json b/package-lock.json index 7eb5631d..b2426999 100644 --- a/package-lock.json +++ b/package-lock.json @@ -18,6 +18,7 @@ "moment": "^2.29.4", "react": "^18.2.0", "react-dom": "^18.2.0", + "vscode-languageclient": "=9.0.0", "vscode-uri": "^3.0.7" }, "devDependencies": { @@ -664,9 +665,9 @@ "dev": true }, "node_modules/@types/vscode": { - "version": "1.77.0", - "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.77.0.tgz", - "integrity": "sha512-MWFN5R7a33n8eJZJmdVlifjig3LWUNRrPeO1xemIcZ0ae0TEQuRc7G2xV0LUX78RZFECY1plYBn+dP/Acc3L0Q==", + "version": "1.83.0", + "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.83.0.tgz", + "integrity": "sha512-3mUtHqLAVz9hegut9au4xehuBrzRE3UJiQMpoEHkNl6XHliihO7eATx2BMHs0odsmmrwjJrlixx/Pte6M3ygDQ==", "dev": true }, "node_modules/@typescript-eslint/eslint-plugin": { @@ -1036,8 +1037,7 @@ "node_modules/balanced-match": { "version": "1.0.0", "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.0.tgz", - "integrity": "sha1-ibTRmasr7kneFk6gK4nORi1xt2c=", - "dev": true + "integrity": "sha1-ibTRmasr7kneFk6gK4nORi1xt2c=" }, "node_modules/binary-extensions": { "version": "2.2.0", @@ -2208,7 +2208,6 @@ "version": "6.0.0", "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz", "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==", - "dev": true, "dependencies": { "yallist": "^4.0.0" }, @@ -2858,7 +2857,6 @@ "version": "7.5.4", "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz", "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==", - "dev": true, "dependencies": { "lru-cache": "^6.0.0" }, @@ -3093,6 +3091,60 @@ "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw==", "dev": true }, + "node_modules/vscode-jsonrpc": { + "version": "8.2.0", + "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.2.0.tgz", + "integrity": "sha512-C+r0eKJUIfiDIfwJhria30+TYWPtuHJXHtI7J0YlOmKAo7ogxP20T0zxB7HZQIFhIyvoBPwWskjxrvAtfjyZfA==", + "engines": { + "node": ">=14.0.0" + } + }, + "node_modules/vscode-languageclient": { + "version": "9.0.0", + "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-9.0.0.tgz", + "integrity": "sha512-EXP4vhSlEj0DtyxrcWVp5aiFrY0WczKSnKSyrMmSbU7qhASPhM+pfcUzY/z8TQCfOhKvq39fidbdTbq9LnBi7g==", + "dependencies": { + "minimatch": "^5.1.0", + "semver": "^7.3.7", + "vscode-languageserver-protocol": "3.17.4" + }, + "engines": { + "vscode": "^1.82.0" + } + }, + "node_modules/vscode-languageclient/node_modules/brace-expansion": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.1.tgz", + "integrity": "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA==", + "dependencies": { + "balanced-match": "^1.0.0" + } + }, + "node_modules/vscode-languageclient/node_modules/minimatch": { + "version": "5.1.6", + "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.6.tgz", + "integrity": "sha512-lKwV/1brpG6mBUFHtb7NUmtABCb2WZZmm2wNiOA5hAb8VdCS4B3dtMWyvcoViccwAW/COERjXLt0zP1zXUN26g==", + "dependencies": { + "brace-expansion": "^2.0.1" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/vscode-languageserver-protocol": { + "version": "3.17.4", + "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.4.tgz", + "integrity": "sha512-IpaHLPft+UBWf4dOIH15YEgydTbXGz52EMU2h16SfFpYu/yOQt3pY14049mtpJu+4CBHn+hq7S67e7O0AwpRqQ==", + "dependencies": { + "vscode-jsonrpc": "8.2.0", + "vscode-languageserver-types": "3.17.4" + } + }, + "node_modules/vscode-languageserver-types": { + "version": "3.17.4", + "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.4.tgz", + "integrity": "sha512-9YXi5pA3XF2V+NUQg6g+lulNS0ncRCKASYdK3Cs7kiH9sVFXWq27prjkC/B8M/xJLRPPRSPCHVMuBTgRNFh2sQ==" + }, "node_modules/vscode-oniguruma": { "version": "1.7.0", "resolved": "https://registry.npmjs.org/vscode-oniguruma/-/vscode-oniguruma-1.7.0.tgz", @@ -3187,8 +3239,7 @@ "node_modules/yallist": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/y18n/-/y18n-4.0.0.tgz", - "integrity": "sha1-le+U+F7MgdAHwmThkKEg8KPIVms=", - "dev": true + "integrity": "sha1-le+U+F7MgdAHwmThkKEg8KPIVms=" }, "node_modules/yargs": { "version": "16.2.0", diff --git a/package.json b/package.json index ddadd79a..94fcc81f 100644 --- a/package.json +++ b/package.json @@ -203,6 +203,17 @@ "command": "tlaplus.repl.run", "title": "Run REPL in Terminal", "category": "TLA+" + }, + { + "command": "tlaplus.tlaps.check-step", + "title": "Check proof step in TLAPS", + "category": "TLA+" + } + ], + "keybindings": [ + { + "command": "tlaplus.tlaps.check-step", + "key": "ctrl+g ctrl+g" } ], "snippets": [ @@ -373,6 +384,17 @@ "scope": "application", "maxLength": 1000, "description": "Command to produce PDFs from .tex files." + }, + "tlaplus.tlaps.enabled": { + "type": "boolean", + "default": false, + "description": "Enable TLAPS integration." + }, + "tlaplus.tlaps.lspServerCommand": { + "type": "array", + "items": {"type": "string"}, + "description": "Command and arguments to start a TLAPS LSP server.", + "default": ["opam", "exec", "tlapm_lsp", "--", "--log-io", "--log-to=/tmp/tlapm_lsp.log"] } } }, @@ -426,6 +448,7 @@ "@vscode/codicons": "^0.0.33", "@vscode/debugadapter": "^1.59.0", "@vscode/webview-ui-toolkit": "^1.2.2", + "vscode-languageclient": "=9.0.0", "await-notify": "^1.0.1", "moment": "^2.29.4", "react": "^18.2.0", diff --git a/src/main.ts b/src/main.ts index a3dab9ef..ef1432b7 100644 --- a/src/main.ts +++ b/src/main.ts @@ -1,3 +1,4 @@ +// cSpell:words tlaplus tlaps sany checkndebug evaluatable import * as vscode from 'vscode'; import * as path from 'path'; import { @@ -25,6 +26,7 @@ import { CfgCompletionItemProvider } from './completions/cfgCompletions'; import { TlaDeclarationsProvider, TlaDefinitionsProvider } from './declarations/tlaDeclarations'; import { TlaDocumentInfos } from './model/documentInfo'; import { syncTlcStatisticsSetting, listenTlcStatConfigurationChanges } from './commands/tlcStatisticsCfg'; +import { TlapsClient } from './tlaps'; const TLAPLUS_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS }; const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS_CFG }; @@ -35,10 +37,13 @@ const tlaDocInfos = new TlaDocumentInfos(); // Holds all the error messages let diagnostic: vscode.DiagnosticCollection; +let tlapsClient: TlapsClient | undefined; + /** * Extension entry point. */ export function activate(context: vscode.ExtensionContext): void { + console.log('TODO: activated (TLA+)'); diagnostic = vscode.languages.createDiagnosticCollection(LANG_TLAPLUS); context.subscriptions.push( vscode.commands.registerCommand( @@ -154,6 +159,7 @@ export function activate(context: vscode.ExtensionContext): void { } }) ); + tlapsClient = new TlapsClient(context); syncTlcStatisticsSetting() .catch((err) => console.error(err)) .then(() => listenTlcStatConfigurationChanges(context.subscriptions)); @@ -161,6 +167,13 @@ export function activate(context: vscode.ExtensionContext): void { .catch((err) => console.error(err)); } +export function deactivate() { + if (tlapsClient) { + tlapsClient.deactivate(); + } + tlapsClient = undefined; +} + async function showChangeLog(extPath: string) { const pkgData = await readFile(`${extPath}${path.sep}package.json`); const curVersion = JSON.parse(pkgData).version; diff --git a/src/tlaps.ts b/src/tlaps.ts new file mode 100644 index 00000000..3d7323e5 --- /dev/null +++ b/src/tlaps.ts @@ -0,0 +1,109 @@ +// cSpell:words tlaplus tlaps tlapm +import * as vscode from 'vscode'; +import { + Executable, + LanguageClient, + LanguageClientOptions, + TransportKind, + VersionedTextDocumentIdentifier +} from 'vscode-languageclient/node'; + +export class TlapsClient { + private client: LanguageClient | undefined; + private configEnabled = false; + private configCommand = [] as string[]; + + constructor(context: vscode.ExtensionContext) { + context.subscriptions.push(vscode.commands.registerTextEditorCommand( + 'tlaplus.tlaps.check-step', + (te, ed, args) => { + if (!this.client) { + return; + } + vscode.commands.executeCommand('tlaplus.tlaps.check-step.lsp', + { + uri: te.document.uri.toString(), + version: te.document.version + } as VersionedTextDocumentIdentifier, + { + start: te.selection.start, + end: te.selection.end + } as vscode.Range, + ); + } + )); + context.subscriptions.push(vscode.workspace.onDidChangeConfiguration(event => { + if (this.readConfig()) { + this.tryStop(); + this.tryStart(); + } + })); + this.readConfig(); + this.tryStart(); + } + + public deactivate() { + this.tryStop(); + } + + private readConfig(): boolean { + const config = vscode.workspace.getConfiguration(); + const configEnabled = config.get('tlaplus.tlaps.enabled'); + const configCommand = config.get('tlaplus.tlaps.lspServerCommand'); + const configChanged = + configEnabled !== this.configEnabled || + JSON.stringify(configCommand) !== JSON.stringify(this.configCommand); + if (configChanged) { + console.log('TLAPS config changed, enabled=', configEnabled, 'command=', configCommand); + } + this.configEnabled = !!configEnabled; + this.configCommand = configCommand ? configCommand : []; + return configChanged; + } + + private tryStart() { + console.log('TODO: TLAPS LSP -- 1'); + if (this.client) { + return; // Already started. + } + console.log('TODO: TLAPS LSP -- 2'); + if (!this.configEnabled) { + return; + } + console.log('TODO: TLAPS LSP -- 3'); + const lspServerCommand = this.configCommand; + if (!lspServerCommand || lspServerCommand.length === 0) { + return; + } + const command = lspServerCommand[0]; + const cmdArgs = lspServerCommand.slice(1); + console.log('TODO: TLAPS LSP -- 4'); + const serverOptions: Executable = { + command: command, + transport: TransportKind.stdio, + args: cmdArgs + }; + const clientOptions: LanguageClientOptions = { + documentSelector: [{ scheme: 'file', language: 'tlaplus' }], + }; + this.client = new LanguageClient( + 'tlaplus.tlaps.lsp', + 'TLA+ Proof System', + serverOptions, + clientOptions, + true, + ); + this.client.start(); + console.log('TLAPS LSP server started.'); + } + + private tryStop() { + const client = this.client; + this.client = undefined; + if (!client) { + return undefined; + } + console.log('TLAPS LSP server is going to stop.'); + return client.stop(); + } +}