Module search paths can be shared between tools.

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"
                 }
             ]
         }

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 => {

src/model/paths.ts

@@ -0,0 +1,7 @@
+export interface InitRequestInItializationOptions {
+    moduleSearchPaths: string[] | null | undefined
+}
+
+export interface InitResponseCapabilitiesExperimental {
+    moduleSearchPaths: string[] | null | undefined
+}

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<msp> {
+    static readonly viewType = 'tlaplus.module-search-paths';
+    private _onDidChangeTreeData = new vscode.EventEmitter<msp | msp[] | undefined | null | void>();
+    readonly onDidChangeTreeData = this._onDidChangeTreeData.event;
+
+    constructor(
+        private context: vscode.ExtensionContext
+    ) {
+        context.subscriptions.push(moduleSearchPaths.updates(_ => {
+            this._onDidChangeTreeData.fire();
+        }));
+    }
+
+    getChildren(element?: msp): Thenable<msp[]> {
+        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;
+    }
+}

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<void>();
+    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<string[]>('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<ModuleSearchPathSource>(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<string[]>((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();

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';
@@ -24,12 +25,15 @@ 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';
 
 let lastUsedJavaHome: string | undefined;
 let cachedJavaPath: string | undefined;
@@ -69,6 +73,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<ToolProcessInfo> {
     const customOptions = getConfigOptions(CFG_PLUSCAL_OPTIONS);
     return runTool(
@@ -84,7 +96,7 @@ export async function runSany(tlaFilePath: string): Promise<ToolProcessInfo> {
         TlaTool.SANY,
         tlaFilePath,
         [ path.basename(tlaFilePath) ],
-        []
+        [ makeTlaLibraryJavaOpt() ]
     );
 }
 
@@ -116,7 +128,7 @@ export async function runTlc(
         return undefined;
     }
     const customOptions = extraOpts.concat(promptedOptions);
-    const javaOptions = [];
+    const javaOptions = [ makeTlaLibraryJavaOpt() ];
     const shareStats = vscode.workspace.getConfiguration().get<ShareOption>(CFG_TLC_STATISTICS_TYPE);
     if (shareStats !== ShareOption.DoNotShare) {
         javaOptions.push('-Dtlc2.TLC.ide=vscode');
@@ -136,6 +148,7 @@ async function runTool(
     javaOptions: string[]
 ): Promise<ToolProcessInfo> {
     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 +158,13 @@ async function runTool(
     return new ToolProcessInfo(buildCommandLine(javaPath, args), proc);
 }
 
+export function moduleSearchPaths(): string[] {
+    return [
+        'jar:file:' + toolsJarPath + '!' + TLA_TOOLS_STANDARD_MODULES,
+        'jar:file:' + cmodsJarPath + '!' + '/'
+    ];
+}
+
 /**
  * Kills the given process.
  */

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();
     }