From 66d2d3633051ebd737a5390f4434bc1a9661ed08 Mon Sep 17 00:00:00 2001
From: Andrei Kozyrev <kozyrev.andreiii2016@gmail.com>
Date: Mon, 30 Sep 2024 17:24:01 +0300
Subject: [PATCH] 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.
---
src/coqLsp/coqLspClient.ts | 10 ++++++++--
src/coqLsp/coqLspConnector.ts | 6 ++++--
src/extension/coqPilot.ts | 3 ++-
src/extension/globalExtensionState.ts | 6 +++++-
src/test/benchmark/benchmarkingFramework.ts | 11 ++++++++++-
src/test/commonTestFunctions/coqLspBuilder.ts | 11 ++++++++++-
6 files changed, 39 insertions(+), 8 deletions(-)
diff --git a/src/coqLsp/coqLspClient.ts b/src/coqLsp/coqLspClient.ts
index 5a85f5f1..bba4ebe7 100644
--- 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
index 61e6ce8c..f2f0e383 100644
--- 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,6 +14,7 @@ export class CoqLspConnector extends LanguageClient {
constructor(
serverConfig: CoqLspServerConfig,
clientConfig: CoqLspClientConfig,
+ public logOutputChannel: OutputChannel,
private eventLogger?: EventLogger
) {
let clientOptions: LanguageClientOptions = {
@@ -21,7 +22,8 @@ export class CoqLspConnector extends LanguageClient {
{ 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
index c529d787..3df239ae 100644
--- 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
index a41931fd..b1640a5b 100644
--- 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
index 47234564..3c889399 100644
--- 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
index 7fca359e..5d845da6 100644
--- 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
+ );
}