From 16ebbce302dc0a81e5c717e81525a36179825571 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sat, 3 Feb 2024 17:33:31 +0200 Subject: [PATCH 1/2] Module search paths can be shared between tools. Signed-off-by: Karolis Petrauskas --- package.json | 11 +++ src/main.ts | 8 ++ src/model/paths.ts | 7 ++ .../moduleSearchPathsTreeDataProvider.ts | 60 +++++++++++++ src/paths.ts | 85 +++++++++++++++++++ src/tla2tools.ts | 21 ++++- src/tlaps.ts | 23 +++++ 7 files changed, 213 insertions(+), 2 deletions(-) create mode 100644 src/model/paths.ts create mode 100644 src/panels/moduleSearchPathsTreeDataProvider.ts create mode 100644 src/paths.ts diff --git a/package.json b/package.json index 7697342..012b77a 100644 --- a/package.json +++ b/package.json @@ -401,6 +401,12 @@ "type": "boolean", "default": true, "description": "Mark proof step states using whole line." + }, + "tlaplus.moduleSearchPaths": { + "type": "array", + "items": {"type": "string"}, + "description": "Paths to look for TLA+ modules.", + "default": [] } } }, @@ -489,6 +495,11 @@ "id": "tlaplus.current-proof-step", "name": "Current Proof Step", "type": "webview" + }, + { + "id": "tlaplus.module-search-paths", + "name": "Module Search Paths", + "type": "tree" } ] } diff --git a/src/main.ts b/src/main.ts index 6f23258..1dc3e4c 100644 --- a/src/main.ts +++ b/src/main.ts @@ -28,6 +28,8 @@ import { TlaDocumentInfos } from './model/documentInfo'; import { syncTlcStatisticsSetting, listenTlcStatConfigurationChanges } from './commands/tlcStatisticsCfg'; import { TlapsClient } from './tlaps'; import { CurrentProofStepWebviewViewProvider } from './panels/currentProofStepWebviewViewProvider'; +import { moduleSearchPaths } from './paths'; +import { ModuleSearchPathsTreeDataProvider } from './panels/moduleSearchPathsTreeDataProvider'; const TLAPLUS_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS }; const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS_CFG }; @@ -44,6 +46,8 @@ let tlapsClient: TlapsClient | undefined; * Extension entry point. */ export function activate(context: vscode.ExtensionContext): void { + moduleSearchPaths.setup(context); + const currentProofStepWebviewViewProvider = new CurrentProofStepWebviewViewProvider(context.extensionUri); diagnostic = vscode.languages.createDiagnosticCollection(LANG_TLAPLUS); context.subscriptions.push( @@ -167,6 +171,10 @@ export function activate(context: vscode.ExtensionContext): void { vscode.window.registerWebviewViewProvider( CurrentProofStepWebviewViewProvider.viewType, currentProofStepWebviewViewProvider, + ), + vscode.window.registerTreeDataProvider( + ModuleSearchPathsTreeDataProvider.viewType, + new ModuleSearchPathsTreeDataProvider(context) ) ); tlapsClient = new TlapsClient(context, details => { diff --git a/src/model/paths.ts b/src/model/paths.ts new file mode 100644 index 0000000..8e26b1b --- /dev/null +++ b/src/model/paths.ts @@ -0,0 +1,7 @@ +export interface InitRequestInItializationOptions { + moduleSearchPaths: string[] | null | undefined +} + +export interface InitResponseCapabilitiesExperimental { + moduleSearchPaths: string[] | null | undefined +} diff --git a/src/panels/moduleSearchPathsTreeDataProvider.ts b/src/panels/moduleSearchPathsTreeDataProvider.ts new file mode 100644 index 0000000..f69b993 --- /dev/null +++ b/src/panels/moduleSearchPathsTreeDataProvider.ts @@ -0,0 +1,60 @@ +import * as vscode from 'vscode'; +import { moduleSearchPaths, ModuleSearchPathSource } from '../paths'; + +const sourceIcon = new vscode.ThemeIcon('folder-library'); +const zipDirIcon = new vscode.ThemeIcon('file-zip'); +const folderIcon = new vscode.ThemeIcon('folder'); + +class mspSource extends vscode.TreeItem { + level = 'source'; + constructor( + public source: ModuleSearchPathSource + ) { + super(source.description, vscode.TreeItemCollapsibleState.Expanded); + } + iconPath = sourceIcon; +} + +class mspPath extends vscode.TreeItem { + level = 'path'; + constructor( + path: string + ) { + super(path, vscode.TreeItemCollapsibleState.None); + this.iconPath = path.startsWith('jar://') ? zipDirIcon : folderIcon; + } +} + +type msp = mspSource | mspPath + +export class ModuleSearchPathsTreeDataProvider implements vscode.TreeDataProvider { + static readonly viewType = 'tlaplus.module-search-paths'; + private _onDidChangeTreeData = new vscode.EventEmitter(); + readonly onDidChangeTreeData = this._onDidChangeTreeData.event; + + constructor( + private context: vscode.ExtensionContext + ) { + context.subscriptions.push(moduleSearchPaths.updates(_ => { + this._onDidChangeTreeData.fire(); + })); + } + + getChildren(element?: msp): Thenable { + if (!element) { + return Promise.resolve( + moduleSearchPaths.getSources().map(s => new mspSource(s)) + ); + } + if (element.level === 'source') { + return Promise.resolve( + moduleSearchPaths.getSourcePaths((element as mspSource).source.name).map(p => new mspPath(p)) + ); + } + return Promise.resolve([]); + } + + getTreeItem(element: msp): vscode.TreeItem { + return element; + } +} diff --git a/src/paths.ts b/src/paths.ts new file mode 100644 index 0000000..21ec92e --- /dev/null +++ b/src/paths.ts @@ -0,0 +1,85 @@ +import * as vscode from 'vscode'; +import * as tla2tools from './tla2tools'; + +export const TLAPS = 'TLAPS'; +export const TLC = 'TLC'; +export const CFG = 'CFG'; + +export interface ModuleSearchPathSource { + name: string; + description: string; +} + +class ModuleSearchPaths { + private priority = [CFG, TLC, TLAPS]; + private sources: { [source: string]: string } = {}; + private paths: { [source: string]: string[] } = {}; + + private _updates = new vscode.EventEmitter(); + readonly updates = this._updates.event; + + public setup(context: vscode.ExtensionContext) { + this.setSourcePaths(TLC, 'TLC Model Checker', tla2tools.moduleSearchPaths()); + const fromCfg = () => { + const config = vscode.workspace.getConfiguration(); + const cfgPaths = config.get('tlaplus.moduleSearchPaths'); + this.setSourcePaths(CFG, 'Configured Paths', cfgPaths ? cfgPaths : []); + }; + context.subscriptions.push(vscode.workspace.onDidChangeConfiguration((e: vscode.ConfigurationChangeEvent) => { + if (e.affectsConfiguration('tlaplus.moduleSearchPaths')) { + fromCfg(); + vscode.commands.executeCommand( + 'tlaplus.tlaps.moduleSearchPaths.updated.lsp', + ...this.getOtherPaths(TLAPS) + ); + } + })); + fromCfg(); + } + + // Order first by the defined priority, then all the remaining alphabetically, just to be predictable. + private sourceOrder(): string[] { + const sourceNames = Object.keys(this.sources); + const ordered: string[] = []; + this.priority.forEach(sn => { + if (sourceNames.includes(sn)) { + ordered.push(sn); + } + }); + const other = sourceNames.filter(sn => !this.priority.includes(sn)); + other.sort(); + ordered.push(...other); + return ordered; + } + + public getSources(): ModuleSearchPathSource[] { + return this.sourceOrder().map(sn => { + return { + name: sn, + description: this.sources[sn] + }; + }); + } + + public getSourcePaths(source: string): string[] { + return this.paths[source]; + } + + // Return all the paths except the specified source. + public getOtherPaths(source: string): string[] { + return this.sourceOrder().reduce((acc, s) => { + if (s !== source) { + acc.push(... this.paths[s]); + } + return acc; + }, []); + } + + public setSourcePaths(source: string, description: string, paths: string[]) { + this.sources[source] = description; + this.paths[source] = paths; + this._updates.fire(); + } +} + +export const moduleSearchPaths = new ModuleSearchPaths(); diff --git a/src/tla2tools.ts b/src/tla2tools.ts index cdfd9ff..fb27ac5 100644 --- a/src/tla2tools.ts +++ b/src/tla2tools.ts @@ -2,6 +2,7 @@ import * as cp from 'child_process'; import { ChildProcess, spawn } from 'child_process'; import * as fs from 'fs'; import * as path from 'path'; +import * as paths from './paths'; import * as vscode from 'vscode'; import { CFG_TLC_STATISTICS_TYPE, ShareOption } from './commands/tlcStatisticsCfg'; import { pathToUri } from './common'; @@ -30,6 +31,7 @@ const TLA_TOOLS_LIB_NAME_END_WIN = '\\' + TLA_TOOLS_LIB_NAME; const toolsJarPath = path.resolve(__dirname, '../tools/' + TLA_TOOLS_LIB_NAME); const javaCmd = 'java' + (process.platform === 'win32' ? '.exe' : ''); const javaVersionChannel = new ToolOutputChannel('TLA+ Java version'); +const TLA_TOOLS_STANDARD_MODULES = '/tla2sany/StandardModules'; let lastUsedJavaHome: string | undefined; let cachedJavaPath: string | undefined; @@ -69,6 +71,14 @@ export class JavaVersion { ) {} } +function makeTlaLibraryJavaOpt(): string { + const libPaths = paths.moduleSearchPaths. + getOtherPaths(paths.TLC). + filter(p => !p.startsWith('jar:')). // TODO: Support archive paths as well. + join(path.delimiter); + return '-DTLA-Library=' + libPaths; +} + export async function runPlusCal(tlaFilePath: string): Promise { const customOptions = getConfigOptions(CFG_PLUSCAL_OPTIONS); return runTool( @@ -84,7 +94,7 @@ export async function runSany(tlaFilePath: string): Promise { TlaTool.SANY, tlaFilePath, [ path.basename(tlaFilePath) ], - [] + [ makeTlaLibraryJavaOpt() ] ); } @@ -116,7 +126,7 @@ export async function runTlc( return undefined; } const customOptions = extraOpts.concat(promptedOptions); - const javaOptions = []; + const javaOptions = [ makeTlaLibraryJavaOpt() ]; const shareStats = vscode.workspace.getConfiguration().get(CFG_TLC_STATISTICS_TYPE); if (shareStats !== ShareOption.DoNotShare) { javaOptions.push('-Dtlc2.TLC.ide=vscode'); @@ -136,6 +146,7 @@ async function runTool( javaOptions: string[] ): Promise { const javaPath = await obtainJavaPath(); + // TODO: Merge cfgOptions with javaOptions to avoid complete overrides. const cfgOptions = getConfigOptions(CFG_JAVA_OPTIONS); const args = buildJavaOptions(cfgOptions, toolsJarPath).concat(javaOptions); args.push(toolName); @@ -145,6 +156,12 @@ async function runTool( return new ToolProcessInfo(buildCommandLine(javaPath, args), proc); } +export function moduleSearchPaths(): string[] { + return [ + 'jar:file:' + toolsJarPath + '!' + TLA_TOOLS_STANDARD_MODULES + ]; +} + /** * Kills the given process. */ diff --git a/src/tlaps.ts b/src/tlaps.ts index 5b40759..b5d4b23 100644 --- a/src/tlaps.ts +++ b/src/tlaps.ts @@ -15,12 +15,19 @@ import { LanguageClient, LanguageClientOptions, Range, + State, + StateChangeEvent, TextDocumentIdentifier, TransportKind, VersionedTextDocumentIdentifier } from 'vscode-languageclient/node'; import { TlapsProofStepDetails } from './model/tlaps'; import { DelayedFn } from './common'; +import { + InitRequestInItializationOptions, + InitResponseCapabilitiesExperimental, +} from './model/paths'; +import { moduleSearchPaths, TLAPS } from './paths'; export enum proofStateNames { proved = 'proved', @@ -186,6 +193,9 @@ export class TlapsClient { }; const clientOptions: LanguageClientOptions = { documentSelector: [{ scheme: 'file', language: 'tlaplus' }], + initializationOptions: { + moduleSearchPaths: moduleSearchPaths.getOtherPaths(TLAPS) + } as InitRequestInItializationOptions }; this.client = new LanguageClient( 'tlaplus.tlaps.lsp', @@ -202,6 +212,19 @@ export class TlapsClient { 'tlaplus/tlaps/currentProofStep', this.currentProofStepDetailsListener )); + this.context.subscriptions.push(this.client.onDidChangeState((e: StateChangeEvent) => { + if (e.oldState !== State.Running && e.newState === State.Running && this.client) { + const initResult = this.client.initializeResult; + if (!initResult || !initResult.capabilities.experimental) { + return; + } + const experimental = initResult.capabilities.experimental as InitResponseCapabilitiesExperimental; + if (!experimental.moduleSearchPaths) { + return; + } + moduleSearchPaths.setSourcePaths(TLAPS, 'TLA Proof System', experimental.moduleSearchPaths); + } + })); this.client.start(); } From 5e032cf00f92083b7a7a2bb960f4134497119bf3 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sat, 3 Feb 2024 22:10:15 +0200 Subject: [PATCH 2/2] Add community modules to the paths supplied by TLC. Signed-off-by: Karolis Petrauskas --- src/tla2tools.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tla2tools.ts b/src/tla2tools.ts index fb27ac5..28005f8 100644 --- a/src/tla2tools.ts +++ b/src/tla2tools.ts @@ -25,10 +25,12 @@ const NO_ERROR = 0; const MIN_TLA_ERROR = 10; // Exit codes not related to tooling start from this number const LOWEST_JAVA_VERSION = 8; const DEFAULT_GC_OPTION = '-XX:+UseParallelGC'; +const TLA_CMODS_LIB_NAME = 'CommunityModules-deps.jar'; const TLA_TOOLS_LIB_NAME = 'tla2tools.jar'; const TLA_TOOLS_LIB_NAME_END_UNIX = '/' + TLA_TOOLS_LIB_NAME; const TLA_TOOLS_LIB_NAME_END_WIN = '\\' + TLA_TOOLS_LIB_NAME; const toolsJarPath = path.resolve(__dirname, '../tools/' + TLA_TOOLS_LIB_NAME); +const cmodsJarPath = path.resolve(__dirname, '../tools/' + TLA_CMODS_LIB_NAME); const javaCmd = 'java' + (process.platform === 'win32' ? '.exe' : ''); const javaVersionChannel = new ToolOutputChannel('TLA+ Java version'); const TLA_TOOLS_STANDARD_MODULES = '/tla2sany/StandardModules'; @@ -158,7 +160,8 @@ async function runTool( export function moduleSearchPaths(): string[] { return [ - 'jar:file:' + toolsJarPath + '!' + TLA_TOOLS_STANDARD_MODULES + 'jar:file:' + toolsJarPath + '!' + TLA_TOOLS_STANDARD_MODULES, + 'jar:file:' + cmodsJarPath + '!' + '/' ]; }