Make needsTheoremInitialGoals required

JetBrains-Research · Nov 26, 2024 · 35130f8 · 35130f8
1 parent 7dcd906
commit 35130f8
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 7 deletions.
diff --git a/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts b/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts
@@ -104,7 +104,8 @@ export namespace ParseCoqProjectImpl {
             mockDocumentVersion,
             Uri.fromPath(filePath),
             coqLspClient,
-            new AbortController().signal // abort behaviour is not supported at the parsing stage
+            new AbortController().signal, // abort behaviour is not supported at the parsing stage
+            true // TODO: pass `ContextTheoremsRanker.needsUnwrappedNotations` here to improve performance
         );
         const serializedParsedFile: SerializedParsedCoqFile = {
             serializedTheoremsByNames: packIntoMappedObject(

diff --git a/src/core/inspectSourceFile.ts b/src/core/inspectSourceFile.ts
@@ -18,7 +18,7 @@ export async function inspectSourceFile(
     fileUri: Uri,
     client: CoqLspClient,
     abortSignal: AbortSignal,
-    needsTheoremInitialGoals: boolean = true,
+    needsTheoremInitialGoals: boolean,
     eventLogger?: EventLogger
 ): Promise<AnalyzedFile> {
     const sourceFileEnvironment = await createSourceFileEnvironment(
@@ -82,7 +82,7 @@ export async function createSourceFileEnvironment(
     fileUri: Uri,
     client: CoqLspClient,
     abortSignal: AbortSignal,
-    needsTheoremInitialGoals: boolean = true,
+    needsTheoremInitialGoals: boolean,
     eventLogger?: EventLogger
 ): Promise<SourceFileEnvironment> {
     const fileTheorems = await parseCoqFile(

diff --git a/src/test/commonTestFunctions/prepareEnvironment.ts b/src/test/commonTestFunctions/prepareEnvironment.ts
@@ -46,7 +46,8 @@ export async function withPreparedEnvironment<T>(
                     (_hole) => true,
                     fileUri,
                     client,
-                    new AbortController().signal
+                    new AbortController().signal,
+                    true // to support any ranker
                 )
             );
         const preparedEnvironment = {

diff --git a/src/test/legacyBenchmark/benchmarkingFramework.ts b/src/test/legacyBenchmark/benchmarkingFramework.ts
@@ -40,6 +40,7 @@ import { consoleLog, consoleLogSeparatorLine } from "./utils/loggingUtils";
 
 export interface TestBenchmarkOptions extends TestBenchmarkOptionsWithDefaults {
     filePath: string;
+    // TODO: support ranker
     inputModelsParams: InputModelsParams;
     relativePathToFile: string;
 }
@@ -451,7 +452,8 @@ async function prepareForBenchmarkCompletions(
             mockDocumentVersion,
             shouldCompleteHole,
             fileUri,
-            coqLspClient
+            coqLspClient,
+            true // TODO: pass `ranker.needsUnwrappedNotations` here
         );
     const llmServices: LLMServices = {
         openAiService: new OpenAiService(eventLogger),
@@ -479,14 +481,16 @@ async function extractCompletionTargets(
     documentVersion: number,
     shouldCompleteHole: (hole: ProofStep) => boolean,
     fileUri: Uri,
-    client: CoqLspClient
+    client: CoqLspClient,
+    rankerNeedsUnwrappedNotations: boolean
 ): Promise<[BenchmarkingCompletionTargets, SourceFileEnvironment]> {
     const abortController = new AbortController();
     const sourceFileEnvironment = await createSourceFileEnvironment(
         documentVersion,
         fileUri,
         client,
-        abortController.signal
+        abortController.signal,
+        rankerNeedsUnwrappedNotations
     );
     const completionTargets = await createCompletionTargets(
         documentVersion,