Fix bug with dublication of the output channel

Built-in output channel in vscode was used for logging events of the CoqLSP used inside. Output channels were created for each CoqLSP instance. Now it's fixed.
JetBrains-Research · Sep 30, 2024 · 66d2d36 · 66d2d36
1 parent 363e210
commit 66d2d36
Show file tree

Hide file tree

Showing 6 changed files with 39 additions and 8 deletions.
diff --git a/src/coqLsp/coqLspClient.ts b/src/coqLsp/coqLspClient.ts
@@ -1,5 +1,6 @@
 import { Mutex } from "async-mutex";
 import { readFileSync } from "fs";
+import { OutputChannel } from "vscode";
 import {
     BaseLanguageClient,
     Diagnostic,
@@ -76,9 +77,14 @@ export class CoqLspClient implements CoqLspClientInterface {
 
     static async create(
         serverConfig: CoqLspServerConfig,
-        clientConfig: CoqLspClientConfig
+        clientConfig: CoqLspClientConfig,
+        logOutputChannel: OutputChannel
     ): Promise<CoqLspClient> {
-        const connector = new CoqLspConnector(serverConfig, clientConfig);
+        const connector = new CoqLspConnector(
+            serverConfig,
+            clientConfig,
+            logOutputChannel
+        );
         await connector.start().catch((error) => {
             throw new CoqLspStartupError(
                 `failed to start coq-lsp with Error: ${error.message}`,

diff --git a/src/coqLsp/coqLspConnector.ts b/src/coqLsp/coqLspConnector.ts
@@ -1,4 +1,4 @@
-import { Uri } from "vscode";
+import { OutputChannel, Uri } from "vscode";
 import {
     LanguageClientOptions,
     RevealOutputChannelOn,
@@ -14,14 +14,16 @@ export class CoqLspConnector extends LanguageClient {
     constructor(
         serverConfig: CoqLspServerConfig,
         clientConfig: CoqLspClientConfig,
+        public logOutputChannel: OutputChannel,
         private eventLogger?: EventLogger
     ) {
         let clientOptions: LanguageClientOptions = {
             documentSelector: [
                 { scheme: "file", language: "coq" },
                 { scheme: "file", language: "markdown", pattern: "**/*.mv" },
             ],
-            outputChannelName: "CoqPilot: coq-lsp events",
+            outputChannel: logOutputChannel,
+            // outputChannelName: "CoqPilot: coq-lsp events",
             revealOutputChannelOn: RevealOutputChannelOn.Info,
             initializationOptions: serverConfig,
             markdown: { isTrusted: true, supportHtml: true },

diff --git a/src/extension/coqPilot.ts b/src/extension/coqPilot.ts
@@ -278,7 +278,8 @@ export class CoqPilot {
             CoqLspConfig.createClientConfig(coqLspServerPath);
         const client = await CoqLspClient.create(
             coqLspServerConfig,
-            coqLspClientConfig
+            coqLspClientConfig,
+            this.globalExtensionState.logOutputChannel
         );
         const contextTheoremsRanker = buildTheoremsRankerFromConfig();
 

diff --git a/src/extension/globalExtensionState.ts b/src/extension/globalExtensionState.ts
@@ -1,7 +1,7 @@
 import * as fs from "fs";
 import * as path from "path";
 import * as tmp from "tmp";
-import { WorkspaceConfiguration, workspace } from "vscode";
+import { WorkspaceConfiguration, window, workspace } from "vscode";
 
 import { LLMServices, disposeServices } from "../llm/llmServices";
 import { GrazieService } from "../llm/llmServices/grazie/grazieService";
@@ -20,6 +20,9 @@ export class GlobalExtensionState {
         this.eventLogger,
         this.parseLoggingVerbosity(workspace.getConfiguration(pluginId))
     );
+    public readonly logOutputChannel = window.createOutputChannel(
+        "CoqPilot: coq-lsp events"
+    );
 
     public readonly llmServicesLogsDir = path.join(
         tmp.dirSync().name,
@@ -65,5 +68,6 @@ export class GlobalExtensionState {
         disposeServices(this.llmServices);
         this.logWriter.dispose();
         fs.rmSync(this.llmServicesLogsDir, { recursive: true, force: true });
+        this.logOutputChannel.dispose();
     }
 }
diff --git a/src/test/benchmark/benchmarkingFramework.ts b/src/test/benchmark/benchmarkingFramework.ts
@@ -1,5 +1,6 @@
 import * as assert from "assert";
 import * as fs from "fs";
+import { window } from "vscode";
 
 import { LLMServices } from "../../llm/llmServices";
 import { GrazieService } from "../../llm/llmServices/grazie/grazieService";
@@ -425,7 +426,15 @@ async function createCoqLspClient(
         process.env.COQ_LSP_PATH || "coq-lsp",
         workspaceRootPath
     );
-    return await CoqLspClient.create(coqLspServerConfig, coqLspClientConfig);
+    const logOutputChannel = window.createOutputChannel(
+        "CoqPilot: coq-lsp events"
+    );
+
+    return await CoqLspClient.create(
+        coqLspServerConfig,
+        coqLspClientConfig,
+        logOutputChannel
+    );
 }
 
 async function extractCompletionTargets(

diff --git a/src/test/commonTestFunctions/coqLspBuilder.ts b/src/test/commonTestFunctions/coqLspBuilder.ts
@@ -1,3 +1,5 @@
+import { window } from "vscode";
+
 import { CoqLspClient } from "../../coqLsp/coqLspClient";
 import { CoqLspConfig } from "../../coqLsp/coqLspConfig";
 
@@ -9,6 +11,13 @@ export async function createCoqLspClient(
         process.env.COQ_LSP_PATH || "coq-lsp",
         workspaceRootPath
     );
+    const logOutputChannel = window.createOutputChannel(
+        "CoqPilot: coq-lsp events"
+    );
 
-    return await CoqLspClient.create(coqLspServerConfig, coqLspClientConfig);
+    return await CoqLspClient.create(
+        coqLspServerConfig,
+        coqLspClientConfig,
+        logOutputChannel
+    );
 }