Merge pull request #48 from JetBrains-Research/proof-checking-refacto…

…r-fix

Fix-ups for "significant proof checking refactoring"

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

@@ -162,7 +162,8 @@ export async function benchmarkSingleCompletionGeneration<
             generationArgs.completionContext,
             generationArgs.sourceFileEnvironment,
             generationArgs.workspaceRoot,
-            logger
+            logger,
+            abortSignal
         );
     } catch (error) {
         if (error instanceof ProofsCheckFailedError) {

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/abstractProofsChecker.ts

@@ -29,6 +29,7 @@ export abstract class AbstractProofsChecker {
         completionContext: CompletionContext,
         sourceFileEnvironment: SourceFileEnvironment,
         workspaceRoot: WorkspaceRoot,
-        logger: BenchmarkingLogger
+        logger: BenchmarkingLogger,
+        abortSignal?: AbortSignal
     ): Promise<ProofsCheckResult>;
 }

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts

@@ -1,4 +1,4 @@
-import { createTestCoqLspClient } from "../../../../../../coqLsp/coqLspBuilders";
+import { withDocumentOpenedByTestCoqLsp } from "../../../../../../coqLsp/coqLspBuilders";
 import { CoqLspTimeoutError } from "../../../../../../coqLsp/coqLspTypes";
 
 import {
@@ -7,8 +7,8 @@ import {
 } from "../../../../../../core/coqProofChecker";
 
 import { stringifyAnyValue } from "../../../../../../utils/printers";
-import { Uri } from "../../../../../../utils/uri";
 import { BenchmarkingLogger } from "../../../../logging/benchmarkingLogger";
+import { deserializeUri } from "../../../../structures/common/serializedUri";
 import { LogsIPCSender } from "../../../../utils/subprocessUtils/ipc/onParentProcessCallExecutor/logsIpcSender";
 import { TimeMark } from "../../measureUtils";
 
@@ -28,31 +28,29 @@ export namespace CheckProofsImpl {
 
     export async function checkProofsMeasured(
         args: Signature.Args,
-        providedLogger: ProvidedLogger
+        providedLogger: ProvidedLogger,
+        abortSignal?: AbortSignal
     ): Promise<Signature.Result> {
-        const coqLspClient = await createTestCoqLspClient(
-            args.workspaceRootPath
-        );
-        const coqProofChecker = new CoqProofChecker(coqLspClient);
-        // TODO: each coq proof checker should use its own prefix to work good in parallel (many checkers for the same theorem in the same file)
+        const fileUri = deserializeUri(args.serializedFileUri);
+        const timeMark = new TimeMark();
 
         try {
-            const timeMark = new TimeMark();
-            const fileUri = Uri.fromPath(args.fileUri);
-
-            // TODO: [@Gleb Solovev] Pay Atteniton that it was previously done by the CoqProofChecker
-            await coqLspClient.openTextDocument(fileUri);
-
-            const proofCheckResults = await coqProofChecker.checkProofs(
-                fileUri,
-                args.documentVersion,
-                args.checkAtPosition,
-                args.preparedProofs
+            const proofCheckResults = await withDocumentOpenedByTestCoqLsp(
+                { uri: fileUri, version: args.documentVersion },
+                {
+                    workspaceRootPath: args.workspaceRootPath,
+                    abortSignal: abortSignal,
+                },
+                (coqLspClient) =>
+                    new CoqProofChecker(coqLspClient).checkProofs(
+                        fileUri,
+                        args.documentVersion,
+                        args.positionToCheckAt,
+                        args.preparedProofs
+                    )
             );
-
-            await coqLspClient.closeTextDocument(fileUri);
-
             const proofsValidationMillis = timeMark.measureElapsedMillis();
+
             return buildSuccessResult(
                 proofCheckResults,
                 proofsValidationMillis,

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts

@@ -2,15 +2,16 @@ import { JSONSchemaType } from "ajv";
 
 import { ProofCheckResult } from "../../../../../../core/coqProofChecker";
 
+import { SerializedUri } from "../../../../structures/common/serializedUri";
+
 export namespace CheckProofsInternalSignature {
     export const subprocessName = "Check generated proofs";
 
     export interface Args {
         workspaceRootPath: string | undefined;
-        fileUri: string;
+        serializedFileUri: SerializedUri;
         documentVersion: number;
-        checkAtPosition: Position;
-
+        positionToCheckAt: Position;
         preparedProofs: string[];
     }
 
@@ -80,21 +81,26 @@ export namespace CheckProofsInternalSignature {
                 type: "string",
                 nullable: true,
             },
-            fileUri: {
+            serializedFileUri: {
                 type: "string",
             },
             documentVersion: {
                 type: "number",
             },
-            checkAtPosition: positionSchema,
+            positionToCheckAt: positionSchema,
             preparedProofs: {
                 type: "array",
                 items: {
                     type: "string",
                 },
             },
         },
-        required: ["fileUri", "documentVersion", "preparedProofs"],
+        required: [
+            "serializedFileUri",
+            "documentVersion",
+            "positionToCheckAt",
+            "preparedProofs",
+        ],
         additionalProperties: false,
     };
 

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts

@@ -3,6 +3,7 @@ import {
     SourceFileEnvironment,
 } from "../../../../../../core/completionGenerationContext";
 
+import { serializeUri } from "../../../../structures/common/serializedUri";
 import {
     WorkspaceRoot,
     isStandaloneFilesRoot,
@@ -27,9 +28,9 @@ export namespace ProofsCheckerUtils {
             workspaceRootPath: isStandaloneFilesRoot(workspaceRoot)
                 ? undefined
                 : workspaceRoot.directoryPath,
-            fileUri: sourceFileEnvironment.fileUri.toString(),
+            serializedFileUri: serializeUri(sourceFileEnvironment.fileUri),
             documentVersion: sourceFileEnvironment.documentVersion,
-            checkAtPosition: completionContext.admitRange.start,
+            positionToCheckAt: completionContext.admitRange.start,
             preparedProofs: preparedProofs,
         };
     }

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/localProofsChecker.ts

@@ -23,7 +23,8 @@ export class LocalProofsChecker extends AbstractProofsChecker {
         completionContext: CompletionContext,
         sourceFileEnvironment: SourceFileEnvironment,
         workspaceRoot: WorkspaceRoot,
-        logger: BenchmarkingLogger
+        logger: BenchmarkingLogger,
+        abortSignal: AbortSignal
     ): Promise<ProofsCheckResult> {
         const args = ProofsCheckerUtils.buildArgs(
             preparedProofs,
@@ -36,7 +37,8 @@ export class LocalProofsChecker extends AbstractProofsChecker {
             {
                 logger: logger,
                 logSuccess: false,
-            }
+            },
+            abortSignal
         );
         return ProofsCheckerUtils.unpackSuccessResultOrThrow(proofsCheckResult);
     }

src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts

@@ -79,7 +79,7 @@ namespace UpdateCacheHolders {
 
         if (cachedFile.getDocumentVersion() !== parsedFile.documentVersion) {
             cacheUpdaterLogger.debug(
-                `* file version update: ${cachedFile.getDocumentVersion()} -> ${parsedFile.documentVersion}`
+                `* document version update: ${cachedFile.getDocumentVersion()} -> ${parsedFile.documentVersion}`
             );
         }
         cachedFile.updateDocumentVersion(parsedFile.documentVersion);

src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts

@@ -1,8 +1,10 @@
-import { createTestCoqLspClient } from "../../../../../coqLsp/coqLspBuilders";
+import { withTestCoqLspClient } from "../../../../../coqLsp/coqLspBuilders";
 import { CoqLspClient } from "../../../../../coqLsp/coqLspClient";
+import { CoqLspError } from "../../../../../coqLsp/coqLspTypes";
 
 import { createSourceFileEnvironment } from "../../../../../core/inspectSourceFile";
 
+import { asErrorOrRethrow } from "../../../../../utils/errorsUtils";
 import { Uri } from "../../../../../utils/uri";
 import { BenchmarkingLogger } from "../../../logging/benchmarkingLogger";
 import { TargetType } from "../../../structures/benchmarkingCore/completionGenerationTask";
@@ -40,49 +42,70 @@ export namespace ParseCoqProjectImpl {
         args: Signature.ArgsModels.Args,
         logger: Logger
     ): Promise<Signature.ResultModels.Result> {
-        const coqLspClient = await createTestCoqLspClient(
-            args.workspaceRootPath
-        );
         const parsedWorkspace: Signature.ResultModels.Result = {};
-        for (const filePath in args.workspaceTargets) {
-            const fileTargets = args.workspaceTargets[filePath];
-            const serializedParsedFile = await openAndParseSourceFile(
-                filePath,
-                coqLspClient,
-                logger
-            );
-            const parsedFileResults: Signature.ResultModels.ParsedFileResults =
-                {
-                    serializedParsedFile: serializedParsedFile,
-                    parsedFileTargets: await extractFileTargetsFromFile(
-                        fileTargets,
-                        serializedParsedFile,
-                        coqLspClient,
-                        logger
-                    ),
-                };
-            parsedWorkspace[filePath] = parsedFileResults;
-        }
+
+        // Note: specific abort controller is not passed here, since
+        // the abort behaviour is not supported (and not needed) at the parsing stage.
+        await withTestCoqLspClient(
+            { workspaceRootPath: args.workspaceRootPath },
+            async (coqLspClient) => {
+                for (const filePath in args.workspaceTargets) {
+                    parsedWorkspace[filePath] =
+                        await coqLspClient.withTextDocument(
+                            { uri: Uri.fromPath(filePath) },
+                            () =>
+                                parseFileTargets(
+                                    args.workspaceTargets[filePath],
+                                    filePath,
+                                    coqLspClient,
+                                    logger
+                                )
+                        );
+                }
+            }
+        );
+
         logger.debug(
             `Successfully parsed Coq project: analyzed ${Object.keys(parsedWorkspace).length} files`
         );
         return parsedWorkspace;
     }
 
-    async function openAndParseSourceFile(
+    async function parseFileTargets(
+        fileTargets: Signature.ArgsModels.FileTarget[],
+        filePath: string,
+        coqLspClient: CoqLspClient,
+        logger: Logger
+    ): Promise<Signature.ResultModels.ParsedFileResults> {
+        const serializedParsedFile = await parseSourceFile(
+            filePath,
+            coqLspClient,
+            logger
+        );
+        return {
+            serializedParsedFile: serializedParsedFile,
+            parsedFileTargets: await extractFileTargetsFromFile(
+                fileTargets,
+                serializedParsedFile,
+                coqLspClient,
+                logger
+            ),
+        };
+    }
+
+    async function parseSourceFile(
         filePath: string,
         coqLspClient: CoqLspClient,
         logger: Logger
     ): Promise<SerializedParsedCoqFile> {
         const mockDocumentVersion = 1;
-        const sourceFileUri = Uri.fromPath(filePath);
-        await coqLspClient.openTextDocument(sourceFileUri);
         // TODO: [@Gleb Solovev] Do not create this Abort Controller but pass
         // the one created at the top
+        // TODO + check coq-lsp creation in benchmarks
         const abortController = new AbortController();
         const sourceFileEnvironment = await createSourceFileEnvironment(
             mockDocumentVersion,
-            sourceFileUri,
+            Uri.fromPath(filePath),
             coqLspClient,
             abortController.signal
         );
@@ -163,20 +186,25 @@ export namespace ParseCoqProjectImpl {
             proofStep: SerializedProofStep,
             targetType: TargetType,
             knownGoal: SerializedGoal | undefined
-        ) => Promise<Signature.ResultModels.ParsedFileTarget> = (
+        ) => Promise<Signature.ResultModels.ParsedFileTarget> = async (
             proofStep,
             targetType,
             knownGoal
-        ) =>
-            buildParsedFileTarget(
-                proofStep,
-                targetType,
-                theorem.name,
-                knownGoal,
-                serializedParsedFile,
-                coqLspClient,
-                logger
-            );
+        ) => {
+            return {
+                theoremName: theorem.name,
+                targetType: targetType,
+                goalToProve:
+                    knownGoal ??
+                    (await parseGoal(
+                        proofStep,
+                        serializedParsedFile,
+                        coqLspClient,
+                        logger
+                    )),
+                positionRange: proofStep.range,
+            };
+        };
         switch (requestType) {
             case TargetRequestType.THEOREM_PROOF:
                 // THEOREM_PROOF goals are already parsed within the theorems,
@@ -197,46 +225,33 @@ export namespace ParseCoqProjectImpl {
         }
     }
 
-    async function buildParsedFileTarget(
+    async function parseGoal(
         proofStep: SerializedProofStep,
-        targetType: TargetType,
-        theoremName: string,
-        knownGoal: SerializedGoal | undefined,
         serializedParsedFile: SerializedParsedCoqFile,
         coqLspClient: CoqLspClient,
         logger: Logger
-    ): Promise<Signature.ResultModels.ParsedFileTarget> {
-        let serializedGoal = knownGoal;
-        if (serializedGoal === undefined) {
-            const goals = await coqLspClient.getGoalsAtPoint(
+    ): Promise<SerializedGoal> {
+        const startPosition = deserializeCodeElementPosition(
+            proofStep.range.start
+        );
+        try {
+            const goal = await coqLspClient.getFirstGoalAtPointOrThrow(
                 proofStep.range.start,
                 Uri.fromPath(serializedParsedFile.filePath),
                 serializedParsedFile.documentVersion
             );
-            const startPosition = deserializeCodeElementPosition(
-                proofStep.range.start
+            logger.debug(
+                `Successfully retrieved target goal at point: "${goal.ty}" at ${startPosition}, "${serializedParsedFile.filePath}"`
             );
-            if (goals.err) {
-                const goal = goals.val;
-                const stack = goal.stack === undefined ? "" : `\n${goal.stack}`;
-                logger.error(
-                    `Failed to retrieve target goal at point: "${goal.message}" at ${startPosition}, "${serializedParsedFile.filePath}"${stack}`
-                );
-                throw goal;
-            } else {
-                const goal = coqLspClient.getFirstGoalOrThrow(goals);
-                logger.debug(
-                    `Successfully retrieved target goal at point: "${goal.ty}" at ${startPosition}, "${serializedParsedFile.filePath}"`
-                );
-                serializedGoal = serializeGoal(goal);
-            }
+            return serializeGoal(goal);
+        } catch (err) {
+            const coqLspError = asErrorOrRethrow(err) as CoqLspError;
+            const stack =
+                coqLspError.stack === undefined ? "" : `\n${coqLspError.stack}`;
+            logger.error(
+                `Failed to retrieve target goal at point: "${coqLspError.message}" at ${startPosition}, "${serializedParsedFile.filePath}"${stack}`
+            );
+            throw coqLspError;
         }
-
-        return {
-            theoremName: theoremName,
-            targetType: targetType,
-            goalToProve: serializedGoal,
-            positionRange: proofStep.range,
-        };
     }
 }