Initial support for TLAPS.

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",

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,13 +159,21 @@ export function activate(context: vscode.ExtensionContext): void {
                 }
             })
     );
+    tlapsClient = new TlapsClient(context);
     syncTlcStatisticsSetting()
         .catch((err) => console.error(err))
         .then(() => listenTlcStatConfigurationChanges(context.subscriptions));
     showChangeLog(context.extensionPath)
         .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;

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<boolean>('tlaplus.tlaps.enabled');
+        const configCommand = config.get<string[]>('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();
+    }
+}