Release v2.4.2+0.2.2+8.19

Merge pull request #53 from JetBrains-Research/v2.5.0-dev

Author: K-dizzled

CHANGELOG.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## 2.4.2
+
+- Fix premise selection bug in benchmarks: in `v2.4.1`, a theorem for which the completion was issued was accidentally added to the list of premises. This was fixed in this release.
+We encountered difficulty setting the correct `coq-lsp` path in the settings, both for the `coq-lsp` plugin itself and for `coqpilot`. When using the `nix` environment, it is common for the path to be updated by hand, and it is not always done correctly. Therefore, we added a warning message to the user, which is shown when `coqpilot` suspects that the build of `coq-lsp` on the given path is not the expected one.
+
 ## 2.4.1
 
 Hot fix with update of dependencies to fix the issue on extension activation.

README.md

@@ -1,4 +1,4 @@
-# CoqPilot ![Version](https://img.shields.io/badge/version-v2.4.1-blue?style=flat-square)
+# CoqPilot ![Version](https://img.shields.io/badge/version-v2.4.2-blue?style=flat-square)
 
 *Authors:* Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev, [Programming Languages and Tools Lab](https://lp.jetbrains.com/research/plt_lab/) at JetBrains Research.
 

package-lock.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/JetBrains-Research/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "2.4.1",
+  "version": "2.4.2",
   "engines": {
     "vscode": "^1.95.0"
   },

package.json

@@ -51,6 +51,7 @@ export async function executeBenchmarkingTask(
     try {
         const generationArgs = {
             completionContext: task.getCompletionContext(),
+            sourceTheorem: task.sourceTheorem,
             sourceFileEnvironment: task.getSourceFileEnvironment(),
             benchmarkingModelParams: params,
             llmService: llmService,

src/benchmark/framework/benchmarkingCore/executeBenchmarkingTask.ts

@@ -44,6 +44,7 @@ import {
 } from "../../structures/benchmarkingResults/benchmarkedItem";
 import { WorkspaceRoot } from "../../structures/common/workspaceRoot";
 import { ParsedCoqFileData } from "../../structures/parsedCoqFile/parsedCoqFileData";
+import { TheoremData } from "../../structures/parsedCoqFile/theoremData";
 import { throwOnAbort } from "../../utils/asyncUtils/abortUtils";
 import { AsyncScheduler } from "../../utils/asyncUtils/asyncScheduler";
 import { reduceToMap } from "../../utils/collectionUtils/mapUtils";
@@ -65,6 +66,7 @@ export interface CompletionGenerationBenchmarkArgs<
     LLMServiceType extends LLMService<any, ResolvedModelParams>,
 > {
     completionContext: CompletionContext;
+    sourceTheorem: TheoremData;
     sourceFileEnvironment: SourceFileEnvironment;
     benchmarkingModelParams: BenchmarkingModelParams<ResolvedModelParams>;
     llmService: LLMServiceType;
@@ -242,6 +244,7 @@ async function generateProofWithRetriesExclusively<
         () =>
             generateProofWithRetriesMeasured(
                 generationArgs.completionContext,
+                generationArgs.sourceTheorem.name,
                 generationArgs.sourceFileEnvironment,
                 generationArgs.benchmarkingModelParams,
                 generationArgs.llmService,
@@ -258,6 +261,7 @@ async function generateProofWithRetriesMeasured<
     ResolvedModelParams extends ModelParams,
 >(
     completionContext: CompletionContext,
+    sourceTheoremName: string,
     sourceFileEnvironment: SourceFileEnvironment,
     benchmarkingModelParams: BenchmarkingModelParams<ResolvedModelParams>,
     llmService: LLMService<any, any>,
@@ -286,6 +290,7 @@ async function generateProofWithRetriesMeasured<
     const proofGenerationContext = buildProofGenerationContext(
         completionContext,
         sourceFileEnvironment.fileTheorems,
+        sourceTheoremName,
         benchmarkingModelParams.theoremRanker
     );
 
@@ -395,14 +400,24 @@ async function generateProofWithRetriesMeasured<
     }
 }
 
+/**
+ * _Important:_ this function is the one responsbile for **removing
+ * the target theorem from the context** (i.e. file theorems) if it is present there.
+ */
 function buildProofGenerationContext(
     completionContext: CompletionContext,
     fileTheorems: Theorem[],
+    targetTheoremName: string,
     theoremRanker?: ContextTheoremsRanker
 ): ProofGenerationContext {
+    const contextTheorems = fileTheorems.filter(
+        (theorem) => theorem.name !== targetTheoremName
+    );
     const rankedTheorems =
-        theoremRanker?.rankContextTheorems(fileTheorems, completionContext) ??
-        fileTheorems;
+        theoremRanker?.rankContextTheorems(
+            contextTheorems,
+            completionContext
+        ) ?? fileTheorems;
     return {
         contextTheorems: rankedTheorems,
         completionTarget: goalToTargetLemma(completionContext.proofGoal),

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/benchmarkSingleCompletionGeneration.ts

@@ -108,6 +108,7 @@ export abstract class AbstractExperiment {
         );
     }
 
+    // TODO: support absolute `artifactsDirPath`
     /**
      * The core method that executes the benchmarking experiment.
      *
@@ -280,10 +281,21 @@ export abstract class AbstractExperiment {
         optionsAfterStartupResolution: ExperimentRunOptions.AfterStartupResolution,
         requestedWorkspaces: string[]
     ): ExperimentRunOptions {
+        // So far `coqLspServerPath` is applied to the benchmarking system
+        // by storing it into `process.env.COQ_LSP_PATH`.
+        // TODO: pass it through the system explicitly (!)
+        const customCoqLspServerPath =
+            optionsAfterStartupResolution.coqLspServerPath;
+        if (customCoqLspServerPath !== undefined) {
+            process.env.COQ_LSP_PATH = customCoqLspServerPath;
+        }
+
         return {
             loggerSeverity: optionsAfterStartupResolution.loggerSeverity,
             logsFilePath: optionsAfterStartupResolution.logsFilePath,
 
+            coqLspServerPath: undefined, // TODO: is passed through `process.env.COQ_LSP_PATH` above
+
             datasetCacheUsage: optionsAfterStartupResolution.datasetCacheUsage,
             datasetCacheDirectoryPath:
                 optionsAfterStartupResolution.datasetCacheDirectoryPath,

src/benchmark/framework/experiment/abstractExperiment.ts

@@ -11,6 +11,17 @@ export interface ExperimentRunOptions extends BenchmarkingOptions {
      */
     logsFilePath: string | undefined;
 
+    /**
+     * Path to the coq-lsp server. Currently, it **must be set up properly**;
+     * otherwise, proof checking always suceeds even for the invalid proofs.
+     *
+     * Notes on the coq-lsp server path resolution.
+     * - If `coqLspServerPath` is set, it will be used.
+     * - Otherwise, the one stored in the `COQ_LSP_PATH` environment variable will be selected.
+     * - Finally, if none of them are set, coq-lsp will search for the server path automatically.
+     */
+    coqLspServerPath: string | undefined;
+
     datasetCacheUsage: DatasetCacheUsageMode;
     /**
      * Path relative to the root directory. If it is not set, a `dataset/.parsingCache` will be used.

src/benchmark/framework/structures/inputParameters/experimentRunOptions.ts

@@ -14,6 +14,7 @@ import {
     Position,
     ProtocolNotificationType,
     PublishDiagnosticsNotification,
+    PublishDiagnosticsParams,
     RequestType,
     TextDocumentIdentifier,
     VersionedTextDocumentIdentifier,
@@ -111,6 +112,7 @@ export class CoqLspClientImpl implements CoqLspClient {
         public readonly abortSignal?: AbortSignal
     ) {
         this.client = coqLspConnector;
+        this.trackSuspiciousLspErrors();
     }
 
     static async create(
@@ -123,7 +125,8 @@ export class CoqLspClientImpl implements CoqLspClient {
         const connector = new CoqLspConnector(
             serverConfig,
             clientConfig,
-            logOutputChannel
+            logOutputChannel,
+            eventLogger
         );
         await connector.start().catch((error) => {
             throw new CoqLspStartupError(
@@ -242,6 +245,49 @@ export class CoqLspClientImpl implements CoqLspClient {
             .trim();
     }
 
+    trackSuspiciousLspErrors() {
+        this.client.onNotification(
+            PublishDiagnosticsNotification.type,
+            (params: PublishDiagnosticsParams) => {
+                function filterIncorrectLspSuspectedDiagnostics(
+                    diagnostic: Diagnostic
+                ): boolean {
+                    const errorSubstrings = [
+                        "Cannot find a physical path bound to logical path",
+                        "Dynlink error: error loading shared library",
+                    ];
+
+                    return errorSubstrings.some(
+                        (substr) =>
+                            diagnostic.message.includes(substr) &&
+                            diagnostic.severity === 1
+                    );
+                }
+
+                const suspectedDiagnostics = params.diagnostics.filter(
+                    filterIncorrectLspSuspectedDiagnostics
+                );
+                if (suspectedDiagnostics.length > 0) {
+                    const data = {
+                        uri: params.uri.toString(),
+                        version: params.version,
+                        diagnosticMessage: suspectedDiagnostics.map(
+                            (d) => d.message
+                        ),
+                    };
+                    const firstErrorMessage =
+                        suspectedDiagnostics[0].message.split("\n")[0];
+
+                    this.eventLogger?.log(
+                        CoqLspConnector.wrongServerSuspectedEvent,
+                        firstErrorMessage,
+                        data
+                    );
+                }
+            }
+        );
+    }
+
     filterDiagnostics(
         diagnostics: Diagnostic[],
         position: Position

src/coqLsp/coqLspClient.ts

@@ -11,6 +11,8 @@ import { EventLogger } from "../logging/eventLogger";
 import { CoqLspClientConfig, CoqLspServerConfig } from "./coqLspConfig";
 
 export class CoqLspConnector extends LanguageClient {
+    static wrongServerSuspectedEvent = "wrong-lsp-server-suspected";
+
     constructor(
         serverConfig: CoqLspServerConfig,
         clientConfig: CoqLspClientConfig,
@@ -63,20 +65,27 @@ export class CoqLspConnector extends LanguageClient {
         super.setTrace(Trace.Verbose);
         await super
             .start()
-            .then(this.logStatusUpdate.bind(this, "started"))
+            .then()
             .catch((error) => {
                 let emsg = error.toString();
                 this.eventLogger?.log("coq-lsp-start-error", emsg);
-                this.logStatusUpdate("stopped");
                 throw error;
             });
     }
 
-    override async stop(): Promise<void> {
-        super.stop().then(this.logStatusUpdate.bind(this, "stopped"));
+    private isVersioningError(message: string): boolean {
+        return message.includes("Incorrect client version");
     }
 
-    private logStatusUpdate = (status: "started" | "stopped") => {
-        this.eventLogger?.log("coq-lsp-status-change", status);
-    };
+    override error(message: string, data: any, showNotification = true) {
+        if (this.isVersioningError(message)) {
+            this.eventLogger?.log(
+                CoqLspConnector.wrongServerSuspectedEvent,
+                message
+            );
+        } else {
+            this.eventLogger?.log("coq-lsp-error", message);
+        }
+        super.error(message, data, showNotification);
+    }
 }