diff --git a/dataset/imm b/dataset/imm index 14025d11..16637a92 160000 --- a/dataset/imm +++ b/dataset/imm @@ -1 +1 @@ -Subproject commit 14025d11ee217b5397c544917c5623a80abbd28e +Subproject commit 16637a922a817230ca03e0d2f6b0f961cc7d410a diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/benchmarkSingleCompletionGeneration.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/benchmarkSingleCompletionGeneration.ts index e516a557..b1c7ec68 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/benchmarkSingleCompletionGeneration.ts +++ b/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) { diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/abstractProofsChecker.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/abstractProofsChecker.ts index 792aaab9..75044d25 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/abstractProofsChecker.ts +++ b/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; } diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts index 93606ce4..4590ec79 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts +++ b/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 { - 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, diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts index 92e67a59..835710b6 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts +++ b/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,13 +81,13 @@ export namespace CheckProofsInternalSignature { type: "string", nullable: true, }, - fileUri: { + serializedFileUri: { type: "string", }, documentVersion: { type: "number", }, - checkAtPosition: positionSchema, + positionToCheckAt: positionSchema, preparedProofs: { type: "array", items: { @@ -94,7 +95,12 @@ export namespace CheckProofsInternalSignature { }, }, }, - required: ["fileUri", "documentVersion", "preparedProofs"], + required: [ + "serializedFileUri", + "documentVersion", + "positionToCheckAt", + "preparedProofs", + ], additionalProperties: false, }; diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts index 2af4eb88..6e17faad 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts +++ b/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, }; } diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/localProofsChecker.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/localProofsChecker.ts index 938f46d8..558ad21e 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/localProofsChecker.ts +++ b/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 { const args = ProofsCheckerUtils.buildArgs( preparedProofs, @@ -36,7 +37,8 @@ export class LocalProofsChecker extends AbstractProofsChecker { { logger: logger, logSuccess: false, - } + }, + abortSignal ); return ProofsCheckerUtils.unpackSuccessResultOrThrow(proofsCheckResult); } diff --git a/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts b/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts index 76c9730b..fc1da514 100644 --- a/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts +++ b/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); diff --git a/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts b/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts index 3343edc2..45e532e7 100644 --- a/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts +++ b/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 { - 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 { + 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 { 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 = ( + ) => Promise = 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 { - let serializedGoal = knownGoal; - if (serializedGoal === undefined) { - const goals = await coqLspClient.getGoalsAtPoint( + ): Promise { + 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, - }; } } diff --git a/src/benchmark/framework/structures/common/serializedUri.ts b/src/benchmark/framework/structures/common/serializedUri.ts new file mode 100644 index 00000000..6d0d15cd --- /dev/null +++ b/src/benchmark/framework/structures/common/serializedUri.ts @@ -0,0 +1,11 @@ +import { Uri } from "../../../../utils/uri"; + +export type SerializedUri = string; + +export function serializeUri(uriObject: Uri): SerializedUri { + return uriObject.uri; +} + +export function deserializeUri(serializedUri: SerializedUri): Uri { + return Uri.fromUriString(serializedUri); +} diff --git a/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts b/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts index be01b871..532d8af7 100644 --- a/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts +++ b/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts @@ -109,7 +109,13 @@ export const serializedTheoremSchema: JSONSchemaType = { type: "number", }, }, - required: ["name", "statement_range", "statement", "fileTheoremsIndex"], + required: [ + "name", + "statement_range", + "statement", + "proof", + "fileTheoremsIndex", + ], additionalProperties: false, }; diff --git a/src/benchmark/framework/utils/coqUtils/proofTargetExtractor.ts b/src/benchmark/framework/utils/coqUtils/proofTargetExtractor.ts index 63aa126d..54c4c4ed 100644 --- a/src/benchmark/framework/utils/coqUtils/proofTargetExtractor.ts +++ b/src/benchmark/framework/utils/coqUtils/proofTargetExtractor.ts @@ -8,11 +8,11 @@ import { export function extractTheoremFisrtProofStep( theorem: TheoremData | Theorem ): ProofStep { - return theorem.proof!.proof_steps[1]; + return theorem.proof.proof_steps[1]; } export function extractSerializedTheoremFisrtProofStep( serializedTheorem: SerializedTheorem ): SerializedProofStep { - return serializedTheorem.proof!.proof_steps[1]; + return serializedTheorem.proof.proof_steps[1]; } diff --git a/src/benchmark/framework/utils/inputResolutionUtils/resolveTheoremsRanker.ts b/src/benchmark/framework/utils/inputResolutionUtils/resolveTheoremsRanker.ts index a5ba45f9..c2fa460e 100644 --- a/src/benchmark/framework/utils/inputResolutionUtils/resolveTheoremsRanker.ts +++ b/src/benchmark/framework/utils/inputResolutionUtils/resolveTheoremsRanker.ts @@ -1,7 +1,7 @@ +import { DistanceContextTheoremsRanker } from "../../../../core/contextTheoremRanker/actualRankers/distanceContextTheoremsRanker"; +import { JaccardIndexContextTheoremsRanker } from "../../../../core/contextTheoremRanker/actualRankers/jaccardIndexContextTheoremsRanker"; +import { RandomContextTheoremsRanker } from "../../../../core/contextTheoremRanker/actualRankers/randomContextTheoremsRanker"; import { ContextTheoremsRanker } from "../../../../core/contextTheoremRanker/contextTheoremsRanker"; -import { DistanceContextTheoremsRanker } from "../../../../core/contextTheoremRanker/distanceContextTheoremsRanker"; -import { JaccardIndexContextTheoremsRanker } from "../../../../core/contextTheoremRanker/jaccardIndexContextTheoremsRanker"; -import { RandomContextTheoremsRanker } from "../../../../core/contextTheoremRanker/randomContextTheoremsRanker"; import { RankerType } from "../../structures/inputParameters/inputBenchmarkingModelParams"; diff --git a/src/benchmark/framework/utils/subprocessUtils/ipc/onParentProcessCallExecutor/executeOnParentProcessCall.ts b/src/benchmark/framework/utils/subprocessUtils/ipc/onParentProcessCallExecutor/executeOnParentProcessCall.ts index b55b8b17..05b17c0e 100644 --- a/src/benchmark/framework/utils/subprocessUtils/ipc/onParentProcessCallExecutor/executeOnParentProcessCall.ts +++ b/src/benchmark/framework/utils/subprocessUtils/ipc/onParentProcessCallExecutor/executeOnParentProcessCall.ts @@ -24,7 +24,8 @@ import { OnParentProcessCallExecutorUtils } from "./utils"; import Utils = OnParentProcessCallExecutorUtils; // TODO: document -// TODO: design better logging through actual file +// TODO: design better logging through actual +// TODO: support abort behaviour export async function executeAsFunctionOnParentProcessCall< ArgsType, ResultType, diff --git a/src/coqLsp/coqLspBuilders.ts b/src/coqLsp/coqLspBuilders.ts index 934e18ad..20026058 100644 --- a/src/coqLsp/coqLspBuilders.ts +++ b/src/coqLsp/coqLspBuilders.ts @@ -2,30 +2,70 @@ import { OutputChannel, window } from "vscode"; import { EventLogger } from "../logging/eventLogger"; -import { CoqLspClient, CoqLspClientImpl } from "./coqLspClient"; +import { + CoqLspClient, + CoqLspClientImpl, + DiagnosticMessage, + DocumentSpec, +} from "./coqLspClient"; import { CoqLspClientConfig, CoqLspConfig } from "./coqLspConfig"; export async function createCoqLspClient( coqLspServerPath: string, logOutputChannel?: OutputChannel, eventLogger?: EventLogger, - abortController?: AbortController + abortSignal?: AbortSignal ): Promise { return createAbstractCoqLspClient( CoqLspConfig.createClientConfig(coqLspServerPath), logOutputChannel, eventLogger, - abortController + abortSignal ); } +export interface TestCoqLspClientOptions { + workspaceRootPath?: string; + abortSignal?: AbortSignal; +} + export async function createTestCoqLspClient( - workspaceRootPath?: string + options: TestCoqLspClientOptions = {} ): Promise { return createAbstractCoqLspClient( CoqLspConfig.createClientConfig( process.env.COQ_LSP_PATH || "coq-lsp", - workspaceRootPath + options.workspaceRootPath + ), + undefined, + undefined, + options.abortSignal + ); +} + +export async function withTestCoqLspClient( + options: TestCoqLspClientOptions, + block: (coqLspClient: CoqLspClient) => Promise +) { + const coqLspClient = await createTestCoqLspClient(options); + try { + return await block(coqLspClient); + } finally { + coqLspClient.dispose(); + } +} + +export async function withDocumentOpenedByTestCoqLsp( + documentSpec: DocumentSpec, + options: TestCoqLspClientOptions, + block: ( + coqLspClient: CoqLspClient, + openedDocDiagnostic: DiagnosticMessage + ) => Promise +): Promise { + return withTestCoqLspClient(options, (coqLspClient) => + coqLspClient.withTextDocument(documentSpec, (openedDocDiagnostic) => + block(coqLspClient, openedDocDiagnostic) ) ); } @@ -36,7 +76,7 @@ async function createAbstractCoqLspClient( "CoqPilot: coq-lsp events" ), eventLogger?: EventLogger, - abortController?: AbortController + abortSignal?: AbortSignal ): Promise { const coqLspServerConfig = CoqLspConfig.createServerConfig(); return await CoqLspClientImpl.create( @@ -44,6 +84,6 @@ async function createAbstractCoqLspClient( coqLspClientConfig, logOutputChannel, eventLogger, - abortController + abortSignal ); } diff --git a/src/coqLsp/coqLspClient.ts b/src/coqLsp/coqLspClient.ts index 6bf7b16f..5e361b61 100644 --- a/src/coqLsp/coqLspClient.ts +++ b/src/coqLsp/coqLspClient.ts @@ -19,7 +19,8 @@ import { VersionedTextDocumentIdentifier, } from "vscode-languageclient"; -import { throwOnAbort } from "../extension/extensionAbortUtils"; +import { throwOnAbort } from "../core/abortUtils"; + import { EventLogger } from "../logging/eventLogger"; import { Uri } from "../utils/uri"; @@ -30,12 +31,17 @@ import { CoqLspStartupError, FlecheDocument, FlecheDocumentParams, - Goal, GoalAnswer, GoalRequest, PpString, + ProofGoal, } from "./coqLspTypes"; +export interface DocumentSpec { + uri: Uri; + version?: number; +} + export interface CoqLspClient extends Disposable { /** * Fetches all goals present at the given position in the document. @@ -52,7 +58,18 @@ export interface CoqLspClient extends Disposable { documentUri: Uri, version: number, command?: string - ): Promise[], Error>>; + ): Promise>; + + /** + * The wrapper for the `getGoalsAtPoint` method returning only the first goal of the extracted ones. + * If the goals extraction is not successfull, this method will throw a `CoqLspError`. + */ + getFirstGoalAtPointOrThrow( + position: Position, + documentUri: Uri, + version: number, + command?: string + ): Promise; /** * Returns a FlecheDocument for the given uri. @@ -65,11 +82,10 @@ export interface CoqLspClient extends Disposable { closeTextDocument(uri: Uri): Promise; - /** - * - * @param goals - */ - getFirstGoalOrThrow(goals: Result[], Error>): Goal; + withTextDocument( + documentSpec: DocumentSpec, + block: (openedDocDiagnostic: DiagnosticMessage) => Promise + ): Promise; } const goalReqType = new RequestType, void>( @@ -92,7 +108,7 @@ export class CoqLspClientImpl implements CoqLspClient { private constructor( coqLspConnector: CoqLspConnector, public readonly eventLogger?: EventLogger, - public readonly abortController?: AbortController + public readonly abortSignal?: AbortSignal ) { this.client = coqLspConnector; } @@ -102,7 +118,7 @@ export class CoqLspClientImpl implements CoqLspClient { clientConfig: CoqLspClientConfig, logOutputChannel: OutputChannel, eventLogger?: EventLogger, - abortController?: AbortController + abortSignal?: AbortSignal ): Promise { const connector = new CoqLspConnector( serverConfig, @@ -115,7 +131,7 @@ export class CoqLspClientImpl implements CoqLspClient { clientConfig.coq_lsp_server_path ); }); - return new CoqLspClientImpl(connector, eventLogger, abortController); + return new CoqLspClientImpl(connector, eventLogger, abortSignal); } async getGoalsAtPoint( @@ -123,9 +139,9 @@ export class CoqLspClientImpl implements CoqLspClient { documentUri: Uri, version: number, command?: string - ): Promise[], Error>> { + ): Promise> { return await this.mutex.runExclusive(async () => { - throwOnAbort(this.abortController?.signal); + throwOnAbort(this.abortSignal); return this.getGoalsAtPointUnsafe( position, documentUri, @@ -135,46 +151,72 @@ export class CoqLspClientImpl implements CoqLspClient { }); } + async getFirstGoalAtPointOrThrow( + position: Position, + documentUri: Uri, + version: number, + command?: string + ): Promise { + return await this.mutex.runExclusive(async () => { + throwOnAbort(this.abortSignal); + const goals = await this.getGoalsAtPointUnsafe( + position, + documentUri, + version, + command + ); + if (goals.err) { + throw goals.val; + } else if (goals.val.length === 0) { + throw new CoqLspError( + `Failed to get the first goal: list of goals is empty at the position ${position} of ${documentUri.fsPath}` + ); + } + return goals.val[0]; + }); + } + async openTextDocument( uri: Uri, version: number = 1 ): Promise { return await this.mutex.runExclusive(async () => { - throwOnAbort(this.abortController?.signal); + throwOnAbort(this.abortSignal); return this.openTextDocumentUnsafe(uri, version); }); } async closeTextDocument(uri: Uri): Promise { return await this.mutex.runExclusive(async () => { - throwOnAbort(this.abortController?.signal); + throwOnAbort(this.abortSignal); return this.closeTextDocumentUnsafe(uri); }); } + async withTextDocument( + documentSpec: DocumentSpec, + block: (openedDocDiagnostic: DiagnosticMessage) => Promise + ): Promise { + const diagnostic = await this.openTextDocument( + documentSpec.uri, + documentSpec.version + ); + // TODO: discuss whether coq-lsp is capable of maintaining several docs opened + // or we need a common lock for open-close here + try { + return await block(diagnostic); + } finally { + await this.closeTextDocument(documentSpec.uri); + } + } + async getFlecheDocument(uri: Uri): Promise { return await this.mutex.runExclusive(async () => { - throwOnAbort(this.abortController?.signal); + throwOnAbort(this.abortSignal); return this.getFlecheDocumentUnsafe(uri); }); } - getFirstGoalOrThrow( - goals: Result[], Error> - ): Goal { - if (goals.err) { - throw new CoqLspError( - "Call to `getFirstGoalOrThrow` with a Error type" - ); - } else if (goals.val.length === 0) { - throw new CoqLspError( - "Call to `getFirstGoalOrThrow` with an empty set of goals" - ); - } - - return goals.val[0]; - } - /** * Dirty due to the fact that the client sends no pure * error: https://github.com/ejgallego/coq-lsp/blob/f98b65344c961d1aad1e0c3785199258f21c3abc/controller/request.ml#L29 @@ -221,7 +263,7 @@ export class CoqLspClientImpl implements CoqLspClient { documentUri: Uri, version: number, command?: string - ): Promise[], Error>> { + ): Promise> { let goalRequestParams: GoalRequest = { textDocument: VersionedTextDocumentIdentifier.create( documentUri.uri, @@ -382,6 +424,15 @@ export class CoqLspClientImpl implements CoqLspClient { return doc; } + /** + * _Implementation note:_ although this `dispose` implementation calls an async method, + * we are not tend to await it, as well as `CoqLspClient.dispose()` in general. + * + * Since different coq-lsp clients correspond to different processes, + * they don't have any shared resources; therefore, a new client can be started without + * waiting for the previous one to finish. Thus, we don't await for this `dispose()` call + * to finish, the client and its process will be disposed at some point asynchronously. + */ dispose(): void { this.subscriptions.forEach((d) => d.dispose()); this.client.stop(); diff --git a/src/coqParser/parseCoqFile.ts b/src/coqParser/parseCoqFile.ts index d306139b..8ea4f3db 100644 --- a/src/coqParser/parseCoqFile.ts +++ b/src/coqParser/parseCoqFile.ts @@ -1,18 +1,18 @@ import { readFileSync } from "fs"; -import { Result } from "ts-results"; import { Position, Range } from "vscode-languageclient"; import { CoqLspClient } from "../coqLsp/coqLspClient"; import { CoqParsingError, FlecheDocument, - Goal, - PpString, + ProofGoal, RangedSpan, } from "../coqLsp/coqLspTypes"; -import { throwOnAbort } from "../extension/extensionAbortUtils"; +import { throwOnAbort } from "../core/abortUtils"; + import { EventLogger } from "../logging/eventLogger"; +import { asErrorOrRethrow } from "../utils/errorsUtils"; import { Uri } from "../utils/uri"; import { ProofStep, Theorem, TheoremProof, Vernacexpr } from "./parsedTypes"; @@ -109,18 +109,18 @@ async function parseFlecheDocument( } else { // TODO: Cover with tests, might be a source of bugs if somewhere // absense of initialGoal is not handled properly or invariants are broken - let initialGoal: Result[], Error> | null = - null; + let initialGoal: ProofGoal | null = null; if (extractTheoremInitialGoal) { - initialGoal = await client.getGoalsAtPoint( - doc.spans[i + 1].range.start, - uri, - 1 - ); - - if (initialGoal.err) { + try { + initialGoal = + await client.getFirstGoalAtPointOrThrow( + doc.spans[i + 1].range.start, + uri, + 1 + ); + } catch (err) { throw new CoqParsingError( - `unable to get initial goal for theorem: ${thrName}` + `Unable to get initial goal for theorem: ${thrName}\nCause: ${asErrorOrRethrow(err).message}` ); } } @@ -132,7 +132,7 @@ async function parseFlecheDocument( doc.spans[i].range, thrStatement, proof, - initialGoal?.val[0] + initialGoal ) ); } diff --git a/src/coqParser/parsedTypes.ts b/src/coqParser/parsedTypes.ts index 530aa504..dbdc7706 100644 --- a/src/coqParser/parsedTypes.ts +++ b/src/coqParser/parsedTypes.ts @@ -1,7 +1,7 @@ /* eslint-disable @typescript-eslint/naming-convention */ import { Range } from "vscode-languageclient"; -import { Goal, PpString } from "../coqLsp/coqLspTypes"; +import { ProofGoal } from "../coqLsp/coqLspTypes"; export enum Vernacexpr { VernacLoad = "VernacLoad", @@ -99,25 +99,25 @@ export enum Vernacexpr { export class ProofStep { constructor( - public text: string, - public vernac_type: Vernacexpr, - public range: Range + readonly text: string, + readonly vernac_type: Vernacexpr, + readonly range: Range ) {} - public toString(): string { + toString(): string { return this.text; } } export class TheoremProof { constructor( - public proof_steps: ProofStep[], - public end_pos: Range, - public is_incomplete: boolean, - public holes: ProofStep[] + readonly proof_steps: ProofStep[], + readonly end_pos: Range, + readonly is_incomplete: boolean, + readonly holes: ProofStep[] ) {} - public toString(): string { + toString(): string { let text = ""; for (const step of this.proof_steps) { text += @@ -127,7 +127,7 @@ export class TheoremProof { return text; } - public onlyText(): string { + onlyText(): string { let text = ""; for (const step of this.proof_steps) { text += @@ -140,20 +140,20 @@ export class TheoremProof { export class Theorem { constructor( - public name: string, - public statement_range: Range, - public statement: string, - public proof: TheoremProof, - public initial_goal: Goal | null = null + readonly name: string, + readonly statement_range: Range, + readonly statement: string, + readonly proof: TheoremProof, + readonly initial_goal: ProofGoal | null = null ) {} - public toString(): string { + toString(): string { let text = this.statement; text += "\n" + this.proof.toString(); return text; } - public onlyText(): string { + onlyText(): string { let text = this.statement; text += "\n" + this.proof.onlyText(); return text; diff --git a/src/extension/extensionAbortUtils.ts b/src/core/abortUtils.ts similarity index 82% rename from src/extension/extensionAbortUtils.ts rename to src/core/abortUtils.ts index 27486216..2f4bf503 100644 --- a/src/extension/extensionAbortUtils.ts +++ b/src/core/abortUtils.ts @@ -1,6 +1,6 @@ export class CompletionAbortError extends Error { private static readonly abortMessage = - "User has triggered a session abort: Stopping all completions"; + "Session abort has been triggered: stopping all completions"; constructor() { super(CompletionAbortError.abortMessage); diff --git a/src/core/completionGenerator.ts b/src/core/completionGenerator.ts index 2574262c..f1fb00e6 100644 --- a/src/core/completionGenerator.ts +++ b/src/core/completionGenerator.ts @@ -3,14 +3,11 @@ import { GeneratedProof } from "../llm/llmServices/generatedProof"; import { CoqLspTimeoutError } from "../coqLsp/coqLspTypes"; -import { - CompletionAbortError, - throwOnAbort, -} from "../extension/extensionAbortUtils"; import { EventLogger } from "../logging/eventLogger"; import { asErrorOrRethrow, buildErrorCompleteLog } from "../utils/errorsUtils"; import { stringifyAnyValue } from "../utils/printers"; +import { CompletionAbortError, throwOnAbort } from "./abortUtils"; import { CompletionContext, ProcessEnvironment, @@ -44,6 +41,10 @@ export enum FailureGenerationStatus { SEARCH_FAILED, } +/** + * _Implementation note:_ when this method is called, the target file is expected to be opened by the user. + * Therefore, no explicit `coqLspClient.openTextDocument(...)` call is made. + */ export async function generateCompletion( completionContext: CompletionContext, sourceFileEnvironment: SourceFileEnvironment, diff --git a/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts b/src/core/contextTheoremRanker/actualRankers/distanceContextTheoremsRanker.ts similarity index 85% rename from src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts rename to src/core/contextTheoremRanker/actualRankers/distanceContextTheoremsRanker.ts index b48d52f4..b305688b 100644 --- a/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/actualRankers/distanceContextTheoremsRanker.ts @@ -1,7 +1,6 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; export class DistanceContextTheoremsRanker implements ContextTheoremsRanker { readonly needsUnwrappedNotations = false; diff --git a/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts b/src/core/contextTheoremRanker/actualRankers/euclidContextTheoremRanker.ts similarity index 85% rename from src/core/contextTheoremRanker/euclidContextTheoremRanker.ts rename to src/core/contextTheoremRanker/actualRankers/euclidContextTheoremRanker.ts index 0be8058d..25380017 100644 --- a/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts +++ b/src/core/contextTheoremRanker/actualRankers/euclidContextTheoremRanker.ts @@ -1,8 +1,7 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; -import { goalAsTheoremString } from "./tokenUtils"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; +import { goalAsTheoremString } from "../utils/tokenUtils"; /** * Ranks theorems based on how similar their statements are to diff --git a/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts b/src/core/contextTheoremRanker/actualRankers/jaccardIndexContextTheoremsRanker.ts similarity index 85% rename from src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts rename to src/core/contextTheoremRanker/actualRankers/jaccardIndexContextTheoremsRanker.ts index 389bf6ca..3af0fd38 100644 --- a/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/actualRankers/jaccardIndexContextTheoremsRanker.ts @@ -1,8 +1,7 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; -import { goalAsTheoremString } from "./tokenUtils"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; +import { goalAsTheoremString } from "../utils/tokenUtils"; /** * Ranks theorems based on how similar their statements are to diff --git a/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts b/src/core/contextTheoremRanker/actualRankers/randomContextTheoremsRanker.ts similarity index 75% rename from src/core/contextTheoremRanker/randomContextTheoremsRanker.ts rename to src/core/contextTheoremRanker/actualRankers/randomContextTheoremsRanker.ts index 97b90c31..1220f432 100644 --- a/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/actualRankers/randomContextTheoremsRanker.ts @@ -1,7 +1,6 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; export class RandomContextTheoremsRanker implements ContextTheoremsRanker { readonly needsUnwrappedNotations = false; diff --git a/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts b/src/core/contextTheoremRanker/actualRankers/weightedJaccardIndexTheoremRanker.ts similarity index 90% rename from src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts rename to src/core/contextTheoremRanker/actualRankers/weightedJaccardIndexTheoremRanker.ts index 03db43dd..7ddeac66 100644 --- a/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts +++ b/src/core/contextTheoremRanker/actualRankers/weightedJaccardIndexTheoremRanker.ts @@ -1,8 +1,7 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; -import { goalAsTheoremString } from "./tokenUtils"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; +import { goalAsTheoremString } from "../utils/tokenUtils"; /** * Ranks theorems based on how similar their statements are to diff --git "a/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" "b/src/core/contextTheoremRanker/actualRankers/\321\201osineContextTheoremRanker.ts" similarity index 85% rename from "src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" rename to "src/core/contextTheoremRanker/actualRankers/\321\201osineContextTheoremRanker.ts" index cd31d402..27a95160 100644 --- "a/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" +++ "b/src/core/contextTheoremRanker/actualRankers/\321\201osineContextTheoremRanker.ts" @@ -1,8 +1,7 @@ -import { Theorem } from "../../coqParser/parsedTypes"; -import { CompletionContext } from "../completionGenerationContext"; - -import { ContextTheoremsRanker } from "./contextTheoremsRanker"; -import { goalAsTheoremString } from "./tokenUtils"; +import { Theorem } from "../../../coqParser/parsedTypes"; +import { CompletionContext } from "../../completionGenerationContext"; +import { ContextTheoremsRanker } from "../contextTheoremsRanker"; +import { goalAsTheoremString } from "../utils/tokenUtils"; /** * Ranks theorems based on how similar their statements are to diff --git a/src/core/contextTheoremRanker/contextTheoremsRanker.ts b/src/core/contextTheoremRanker/contextTheoremsRanker.ts index 821448c1..8127cb0e 100644 --- a/src/core/contextTheoremRanker/contextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/contextTheoremsRanker.ts @@ -7,5 +7,9 @@ export interface ContextTheoremsRanker { completionContext: CompletionContext ): Theorem[]; + /** + * _Note:_ so far it only triggers initial goals of all parsed theorems + * being extracted at the parsing stage too. + */ needsUnwrappedNotations: boolean; } diff --git a/src/core/contextTheoremRanker/tokenUtils.ts b/src/core/contextTheoremRanker/utils/tokenUtils.ts similarity index 51% rename from src/core/contextTheoremRanker/tokenUtils.ts rename to src/core/contextTheoremRanker/utils/tokenUtils.ts index 7eee502a..ee7488a2 100644 --- a/src/core/contextTheoremRanker/tokenUtils.ts +++ b/src/core/contextTheoremRanker/utils/tokenUtils.ts @@ -1,8 +1,8 @@ -import { Goal, PpString } from "../../coqLsp/coqLspTypes"; +import { ProofGoal } from "../../../coqLsp/coqLspTypes"; -import { hypToString } from "../exposedCompletionGeneratorUtils"; +import { hypToString } from "../../exposedCompletionGeneratorUtils"; -export function goalAsTheoremString(proofGoal: Goal): string { +export function goalAsTheoremString(proofGoal: ProofGoal): string { const auxTheoremConcl = proofGoal?.ty; const theoremIndeces = proofGoal?.hyps .map((hyp) => `(${hypToString(hyp)})`) diff --git a/src/core/coqProofChecker.ts b/src/core/coqProofChecker.ts index 7774b9a4..f72b7ce3 100644 --- a/src/core/coqProofChecker.ts +++ b/src/core/coqProofChecker.ts @@ -14,19 +14,7 @@ export interface ProofCheckResult { type Proof = string; -export interface CoqProofCheckerInterface { - checkProofs( - fileUri: Uri, - documentVersion: number, - checkAtPosition: Position, - proofs: Proof[], - coqLspTimeoutMillis?: number - ): Promise; - - dispose(): void; -} - -export class CoqProofChecker implements CoqProofCheckerInterface { +export class CoqProofChecker { private mutex: Mutex = new Mutex(); constructor(private coqLspClient: CoqLspClient) {} @@ -34,7 +22,7 @@ export class CoqProofChecker implements CoqProofCheckerInterface { async checkProofs( fileUri: Uri, documentVersion: number, - checkAtPosition: Position, + positionToCheckAt: Position, proofs: Proof[], coqLspTimeoutMillis: number = 15000 ): Promise { @@ -55,7 +43,7 @@ export class CoqProofChecker implements CoqProofCheckerInterface { this.checkProofsUnsafe( fileUri, documentVersion, - checkAtPosition, + positionToCheckAt, proofs ), timeoutPromise, @@ -70,7 +58,7 @@ export class CoqProofChecker implements CoqProofCheckerInterface { private async checkProofsUnsafe( fileUri: Uri, documentVersion: number, - checkAtPosition: Position, + positionToCheckAt: Position, proofs: Proof[] ): Promise { const results: ProofCheckResult[] = []; @@ -84,8 +72,8 @@ export class CoqProofChecker implements CoqProofCheckerInterface { continue; } - const goalResult = await this.coqLspClient.getGoalsAtPoint( - checkAtPosition, + const goalsResult = await this.coqLspClient.getGoalsAtPoint( + positionToCheckAt, fileUri, documentVersion, proof @@ -93,8 +81,10 @@ export class CoqProofChecker implements CoqProofCheckerInterface { results.push({ proof: proof, - isValid: goalResult.ok, - diagnostic: goalResult.err ? goalResult.val.message : undefined, + isValid: goalsResult.ok, + diagnostic: goalsResult.err + ? goalsResult.val.message + : undefined, }); } diff --git a/src/core/inspectSourceFile.ts b/src/core/inspectSourceFile.ts index befd0914..28c38c37 100644 --- a/src/core/inspectSourceFile.ts +++ b/src/core/inspectSourceFile.ts @@ -55,7 +55,7 @@ async function createCompletionContexts( ): Promise { const holesToComplete = fileTheorems .filter((thr) => thr.proof) - .map((thr) => thr.proof!.holes) + .map((thr) => thr.proof.holes) .flat() .filter(shouldCompleteHole); @@ -66,14 +66,11 @@ async function createCompletionContexts( fileUri, documentVersion ); - if (goals.ok) { - const firstGoal = goals.val.shift(); - if (firstGoal) { - completionContexts.push({ - proofGoal: firstGoal, - admitRange: hole.range, - }); - } + if (goals.ok && goals.val.length !== 0) { + completionContexts.push({ + proofGoal: goals.val[0], + admitRange: hole.range, + }); } } diff --git a/src/extension/coqPilot.ts b/src/extension/coqPilot.ts index 10c8ab4e..df8cab4c 100644 --- a/src/extension/coqPilot.ts +++ b/src/extension/coqPilot.ts @@ -7,6 +7,7 @@ import { import { CoqLspStartupError } from "../coqLsp/coqLspTypes"; +import { CompletionAbortError } from "../core/abortUtils"; import { CompletionContext, ProcessEnvironment, @@ -25,40 +26,37 @@ import { ProofStep } from "../coqParser/parsedTypes"; import { buildErrorCompleteLog } from "../utils/errorsUtils"; import { Uri } from "../utils/uri"; +import { PluginContext } from "./pluginContext"; +import { SessionState } from "./sessionState"; import { buildTheoremsRankerFromConfig, readAndValidateUserModelsParams, -} from "./configReaders"; +} from "./settings/configReaders"; +import { SettingsValidationError } from "./settings/settingsValidationError"; import { deleteTextFromRange, highlightTextInEditor, insertCompletion, -} from "./documentEditor"; +} from "./ui/documentEditor"; import { EditorMessages, showMessageToUser, showMessageToUserWithSettingsHint, -} from "./editorMessages"; -import { CompletionAbortError } from "./extensionAbortUtils"; -import { subscribeToHandleLLMServicesEvents } from "./llmServicesEventsHandler"; -import { PluginContext } from "./pluginContext"; -import { PluginStatusIndicator } from "./pluginStatusIndicator"; +} from "./ui/messages/editorMessages"; +import { subscribeToHandleLLMServicesEvents } from "./ui/messages/llmServicesEventsHandler"; +import { PluginStatusIndicator } from "./ui/pluginStatusIndicator"; +import { pluginId } from "./utils/pluginId"; import { positionInRange, toVSCodePosition, toVSCodeRange, -} from "./positionRangeUtils"; -import { SessionState } from "./sessionState"; -import { SettingsValidationError } from "./settingsValidationError"; - -export const pluginId = "coqpilot"; -export const pluginName = "CoqPilot"; +} from "./utils/positionRangeUtils"; export class CoqPilot { private constructor( private readonly vscodeContext: VSCodeContext, private readonly pluginContext: PluginContext, - private sessionState: SessionState, + private readonly sessionState: SessionState, toggleCommand: string ) { this.registerEditorCommand( @@ -74,6 +72,8 @@ export class CoqPilot { this.performCompletionForAllAdmits.bind(this) ); + // TODO: would it be clearer and safer to initialise a new session + // instead of restarting the same object (?) this.registerEditorCommand( toggleCommand, this.sessionState.toggleCurrentSession.bind(this.sessionState) @@ -129,7 +129,7 @@ export class CoqPilot { shouldCompleteHole: (hole: ProofStep) => boolean, editor: TextEditor ) { - if (!this.sessionState.isSessionActive) { + if (!this.sessionState.isActive) { showMessageToUser(EditorMessages.extensionIsPaused, "warning"); return; } @@ -152,8 +152,9 @@ export class CoqPilot { ); } else if (e instanceof CompletionAbortError) { if (!this.sessionState.userNotifiedAboutAbort) { + // TODO: potential race condition causeing notification shown twice + this.sessionState.markAbortNotificationAsShown(); showMessageToUser(EditorMessages.completionAborted, "info"); - this.sessionState.userReceivedAbortNotification(); } } else { showMessageToUser( @@ -309,6 +310,8 @@ export class CoqPilot { const coqProofChecker = new CoqProofChecker( this.sessionState.coqLspClient ); + // Note: here and later the target file is expected to be opened by the user, + // so no explicit `coqLspClient.openTextDocument(...)` call is needed const [completionContexts, sourceFileEnvironment] = await inspectSourceFile( documentVersion, diff --git a/src/extension/pluginContext.ts b/src/extension/pluginContext.ts index 727bcb93..9861edcc 100644 --- a/src/extension/pluginContext.ts +++ b/src/extension/pluginContext.ts @@ -11,8 +11,8 @@ import { PredefinedProofsService } from "../llm/llmServices/predefinedProofs/pre import { EventLogger, Severity } from "../logging/eventLogger"; -import { pluginId } from "./coqPilot"; -import VSCodeLogWriter from "./vscodeLogWriter"; +import VSCodeLogWriter from "./ui/vscodeLogWriter"; +import { pluginId } from "./utils/pluginId"; export class PluginContext implements Disposable { public readonly eventLogger: EventLogger = new EventLogger(); diff --git a/src/extension/sessionState.ts b/src/extension/sessionState.ts index c9621cba..36c42cfc 100644 --- a/src/extension/sessionState.ts +++ b/src/extension/sessionState.ts @@ -3,14 +3,15 @@ import { Disposable, OutputChannel } from "vscode"; import { createCoqLspClient } from "../coqLsp/coqLspBuilders"; import { CoqLspClient } from "../coqLsp/coqLspClient"; +import { CompletionAbortError } from "../core/abortUtils"; + import { EventLogger } from "../logging/eventLogger"; -import { parseCoqLspServerPath } from "./configReaders"; -import { CompletionAbortError } from "./extensionAbortUtils"; -import { PluginStatusIndicator } from "./pluginStatusIndicator"; +import { parseCoqLspServerPath } from "./settings/configReaders"; +import { PluginStatusIndicator } from "./ui/pluginStatusIndicator"; export class SessionState implements Disposable { - private _isSessionActive = true; + private _isActive = true; private _coqLspClient: CoqLspClient; private _abortController: AbortController; @@ -20,13 +21,13 @@ export class SessionState implements Disposable { private _userNotifiedAboutAbort = false; throwOnInactiveSession(): void { - if (!this._isSessionActive) { + if (!this._isActive) { throw new Error("Trying to access a disposed session state"); } } - get isSessionActive(): boolean { - return this._isSessionActive; + get isActive(): boolean { + return this._isActive; } get userNotifiedAboutAbort(): boolean { @@ -52,6 +53,8 @@ export class SessionState implements Disposable { ) { this._coqLspClient = coqLspClient; this._abortController = abortController; + + this.eventLogger.log("session-start", "User has started a new session"); } static async create( @@ -66,7 +69,7 @@ export class SessionState implements Disposable { coqLspServerPath, logOutputChannel, eventLogger, - abortController + abortController.signal ); pluginStatusIndicator.updateStatusBar(true); @@ -80,7 +83,7 @@ export class SessionState implements Disposable { ); } - userReceivedAbortNotification(): void { + markAbortNotificationAsShown(): void { this._userNotifiedAboutAbort = true; } @@ -89,23 +92,23 @@ export class SessionState implements Disposable { } hideInProgressSpinner(): void { - this.pluginStatusIndicator.hideInProgressSpinner(this._isSessionActive); + this.pluginStatusIndicator.hideInProgressSpinner(this._isActive); } async toggleCurrentSession(): Promise { - if (this._isSessionActive) { + if (this._isActive) { this.abort(); } else { - await this.startNewSession(); + await this.restartSession(); } } - abort(): void { - this._isSessionActive = false; + private abort(): void { + this._isActive = false; this._abortController.abort(new CompletionAbortError()); this._coqLspClient.dispose(); - this.pluginStatusIndicator.updateStatusBar(false); + this.pluginStatusIndicator.updateStatusBar(this._isActive); this.eventLogger.log( "session-abort", @@ -113,25 +116,28 @@ export class SessionState implements Disposable { ); } - async startNewSession(): Promise { - this._isSessionActive = true; + private async restartSession(): Promise { + this._isActive = true; this._abortController = new AbortController(); + this._userNotifiedAboutAbort = false; const coqLspServerPath = parseCoqLspServerPath(); this._coqLspClient = await createCoqLspClient( coqLspServerPath, this.logOutputChannel, this.eventLogger, - this._abortController + this._abortController.signal ); - this.pluginStatusIndicator.updateStatusBar(true); + this.pluginStatusIndicator.updateStatusBar(this._isActive); - this.eventLogger.log("session-start", "User has started a new session"); + this.eventLogger.log( + "session-restart", + "User has restarted the session" + ); } dispose(): void { - this._abortController.abort(); this._coqLspClient.dispose(); } } diff --git a/src/extension/configReaders.ts b/src/extension/settings/configReaders.ts similarity index 91% rename from src/extension/configReaders.ts rename to src/extension/settings/configReaders.ts index dcd0959b..5eafaa8b 100644 --- a/src/extension/configReaders.ts +++ b/src/extension/settings/configReaders.ts @@ -1,10 +1,10 @@ import Ajv, { DefinedError, JSONSchemaType } from "ajv"; import { WorkspaceConfiguration, workspace } from "vscode"; -import { LLMServices } from "../llm/llmServices"; -import { LLMService } from "../llm/llmServices/llmService"; -import { ModelParams, ModelsParams } from "../llm/llmServices/modelParams"; -import { SingleParamResolutionResult } from "../llm/llmServices/utils/paramsResolvers/abstractResolvers"; +import { LLMServices } from "../../llm/llmServices"; +import { LLMService } from "../../llm/llmServices/llmService"; +import { ModelParams, ModelsParams } from "../../llm/llmServices/modelParams"; +import { SingleParamResolutionResult } from "../../llm/llmServices/utils/paramsResolvers/abstractResolvers"; import { GrazieUserModelParams, LMStudioUserModelParams, @@ -15,21 +15,21 @@ import { lmStudioUserModelParamsSchema, openAiUserModelParamsSchema, predefinedProofsUserModelParamsSchema, -} from "../llm/userModelParams"; +} from "../../llm/userModelParams"; -import { ContextTheoremsRanker } from "../core/contextTheoremRanker/contextTheoremsRanker"; -import { DistanceContextTheoremsRanker } from "../core/contextTheoremRanker/distanceContextTheoremsRanker"; -import { JaccardIndexContextTheoremsRanker } from "../core/contextTheoremRanker/jaccardIndexContextTheoremsRanker"; -import { RandomContextTheoremsRanker } from "../core/contextTheoremRanker/randomContextTheoremsRanker"; +import { DistanceContextTheoremsRanker } from "../../core/contextTheoremRanker/actualRankers/distanceContextTheoremsRanker"; +import { JaccardIndexContextTheoremsRanker } from "../../core/contextTheoremRanker/actualRankers/jaccardIndexContextTheoremsRanker"; +import { RandomContextTheoremsRanker } from "../../core/contextTheoremRanker/actualRankers/randomContextTheoremsRanker"; +import { ContextTheoremsRanker } from "../../core/contextTheoremRanker/contextTheoremsRanker"; -import { AjvMode, buildAjv } from "../utils/ajvErrorsHandling"; -import { stringifyAnyValue, stringifyDefinedValue } from "../utils/printers"; - -import { pluginId } from "./coqPilot"; +import { AjvMode, buildAjv } from "../../utils/ajvErrorsHandling"; +import { stringifyAnyValue, stringifyDefinedValue } from "../../utils/printers"; import { EditorMessages, showMessageToUserWithSettingsHint, -} from "./editorMessages"; +} from "../ui/messages/editorMessages"; +import { pluginId } from "../utils/pluginId"; + import { SettingsValidationError, toSettingName, diff --git a/src/extension/settingsValidationError.ts b/src/extension/settings/settingsValidationError.ts similarity index 81% rename from src/extension/settingsValidationError.ts rename to src/extension/settings/settingsValidationError.ts index e9265048..29de23bf 100644 --- a/src/extension/settingsValidationError.ts +++ b/src/extension/settings/settingsValidationError.ts @@ -1,11 +1,11 @@ -import { switchByLLMServiceType } from "../llm/llmServices"; -import { LLMService } from "../llm/llmServices/llmService"; +import { switchByLLMServiceType } from "../../llm/llmServices"; +import { LLMService } from "../../llm/llmServices/llmService"; -import { pluginId } from "./coqPilot"; import { UIMessageSeverity, showMessageToUserWithSettingsHint, -} from "./editorMessages"; +} from "../ui/messages/editorMessages"; +import { pluginId } from "../utils/pluginId"; export class SettingsValidationError extends Error { constructor( diff --git a/src/extension/documentEditor.ts b/src/extension/ui/documentEditor.ts similarity index 100% rename from src/extension/documentEditor.ts rename to src/extension/ui/documentEditor.ts diff --git a/src/extension/editorMessages.ts b/src/extension/ui/messages/editorMessages.ts similarity index 96% rename from src/extension/editorMessages.ts rename to src/extension/ui/messages/editorMessages.ts index cd22d2c1..fa9a92ab 100644 --- a/src/extension/editorMessages.ts +++ b/src/extension/ui/messages/editorMessages.ts @@ -1,11 +1,10 @@ import { DefinedError } from "ajv"; import { commands, window } from "vscode"; -import { ajvErrorsAsString } from "../utils/ajvErrorsHandling"; -import { stringifyAnyValue } from "../utils/printers"; -import { Time } from "../utils/time"; - -import { pluginId } from "./coqPilot"; +import { ajvErrorsAsString } from "../../../utils/ajvErrorsHandling"; +import { stringifyAnyValue } from "../../../utils/printers"; +import { Time } from "../../../utils/time"; +import { pluginId } from "../../utils/pluginId"; export const openSettingsItem = "Open settings"; diff --git a/src/extension/llmServicesEventsHandler.ts b/src/extension/ui/messages/llmServicesEventsHandler.ts similarity index 92% rename from src/extension/llmServicesEventsHandler.ts rename to src/extension/ui/messages/llmServicesEventsHandler.ts index 0e87c061..43221229 100644 --- a/src/extension/llmServicesEventsHandler.ts +++ b/src/extension/ui/messages/llmServicesEventsHandler.ts @@ -2,26 +2,26 @@ import { ConfigurationError, GenerationFailedError, RemoteConnectionError, -} from "../llm/llmServiceErrors"; -import { LLMServices, asLLMServices } from "../llm/llmServices"; +} from "../../../llm/llmServiceErrors"; +import { LLMServices, asLLMServices } from "../../../llm/llmServices"; import { LLMServiceRequest, LLMServiceRequestFailed, LLMServiceRequestSucceeded, -} from "../llm/llmServices/commonStructures/llmServiceRequest"; -import { LLMServiceImpl } from "../llm/llmServices/llmService"; -import { ModelParams } from "../llm/llmServices/modelParams"; +} from "../../../llm/llmServices/commonStructures/llmServiceRequest"; +import { LLMServiceImpl } from "../../../llm/llmServices/llmService"; +import { ModelParams } from "../../../llm/llmServices/modelParams"; -import { EventLogger } from "../logging/eventLogger"; -import { stringifyAnyValue } from "../utils/printers"; -import { SimpleSet } from "../utils/simpleSet"; +import { EventLogger } from "../../../logging/eventLogger"; +import { stringifyAnyValue } from "../../../utils/printers"; +import { SimpleSet } from "../../../utils/simpleSet"; +import { toSettingName } from "../../settings/settingsValidationError"; import { EditorMessages, showMessageToUser, showMessageToUserWithSettingsHint, } from "./editorMessages"; -import { toSettingName } from "./settingsValidationError"; enum LLMServiceAvailablityState { AVAILABLE, diff --git a/src/extension/pluginStatusIndicator.ts b/src/extension/ui/pluginStatusIndicator.ts similarity index 96% rename from src/extension/pluginStatusIndicator.ts rename to src/extension/ui/pluginStatusIndicator.ts index 30182c7f..93b392cf 100644 --- a/src/extension/pluginStatusIndicator.ts +++ b/src/extension/ui/pluginStatusIndicator.ts @@ -5,7 +5,7 @@ import { window, } from "vscode"; -import { pluginName } from "./coqPilot"; +import { pluginName } from "../utils/pluginId"; export class PluginStatusIndicator { private readonly statusBarItem: StatusBarItem; diff --git a/src/extension/vscodeLogWriter.ts b/src/extension/ui/vscodeLogWriter.ts similarity index 95% rename from src/extension/vscodeLogWriter.ts rename to src/extension/ui/vscodeLogWriter.ts index 644e0e05..b7e9e973 100644 --- a/src/extension/vscodeLogWriter.ts +++ b/src/extension/ui/vscodeLogWriter.ts @@ -1,7 +1,11 @@ import pino, { DestinationStream, LoggerOptions } from "pino"; import { OutputChannel, window } from "vscode"; -import { EventLogger, Severity, anyEventKeyword } from "../logging/eventLogger"; +import { + EventLogger, + Severity, + anyEventKeyword, +} from "../../logging/eventLogger"; class VSCodeLogWriter { private readonly outputStream = new VSCodeOutputChannelDestinationStream( diff --git a/src/extension/utils/pluginId.ts b/src/extension/utils/pluginId.ts new file mode 100644 index 00000000..eea28acd --- /dev/null +++ b/src/extension/utils/pluginId.ts @@ -0,0 +1,2 @@ +export const pluginId = "coqpilot"; +export const pluginName = "CoqPilot"; diff --git a/src/extension/positionRangeUtils.ts b/src/extension/utils/positionRangeUtils.ts similarity index 100% rename from src/extension/positionRangeUtils.ts rename to src/extension/utils/positionRangeUtils.ts diff --git a/src/llm/llmServices/utils/chatFactory.ts b/src/llm/llmServices/utils/chatFactory.ts index ca027306..1e3efd43 100644 --- a/src/llm/llmServices/utils/chatFactory.ts +++ b/src/llm/llmServices/utils/chatFactory.ts @@ -189,7 +189,7 @@ export function createProofFixMessage( export function theoremToChatItem(theorem: Theorem): UserAssistantChatItem { return { userMessage: theorem.statement, - assistantMessage: theorem.proof?.onlyText() ?? "Admitted.", + assistantMessage: theorem.proof.onlyText(), }; } diff --git a/src/test/commonTestFunctions/coqFileParser.ts b/src/test/commonTestFunctions/coqFileParser.ts index a73137e8..e53b160d 100644 --- a/src/test/commonTestFunctions/coqFileParser.ts +++ b/src/test/commonTestFunctions/coqFileParser.ts @@ -1,4 +1,4 @@ -import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; +import { withDocumentOpenedByTestCoqLsp } from "../../coqLsp/coqLspBuilders"; import { parseCoqFile } from "../../coqParser/parseCoqFile"; import { Theorem } from "../../coqParser/parsedTypes"; @@ -14,18 +14,12 @@ export async function parseTheoremsFromCoqFile( resourcePath, projectRootPath ); - const fileUri = Uri.fromPath(filePath); - const client = await createTestCoqLspClient(rootDir); - await client.openTextDocument(fileUri); - const abortController = new AbortController(); - const document = await parseCoqFile( - fileUri, - client, - abortController.signal + return await withDocumentOpenedByTestCoqLsp( + { uri: fileUri }, + { workspaceRootPath: rootDir }, + (coqLspClient) => + parseCoqFile(fileUri, coqLspClient, new AbortController().signal) ); - await client.closeTextDocument(fileUri); - - return document; } diff --git a/src/test/commonTestFunctions/prepareEnvironment.ts b/src/test/commonTestFunctions/prepareEnvironment.ts index d4e51847..54d1d5e6 100644 --- a/src/test/commonTestFunctions/prepareEnvironment.ts +++ b/src/test/commonTestFunctions/prepareEnvironment.ts @@ -21,56 +21,66 @@ export interface PreparedEnvironment { completionContexts: CompletionContext[]; sourceFileEnvironment: SourceFileEnvironment; } + /** * Note: both paths should be relative to `src/test/resources/` folder. */ -export async function prepareEnvironment( +export async function withPreparedEnvironment( resourcePath: string[], - projectRootPath?: string[] -): Promise { + projectRootPath: string[] | undefined, + block: (preparedEnvironment: PreparedEnvironment) => Promise +) { const [filePath, rootDir] = resolveResourcesDir( resourcePath, projectRootPath ); const fileUri = Uri.fromPath(filePath); - const client = await createTestCoqLspClient(rootDir); + const client = await createTestCoqLspClient({ workspaceRootPath: rootDir }); const coqProofChecker = new CoqProofChecker(client); - - await client.openTextDocument(fileUri); - const abortController = new AbortController(); - const [completionContexts, sourceFileEnvironment] = await inspectSourceFile( - 1, - (_hole) => true, - fileUri, - client, - abortController.signal - ); - await client.closeTextDocument(fileUri); - - return { - coqLspClient: client, - coqProofChecker: coqProofChecker, - completionContexts: completionContexts, - sourceFileEnvironment: sourceFileEnvironment, - }; + try { + const [completionContexts, sourceFileEnvironment] = + await client.withTextDocument({ uri: fileUri }, () => + inspectSourceFile( + 1, + (_hole) => true, + fileUri, + client, + new AbortController().signal + ) + ); + const preparedEnvironment = { + coqLspClient: client, + coqProofChecker: coqProofChecker, + completionContexts: completionContexts, + sourceFileEnvironment: sourceFileEnvironment, + }; + return await block(preparedEnvironment); + } finally { + client.dispose(); + } } -export async function prepareEnvironmentWithContexts( +export async function withPreparedEnvironmentAndItsFirstContext( resourcePath: string[], - projectRootPath?: string[] -): Promise< - [PreparedEnvironment, [CompletionContext, ProofGenerationContext][]] -> { - const environment = await prepareEnvironment(resourcePath, projectRootPath); - return [ - environment, - environment.completionContexts.map((completionContext) => [ - completionContext, - buildProofGenerationContext( - completionContext, - environment.sourceFileEnvironment.fileTheorems - ), - ]), - ]; + projectRootPath: string[] | undefined, + block: ( + preparedEnvironment: PreparedEnvironment, + completionContext: CompletionContext, + proofGenerationContext: ProofGenerationContext + ) => Promise +): Promise { + return withPreparedEnvironment( + resourcePath, + projectRootPath, + (environment) => + block( + environment, + environment.completionContexts[0], + buildProofGenerationContext( + environment.completionContexts[0], + environment.sourceFileEnvironment.fileTheorems + ) + ) + ); } diff --git a/src/test/coqLsp/coqLspGetGoals.test.ts b/src/test/coqLsp/coqLspGetGoals.test.ts index bbb7bb1d..c06586b5 100644 --- a/src/test/coqLsp/coqLspGetGoals.test.ts +++ b/src/test/coqLsp/coqLspGetGoals.test.ts @@ -1,8 +1,8 @@ import { expect } from "earl"; import { Result } from "ts-results"; -import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; -import { Goal, PpString } from "../../coqLsp/coqLspTypes"; +import { withDocumentOpenedByTestCoqLsp } from "../../coqLsp/coqLspBuilders"; +import { ProofGoal } from "../../coqLsp/coqLspTypes"; import { Uri } from "../../utils/uri"; import { resolveResourcesDir } from "../commonTestFunctions/pathsResolver"; @@ -12,26 +12,30 @@ suite("Retrieve goals from Coq file", () => { points: { line: number; character: number }[], resourcePath: string[], projectRootPath?: string[] - ): Promise[], Error>[]> { + ): Promise[]> { const [filePath, rootDir] = resolveResourcesDir( resourcePath, projectRootPath ); const fileUri = Uri.fromPath(filePath); - const client = await createTestCoqLspClient(rootDir); - await client.openTextDocument(fileUri); - const goals = await Promise.all( - points.map(async (point) => { - return await client.getGoalsAtPoint(point, fileUri, 1); - }) + return withDocumentOpenedByTestCoqLsp( + { uri: fileUri }, + { workspaceRootPath: rootDir }, + (coqLspClient) => + Promise.all( + points.map(async (point) => { + return await coqLspClient.getGoalsAtPoint( + point, + fileUri, + 1 + ); + }) + ) ); - await client.closeTextDocument(fileUri); - - return goals; } - function unpackGoal(goal: Goal): { hyps: string[]; ty: string } { + function unpackGoal(goal: ProofGoal): { hyps: string[]; ty: string } { return { hyps: goal.hyps.map((hyp) => `${hyp.names.join(" ")} : ${hyp.ty}`), ty: goal.ty as string, diff --git a/src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts b/src/test/coqLsp/coqLspGetGoalsWithCommandApplied.test.ts similarity index 66% rename from src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts rename to src/test/coqLsp/coqLspGetGoalsWithCommandApplied.test.ts index 1c284985..5fcdc67c 100644 --- a/src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts +++ b/src/test/coqLsp/coqLspGetGoalsWithCommandApplied.test.ts @@ -1,48 +1,38 @@ import { expect } from "earl"; import { Result } from "ts-results"; -import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; -import { Goal, PpString } from "../../coqLsp/coqLspTypes"; +import { withDocumentOpenedByTestCoqLsp } from "../../coqLsp/coqLspBuilders"; +import { ProofGoal } from "../../coqLsp/coqLspTypes"; import { Uri } from "../../utils/uri"; import { resolveResourcesDir } from "../commonTestFunctions/pathsResolver"; suite("Request goals with `command/pretac` argument", () => { - async function getGoalsAtPosition( + async function requestGoalsWithCommandApplied( position: { line: number; character: number }, resourcePath: string[], command: string, projectRootPath?: string[] - ): Promise[], Error>> { + ): Promise> { const [filePath, rootDir] = resolveResourcesDir( resourcePath, projectRootPath ); const fileUri = Uri.fromPath(filePath); - const client = await createTestCoqLspClient(rootDir); - let goals: Result[], Error> | undefined; - - try { - await client.openTextDocument(fileUri); - goals = await client.getGoalsAtPoint(position, fileUri, 1, command); - } finally { - await client.closeTextDocument(fileUri); - client.dispose(); - } - - if (goals === undefined) { - throw new Error("The goals were not received."); - } - - return goals; + return withDocumentOpenedByTestCoqLsp( + { uri: fileUri }, + { workspaceRootPath: rootDir }, + (coqLspClient) => + coqLspClient.getGoalsAtPoint(position, fileUri, 1, command) + ); } - function checkSuccessfullGoalConcls( - goals: Result[], Error>, + function checkSuccessfullGoalConclusions( + goals: Result, goalConclusions: string[] ): void { - expect(goals.ok).toEqual(true); + expect(goals.ok).toBeTruthy(); if (goals.ok) { expect(goals.val).toHaveLength(goalConclusions.length); for (let i = 0; i < goalConclusions.length; i++) { @@ -52,18 +42,18 @@ suite("Request goals with `command/pretac` argument", () => { } function checkCommandApplicationError( - goals: Result[], Error>, + goals: Result, expectedError: string ): void { - expect(goals.err).toEqual(true); + expect(goals.err).toBeTruthy(); expect(goals.val).toBeA(Error); if (goals.err) { expect(goals.val.message).toEqual(expectedError); } } - test("One Coq sentence: fail to solve with invalid goal", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence: failed to solve with invalid goal", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["small_document.v"], "reflexivity." @@ -75,8 +65,8 @@ suite("Request goals with `command/pretac` argument", () => { ); }); - test("One Coq sentence: fail to solve with invalid tactic", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence: failed to solve with invalid tactic", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["small_document.v"], "reflexivit." @@ -88,51 +78,51 @@ suite("Request goals with `command/pretac` argument", () => { ); }); - test("One Coq sentence: successfully solve no goals left", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence: successfully solved, no goals left", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["small_document.v"], "auto." ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); - test("One Coq sentence: successfully solve 1 goal left", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence: successfully solved, 1 goal left", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["test_many_subgoals.v"], "auto." ); - checkSuccessfullGoalConcls(goals, ["S n + 0 = S n"]); + checkSuccessfullGoalConclusions(goals, ["S n + 0 = S n"]); }); - test("One Coq sentence: successfully solve 2 goals left", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence: successfully solved, 2 goals left", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 22, character: 4 }, ["test_many_subgoals.v"], "auto." ); - checkSuccessfullGoalConcls(goals, [ + checkSuccessfullGoalConclusions(goals, [ "Second = First \\/ Second = Second \\/ Second = Third", "Third = First \\/ Third = Second \\/ Third = Third", ]); }); - test("One Coq sentence wrapped into curly braces: solve successfully", async () => { - const goals = await getGoalsAtPosition( + test("One Coq sentence wrapped into curly braces: solved successfully", async () => { + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["small_document.v"], " { auto. }" ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); test("One Coq sentence wrapped into curly braces: invalid proof", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 9, character: 4 }, ["small_document.v"], " { kek. }" @@ -145,27 +135,27 @@ suite("Request goals with `command/pretac` argument", () => { }); test("One Coq sentence wrapped into curly braces: valid proof, test indent", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "{ auto. }" ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); test("Many Coq sentences: valid proof", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "simpl. induction n. reflexivity. auto." ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); test("Many Coq sentences: invalid proof", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "simpl. induction n. reflexivity. reflexivity." @@ -178,17 +168,17 @@ suite("Request goals with `command/pretac` argument", () => { }); test("Many Coq sentences: valid proof with multiple curly braces", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "{ simpl. \n induction n. \n { reflexivity. }\n auto. \n }" ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); test("Many Coq sentences: invalid proof with multiple curly braces", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "{ simpl. \n induction n. \n { reflexivity. }\n reflexivity. \n }" @@ -201,17 +191,17 @@ suite("Request goals with `command/pretac` argument", () => { }); test("Many Coq sentences: valid proof with bullets", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "{ \n simpl. \n induction n. \n - reflexivity.\n - auto. \n }" ); - checkSuccessfullGoalConcls(goals, []); + checkSuccessfullGoalConclusions(goals, []); }); test("Many Coq sentences: invalid proof with bullets", async () => { - const goals = await getGoalsAtPosition( + const goals = await requestGoalsWithCommandApplied( { line: 2, character: 12 }, ["test_many_subgoals.v"], "{ \n simpl. \n induction n. \n - reflexivity.\n - reflexivity. \n }" diff --git a/src/test/coqParser/parseCoqFile.test.ts b/src/test/coqParser/parseCoqFile.test.ts index cc4c06fd..5d9b8ee7 100644 --- a/src/test/coqParser/parseCoqFile.test.ts +++ b/src/test/coqParser/parseCoqFile.test.ts @@ -34,15 +34,14 @@ suite("Coq file parser tests", () => { expect(theorem.name).toEqual(theoremData[i].name); expect(theorem.statement).toEqual(theoremData[i].statement); expect(theorem.statement_range.start).toEqual(theoremData[i].start); - expect(theorem.proof).not.toBeNullish(); - expect(theorem.proof?.end_pos.end).toEqual(theoremData[i].end); - expect(theorem.proof?.is_incomplete).toEqual( + expect(theorem.proof.end_pos.end).toEqual(theoremData[i].end); + expect(theorem.proof.is_incomplete).toEqual( theoremData[i].isIncomplete ); - expect(theorem.proof!.holes).toHaveLength( + expect(theorem.proof.holes).toHaveLength( theoremData[i].holesStartPoints.length ); - for (const [j, hole] of theorem.proof!.holes.entries()) { + for (const [j, hole] of theorem.proof.holes.entries()) { expect(hole.range.start).toEqual( theoremData[i].holesStartPoints[j].start ); @@ -80,7 +79,7 @@ suite("Coq file parser tests", () => { }, ]; - const holes = doc.map((theorem) => theorem.proof?.holes ?? []).flat(); + const holes = doc.map((theorem) => theorem.proof.holes).flat(); expect(holes).toHaveLength(6); for (const [i, hole] of holes.entries()) { @@ -123,8 +122,7 @@ suite("Coq file parser tests", () => { for (const [i, theorem] of doc.entries()) { expect(theorem.name).toEqual(theoremData[i].name); expect(theorem.statement).toEqual(theoremData[i].statement); - expect(theorem.proof).not.toBeNullish(); - expect(theorem.proof?.is_incomplete).toEqual( + expect(theorem.proof.is_incomplete).toEqual( theoremData[i].isIncomplete ); } diff --git a/src/test/core/completionGenerator.test.ts b/src/test/core/completionGenerator.test.ts index d7fddc75..9ec28e12 100644 --- a/src/test/core/completionGenerator.test.ts +++ b/src/test/core/completionGenerator.test.ts @@ -15,7 +15,7 @@ import { createDefaultServices, createPredefinedProofsModelsParams, } from "../commonTestFunctions/defaultLLMServicesBuilder"; -import { prepareEnvironment } from "../commonTestFunctions/prepareEnvironment"; +import { withPreparedEnvironment } from "../commonTestFunctions/prepareEnvironment"; suite("Completion generation tests", () => { async function generateCompletionForAdmitsFromFile( @@ -23,42 +23,39 @@ suite("Completion generation tests", () => { predefinedProofs: string[], projectRootPath?: string[] ): Promise { - const environment = await prepareEnvironment( + return withPreparedEnvironment( resourcePath, - projectRootPath + projectRootPath, + async (environment) => { + const processEnvironment: ProcessEnvironment = { + coqProofChecker: environment.coqProofChecker, + modelsParams: + createPredefinedProofsModelsParams(predefinedProofs), + services: createDefaultServices(), + }; + try { + return await environment.coqLspClient.withTextDocument( + { uri: environment.sourceFileEnvironment.fileUri }, + () => + Promise.all( + environment.completionContexts.map( + async (completionContext) => { + const result = await generateCompletion( + completionContext, + environment.sourceFileEnvironment, + processEnvironment, + new AbortController().signal + ); + return result; + } + ) + ) + ); + } finally { + disposeServices(processEnvironment.services); + } + } ); - const processEnvironment: ProcessEnvironment = { - coqProofChecker: environment.coqProofChecker, - modelsParams: createPredefinedProofsModelsParams(predefinedProofs), - services: createDefaultServices(), - }; - const abortController = new AbortController(); - try { - await environment.coqLspClient.openTextDocument( - environment.sourceFileEnvironment.fileUri - ); - - const generationResult = await Promise.all( - environment.completionContexts.map( - async (completionContext) => { - const result = await generateCompletion( - completionContext, - environment.sourceFileEnvironment, - processEnvironment, - abortController.signal - ); - return result; - } - ) - ); - - return generationResult; - } finally { - disposeServices(processEnvironment.services); - await environment.coqLspClient.closeTextDocument( - environment.sourceFileEnvironment.fileUri - ); - } } function unpackProof(text: string): string { diff --git a/src/test/core/coqProofChecker.test.ts b/src/test/core/coqProofChecker.test.ts index ef864a39..473f225a 100644 --- a/src/test/core/coqProofChecker.test.ts +++ b/src/test/core/coqProofChecker.test.ts @@ -1,6 +1,6 @@ import { expect } from "earl"; -import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; +import { withDocumentOpenedByTestCoqLsp } from "../../coqLsp/coqLspBuilders"; import { CoqProofChecker } from "../../core/coqProofChecker"; import { ProofCheckResult } from "../../core/coqProofChecker"; @@ -22,35 +22,32 @@ suite("`CoqProofChecker` tests", () => { const fileUri = Uri.fromPath(filePath); const documentVersion = 1; - const client = await createTestCoqLspClient(rootDir); - const coqProofChecker = new CoqProofChecker(client); - await client.openTextDocument(fileUri); - - const preparedProofs = proofsToCheck.map((proofs) => - proofs.map(prepareProofBeforeCheck) - ); - - const proofRes = await Promise.all( - positions.map(async (position, i) => { - const proofCheckRes = await coqProofChecker.checkProofs( - fileUri, - documentVersion, - position, - preparedProofs[i] + return withDocumentOpenedByTestCoqLsp( + { uri: fileUri, version: documentVersion }, + { workspaceRootPath: rootDir }, + (coqLspClient) => { + const coqProofChecker = new CoqProofChecker(coqLspClient); + const preparedProofs = proofsToCheck.map((proofs) => + proofs.map(prepareProofBeforeCheck) + ); + return Promise.all( + positions.map(async (position, i) => { + const proofCheckRes = await coqProofChecker.checkProofs( + fileUri, + documentVersion, + position, + preparedProofs[i] + ); + return proofCheckRes.map((res) => { + return { + ...res, + proof: unpackProof(res.proof), + }; + }); + }) ); - return proofCheckRes.map((res) => { - return { - ...res, - proof: unpackProof(res.proof), - }; - }); - }) + } ); - - await client.closeTextDocument(fileUri); - client.dispose(); - - return proofRes; } function prepareProofBeforeCheck(proof: string) { diff --git a/src/test/legacyBenchmark/benchmarkingFramework.ts b/src/test/legacyBenchmark/benchmarkingFramework.ts index 84374d8a..5a20d336 100644 --- a/src/test/legacyBenchmark/benchmarkingFramework.ts +++ b/src/test/legacyBenchmark/benchmarkingFramework.ts @@ -11,7 +11,7 @@ import { OpenAiService } from "../../llm/llmServices/openai/openAiService"; import { PredefinedProofsService } from "../../llm/llmServices/predefinedProofs/predefinedProofsService"; import { resolveParametersOrThrow } from "../../llm/llmServices/utils/resolveOrThrow"; -import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; +import { withDocumentOpenedByTestCoqLsp } from "../../coqLsp/coqLspBuilders"; import { CoqLspClient } from "../../coqLsp/coqLspClient"; import { ProofGoal } from "../../coqLsp/coqLspTypes"; @@ -38,44 +38,120 @@ import { InputModelsParams } from "./inputModelsParams"; import { BenchmarkReportHolder, TheoremProofResult } from "./reportHolder"; import { consoleLog, consoleLogSeparatorLine } from "./utils/loggingUtils"; +export interface TestBenchmarkOptions extends TestBenchmarkOptionsWithDefaults { + filePath: string; + inputModelsParams: InputModelsParams; + relativePathToFile: string; +} + +export interface TestBenchmarkOptionsWithDefaults { + specificTheoremsForBenchmark: string[] | undefined; + benchmarkFullTheorems: Boolean; + benchmarkAdmits: Boolean; + workspaceRootPath?: string; + requireAllAdmitsCompleted: Boolean; + maxPremisesNumber?: number; + groupName: string; + reportHolder?: BenchmarkReportHolder; + additionalImports?: AdditionalFileImport[]; + perProofTimeoutMillis: number; +} + +export function resolveTestBenchmarkOptionsWithDefaults( + inputOptions: TestBenchmarkOptions & + Partial +): TestBenchmarkOptions { + return { + ...inputOptions, + benchmarkFullTheorems: inputOptions.benchmarkFullTheorems ?? true, + benchmarkAdmits: inputOptions.benchmarkAdmits ?? true, + requireAllAdmitsCompleted: + inputOptions.requireAllAdmitsCompleted ?? false, + groupName: inputOptions.groupName ?? "Unnamed", + perProofTimeoutMillis: inputOptions.perProofTimeoutMillis ?? 15_000, + }; +} + export async function runTestBenchmark( + inputOptions: TestBenchmarkOptions +): Promise { + const resolvedOptions = + resolveTestBenchmarkOptionsWithDefaults(inputOptions); + + const [fileUri, isNewlyCreatedFile] = getFileUriWithImports( + resolvedOptions.filePath, + resolvedOptions.additionalImports + ); + /** + * Note: so far the abort signal is never triggered; + * however, such behaviour can be supported: + * the same `AbortController` object is passed throughout the run properly. + */ + const abortController = new AbortController(); + + return withDocumentOpenedByTestCoqLsp( + { uri: fileUri }, + { + workspaceRootPath: inputOptions.workspaceRootPath, + abortSignal: abortController.signal, + }, + (coqLspClient) => + runTestBenchmarkOnPreparedFile( + resolvedOptions, + coqLspClient, + fileUri, + isNewlyCreatedFile, + abortController + ) + ); +} + +function getFileUriWithImports( filePath: string, - inputModelsParams: InputModelsParams, - relativePathToFile: string, - specificTheoremsForBenchmark: string[] | undefined, - benchmarkFullTheorems: Boolean = true, - benchmarkAdmits: Boolean = true, - workspaceRootPath?: string, - requireAllAdmitsCompleted: Boolean = false, - maxPremisesNumber?: number, - groupName: string = "Unnamed", - reportHolder?: BenchmarkReportHolder, - additionalImports?: AdditionalFileImport[], - perProofTimeoutMillis: number = 15000 + additionalImports?: AdditionalFileImport[] +): [Uri, boolean] { + if (additionalImports === undefined) { + return [Uri.fromPath(filePath), false]; + } + const importStrings = + additionalImports?.map((importFile) => importFile.get()) ?? []; + const fileContent = fs.readFileSync(filePath, "utf8"); + const updatedFileContent = importStrings.join("\n") + "\n" + fileContent; + const auxFilePath = buildAuxFileUri(filePath); + fs.writeFileSync(auxFilePath.fsPath, updatedFileContent); + return [auxFilePath, true]; +} + +export async function runTestBenchmarkOnPreparedFile( + options: TestBenchmarkOptions, + coqLspClient: CoqLspClient, + fileUri: Uri, + isNewlyCreatedFile: boolean, + abortController: AbortController ): Promise { - consoleLog(`run benchmarks for file: ${filePath}\n`, "blue"); + consoleLog(`run benchmarks for file: ${options.filePath}\n`, "blue"); const shouldCompleteHole = (_hole: ProofStep) => true; const eventLogger = new EventLogger(); const [completionTargets, sourceFileEnvironment, processEnvironment] = await prepareForBenchmarkCompletions( - inputModelsParams, + options.inputModelsParams, shouldCompleteHole, - workspaceRootPath, - filePath, - eventLogger, - additionalImports + coqLspClient, + fileUri, + isNewlyCreatedFile, + eventLogger ); const filteredCompletionTargets = { admitTargets: completionTargets.admitTargets.filter( (target) => - specificTheoremsForBenchmark?.includes( + options.specificTheoremsForBenchmark?.includes( target.parentTheorem.name ) ?? true ), theoremTargets: completionTargets.theoremTargets.filter( (target) => - specificTheoremsForBenchmark?.includes( + options.specificTheoremsForBenchmark?.includes( target.parentTheorem.name ) ?? true ), @@ -86,43 +162,45 @@ export async function runTestBenchmark( let admitTargetsResults: BenchmarkResult | undefined = undefined; let theoremTargetsResults: BenchmarkResult | undefined = undefined; - if (benchmarkAdmits) { + if (options.benchmarkAdmits) { consoleLog("try to complete admits\n"); admitTargetsResults = await benchmarkTargets( filteredCompletionTargets.admitTargets, sourceFileEnvironment, processEnvironment, - getSingleModelId(inputModelsParams), - relativePathToFile, - groupName, + getSingleModelId(options.inputModelsParams), + options.relativePathToFile, + options.groupName, + abortController, eventLogger, - maxPremisesNumber, - reportHolder, - perProofTimeoutMillis + options.maxPremisesNumber, + options.reportHolder, + options.perProofTimeoutMillis ); consoleLog( `BENCHMARK RESULT, ADMITS COMPLETED: ${admitTargetsResults}\n` ); consoleLogSeparatorLine("\n"); - if (requireAllAdmitsCompleted) { + if (options.requireAllAdmitsCompleted) { assert.ok(admitTargetsResults.allCompleted()); } } - if (benchmarkFullTheorems) { + if (options.benchmarkFullTheorems) { consoleLog("try to prove theorems\n"); theoremTargetsResults = await benchmarkTargets( filteredCompletionTargets.theoremTargets, sourceFileEnvironment, processEnvironment, - getSingleModelId(inputModelsParams), - relativePathToFile, - groupName, + getSingleModelId(options.inputModelsParams), + options.relativePathToFile, + options.groupName, + abortController, eventLogger, - maxPremisesNumber, - reportHolder, - perProofTimeoutMillis + options.maxPremisesNumber, + options.reportHolder, + options.perProofTimeoutMillis ); consoleLog( `BENCHMARK RESULT, THEOREMS PROVED: ${theoremTargetsResults}\n` @@ -195,6 +273,7 @@ export async function benchmarkTargets( modelId: string, checkedFilePath: string, groupName: string, + abortController: AbortController, eventLogger: EventLogger, maxPremisesNumber?: number, reportHolder?: BenchmarkReportHolder, @@ -210,6 +289,7 @@ export async function benchmarkTargets( modelId, checkedFilePath, groupName, + abortController, eventLogger, maxPremisesNumber, reportHolder, @@ -232,6 +312,7 @@ async function benchmarkCompletionGeneration( modelId: string, checkedFilePath: string, groupName: string, + abortController: AbortController, eventLogger: EventLogger, maxPremisesNumber?: number, reportHolder?: BenchmarkReportHolder, @@ -266,7 +347,6 @@ async function benchmarkCompletionGeneration( premisesNumber: maxPremisesNumber, }; - const abortController = new AbortController(); const result = await generateCompletion( completionContext, sourceFileEnvironmentWithFilteredContext, @@ -357,44 +437,21 @@ function buildAuxFileUri(filePath: string, unique: boolean = true): Uri { async function prepareForBenchmarkCompletions( inputModelsParams: InputModelsParams, shouldCompleteHole: (hole: ProofStep) => boolean, - workspaceRootPath: string | undefined, - filePath: string, - eventLogger: EventLogger, - additionalImports?: AdditionalFileImport[] + coqLspClient: CoqLspClient, + fileUri: Uri, + isNewlyCreatedFile: boolean, + eventLogger: EventLogger ): Promise< [BenchmarkingCompletionTargets, SourceFileEnvironment, ProcessEnvironment] > { - function getFileUriWithImports( - filePath: string, - additionalImports?: AdditionalFileImport[] - ): [Uri, boolean] { - if (additionalImports === undefined) { - return [Uri.fromPath(filePath), false]; - } - - const importStrings = - additionalImports?.map((importFile) => importFile.get()) ?? []; - const fileContent = fs.readFileSync(filePath, "utf8"); - const updatedFileContent = - importStrings.join("\n") + "\n" + fileContent; - const auxFilePath = buildAuxFileUri(filePath); - fs.writeFileSync(auxFilePath.fsPath, updatedFileContent); - return [auxFilePath, true]; - } - - const [fileUri, isNew] = getFileUriWithImports(filePath, additionalImports); - - const client = await createTestCoqLspClient(workspaceRootPath); - await client.openTextDocument(fileUri); - - const coqProofChecker = new CoqProofChecker(client); + const coqProofChecker = new CoqProofChecker(coqLspClient); const mockDocumentVersion = 1; const [completionTargets, sourceFileEnvironment] = await extractCompletionTargets( mockDocumentVersion, shouldCompleteHole, fileUri, - client + coqLspClient ); const llmServices: LLMServices = { openAiService: new OpenAiService(eventLogger), @@ -411,7 +468,7 @@ async function prepareForBenchmarkCompletions( services: llmServices, }; - if (isNew) { + if (isNewlyCreatedFile) { fs.unlinkSync(fileUri.fsPath); } @@ -463,7 +520,7 @@ async function createCompletionTargets( const theoremsWithProofs = fileTheorems.filter((thr) => thr.proof); const admitHolesToComplete = theoremsWithProofs .map((thr) => - thr.proof!.holes.map((hole) => { + thr.proof.holes.map((hole) => { return { parentTheorem: thr, proofStep: hole, @@ -477,7 +534,7 @@ async function createCompletionTargets( const firstProofSteps = theoremsWithProofs.map((thr) => { return { parentTheorem: thr, - proofStep: thr.proof!.proof_steps[1], + proofStep: thr.proof.proof_steps[1], }; }); @@ -510,15 +567,12 @@ async function resolveProofStepsToCompletionContexts( fileUri, documentVersion ); - if (goals.ok) { - const firstGoal = goals.val.shift(); - if (firstGoal) { - completionContexts.push({ - proofGoal: firstGoal, - admitRange: parentedProofStep.proofStep.range, - parentTheorem: parentedProofStep.parentTheorem, - }); - } + if (goals.ok && goals.val.length !== 0) { + completionContexts.push({ + proofGoal: goals.val[0], + admitRange: parentedProofStep.proofStep.range, + parentTheorem: parentedProofStep.parentTheorem, + }); } } return completionContexts; diff --git a/src/test/legacyBenchmark/report.json b/src/test/legacyBenchmark/report.json deleted file mode 100644 index 9e26dfee..00000000 --- a/src/test/legacyBenchmark/report.json +++ /dev/null @@ -1 +0,0 @@ -{} \ No newline at end of file diff --git a/src/test/legacyBenchmark/reportHolder.ts b/src/test/legacyBenchmark/reportHolder.ts index bbd02c9c..609d5bf5 100644 --- a/src/test/legacyBenchmark/reportHolder.ts +++ b/src/test/legacyBenchmark/reportHolder.ts @@ -44,10 +44,6 @@ export class BenchmarkReportHolder { private readonly groupOrder = ["A", "B", "C"]; constructor(private readonly reportPath: string) { - if (!existsSync(reportPath)) { - writeFileSync(reportPath, "{}"); - } - const jsonSchemaValidator = buildAjv(AjvMode.RETURN_AFTER_FIRST_ERROR); this.validate = jsonSchemaValidator.compile(theoremProofResultSchema); } @@ -153,10 +149,16 @@ export class BenchmarkReportHolder { } parseReport(): BenchmarkReport { + if (!existsSync(this.reportPath)) { + writeFileSync(this.reportPath, "{}"); + return {}; + } + const reportContent = JSON.parse( readFileSync(this.reportPath, { encoding: "utf-8" }) ); const report: BenchmarkReport = {}; + for (const [theoremName, proofResults] of Object.entries( reportContent )) { diff --git a/src/test/legacyBenchmark/results.ts b/src/test/legacyBenchmark/results.ts index 0053babf..9a1f620b 100644 --- a/src/test/legacyBenchmark/results.ts +++ b/src/test/legacyBenchmark/results.ts @@ -84,7 +84,7 @@ export namespace Results { readonly name = this.theorem.name; readonly proofLength: LengthMetrics = { - inSteps: this.theorem.proof?.proof_steps.length, + inSteps: this.theorem.proof.proof_steps.length, }; // TODO diff --git a/src/test/legacyBenchmark/runBenchmark.test.ts b/src/test/legacyBenchmark/runBenchmark.test.ts index d3873b55..3b2626dc 100644 --- a/src/test/legacyBenchmark/runBenchmark.test.ts +++ b/src/test/legacyBenchmark/runBenchmark.test.ts @@ -104,21 +104,15 @@ suite("[SourceExecutable] Legacy Benchmark", () => { for (const resolvedFilePath of resolvedFilePaths) { const { admitsCompleted, theoremsProved } = - await runTestBenchmark( - resolvedFilePath, - benchmark.inputModelsParams, - item.path, - item.specificTheoremForBenchmark, - benchmark.benchmarkFullTheorems, - benchmark.benchmarkAdmits, - resolvedWorkspaceRootPath, - benchmark.requireAllAdmitsCompleted, - benchmark.maxPremisesNumber, - benchmark.groupName, - reportHolder, - benchmark.additionalImports, - benchmark.perProofTimeoutMillis - ); + await runTestBenchmark({ + ...benchmark, + filePath: resolvedFilePath, + relativePathToFile: item.path, + specificTheoremsForBenchmark: + item.specificTheoremsForBenchmark, + workspaceRootPath: resolvedWorkspaceRootPath, + reportHolder: reportHolder, + }); admitsCompletedInTotal.add( admitsCompleted ?? new BenchmarkResult(0, 0) ); diff --git a/src/test/legacyBenchmark/utils/datasetConstructionUtils.ts b/src/test/legacyBenchmark/utils/datasetConstructionUtils.ts index 116f814f..8efd7694 100644 --- a/src/test/legacyBenchmark/utils/datasetConstructionUtils.ts +++ b/src/test/legacyBenchmark/utils/datasetConstructionUtils.ts @@ -2,16 +2,16 @@ import * as fs from "fs"; export class DatasetItem { workspaceRootPath: string | undefined; - specificTheoremForBenchmark: string[] | undefined; + specificTheoremsForBenchmark: string[] | undefined; /* Paths should be relative to 'dataset' folder */ constructor( public path: string, - specificTheoremForBenchmark: string[] | undefined = undefined, + specificTheoremsForBenchmark: string[] | undefined = undefined, workspaceRootPath: string | undefined = undefined ) { this.workspaceRootPath = workspaceRootPath; - this.specificTheoremForBenchmark = specificTheoremForBenchmark; + this.specificTheoremsForBenchmark = specificTheoremsForBenchmark; } } diff --git a/src/test/llm/llmServices/utils/chatFactory.test.ts b/src/test/llm/llmServices/utils/chatFactory.test.ts index 0aea81dc..b1b9b1c8 100644 --- a/src/test/llm/llmServices/utils/chatFactory.test.ts +++ b/src/test/llm/llmServices/utils/chatFactory.test.ts @@ -72,8 +72,6 @@ suite("[LLMService-s utils] Building chats test", () => { async function buildTestData(): Promise<[TestTheorems, TestMessages]> { const [plusTheorem, plusAssocTheorem, theoremToComplete] = await readTheorems(); - expect(plusTheorem.proof).toBeTruthy(); - expect(plusAssocTheorem.proof).toBeTruthy(); const messages = { systemMessage: { @@ -95,11 +93,11 @@ suite("[LLMService-s utils] Building chats test", () => { plusTheoremProof: { role: "assistant", - content: plusTheorem.proof!.onlyText(), + content: plusTheorem.proof.onlyText(), } as ChatMessage, plusAssocTheoremProof: { role: "assistant", - content: plusAssocTheorem.proof!.onlyText(), + content: plusAssocTheorem.proof.onlyText(), } as ChatMessage, }; diff --git a/src/test/llm/llmServices/utils/chatTokensFitter.test.ts b/src/test/llm/llmServices/utils/chatTokensFitter.test.ts index 98e4f6db..9bc2badd 100644 --- a/src/test/llm/llmServices/utils/chatTokensFitter.test.ts +++ b/src/test/llm/llmServices/utils/chatTokensFitter.test.ts @@ -95,7 +95,7 @@ suite("[LLMService-s utils] ChatTokensFitter test", () => { test("Two theorems, overflow after first", async () => { const twoTheorems = await readTwoTheorems(); const statementTokens = approxCalculateTokens(twoTheorems[0].statement); - const theoremProof = twoTheorems[0].proof?.onlyText() ?? ""; + const theoremProof = twoTheorems[0].proof.onlyText(); const proofTokens = approxCalculateTokens(theoremProof); const fittedTheoremsNumber = countTheoremsPickedFromContext({ maxTokensToGenerate: 1000, @@ -110,7 +110,7 @@ suite("[LLMService-s utils] ChatTokensFitter test", () => { test("Two theorems, overflow almost before first", async () => { const twoTheorems = await readTwoTheorems(); const statementTokens = approxCalculateTokens(twoTheorems[0].statement); - const theoremProof = twoTheorems[0].proof?.onlyText() ?? ""; + const theoremProof = twoTheorems[0].proof.onlyText(); const proofTokens = approxCalculateTokens(theoremProof); const fittedTheoremsNumber = countTheoremsPickedFromContext({ maxTokensToGenerate: 1000, @@ -128,7 +128,7 @@ suite("[LLMService-s utils] ChatTokensFitter test", () => { twoTheorems[0].statement, gptModelName ); - const theoremProof = twoTheorems[0].proof?.onlyText() ?? ""; + const theoremProof = twoTheorems[0].proof.onlyText(); const proofTokens = calculateTokensViaTikToken( theoremProof, gptModelName diff --git a/src/test/llm/llmSpecificTestUtils/testAdmitCompletion.ts b/src/test/llm/llmSpecificTestUtils/testAdmitCompletion.ts index d2789c22..335b4009 100644 --- a/src/test/llm/llmSpecificTestUtils/testAdmitCompletion.ts +++ b/src/test/llm/llmSpecificTestUtils/testAdmitCompletion.ts @@ -6,7 +6,7 @@ import { ModelParams } from "../../../llm/llmServices/modelParams"; import { UserModelParams } from "../../../llm/userModelParams"; import { checkTheoremProven } from "../../commonTestFunctions/checkProofs"; -import { prepareEnvironmentWithContexts } from "../../commonTestFunctions/prepareEnvironment"; +import { withPreparedEnvironmentAndItsFirstContext } from "../../commonTestFunctions/prepareEnvironment"; import { withLLMServiceAndParams } from "../../commonTestFunctions/withLLMService"; export async function testLLMServiceCompletesAdmitFromFile< @@ -22,22 +22,30 @@ export async function testLLMServiceCompletesAdmitFromFile< service, inputParams, async (service, resolvedParams: ResolvedModelParams) => { - const [environment, [[completionContext, proofGenerationContext]]] = - await prepareEnvironmentWithContexts(resourcePath); - const generatedProofs = await service.generateProof( - proofGenerationContext, - resolvedParams, - choices, - ErrorsHandlingMode.RETHROW_ERRORS - ); - expect(generatedProofs).toHaveLength(choices); - expect( - checkTheoremProven( - generatedProofs, + withPreparedEnvironmentAndItsFirstContext( + resourcePath, + undefined, + async ( + environment, completionContext, - environment - ) - ).toBeTruthy(); + proofGenerationContext + ) => { + const generatedProofs = await service.generateProof( + proofGenerationContext, + resolvedParams, + choices, + ErrorsHandlingMode.RETHROW_ERRORS + ); + expect(generatedProofs).toHaveLength(choices); + expect( + checkTheoremProven( + generatedProofs, + completionContext, + environment + ) + ).toBeTruthy(); + } + ); } ); }