Solve all admits

CHANGELOG.md

@@ -1,5 +1,9 @@
 # Change Log
 
+### 1.4.0
+- Add command to solve all admitted holes in the file.
+- Fixing bugs with coq-lsp behavior. 
+
 ### 1.3.1
 - Test coverage increased.
 - Refactoring client and ProofView.  

package.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/K-dizzled/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "1.3.0",
+  "version": "1.4.0",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -44,6 +44,10 @@
       {
         "command": "coqpilot.toggle",
         "title": "Coqpilot: Toggle the plugin"
+      }, 
+      {
+        "command": "coqpilot.prove_all_holes",
+        "title": "Coqpilot: Try to prove all holes (admitted goals) in the current file."
       }
     ],
     "configuration": [

src/coqLlmInteraction/interactor.ts

@@ -31,6 +31,10 @@ export class GenerationResult<T> {
         this.data = data;
     }
 
+    static editorError<T>(message: string | undefined = undefined): GenerationResult<T> {
+        return new GenerationResult<T>(GenerationStatus.exception, message ?? "Editor error.", "Editor");
+    }
+
     static success<T>(data: T): GenerationResult<T> {
         return new GenerationResult<T>(GenerationStatus.success, null, null, data);
     }
@@ -153,6 +157,8 @@ export class Interactor {
             return GenerationResult.exception(llmResponse.message, "Open-ai completion request");
         }
 
+        llmResponse = llmResponse.map(this.llmPrompt.removeBackticks);
+
         // Surround with curly braces and remove Proof. and Qed.
         llmResponse = llmResponse.map(this.llmPrompt.thrProofToBullet);
 

src/coqLlmInteraction/llmPromptInterface.ts

@@ -1,5 +1,6 @@
 import { Theorem } from "../lib/pvTypes";
 import { shuffleArray } from "./utils";
+import logger from '../extension/logger';
 
 class SeparatedTheorems {
     constructor(
@@ -50,6 +51,10 @@ export class LlmPromptBase {
         return (str.length / 4) >> 0;
     };
 
+    removeBackticks = (str: string): string => {
+        return str.replace(/`/g, '');
+    };
+
     thrProofToBullet = (proof: string): string => {
         // Remove "Proof." and "Qed."
         let res = proof.replace(/Proof using\./g, '')
@@ -60,7 +65,7 @@ export class LlmPromptBase {
     };
 
     cleanFromBrackets = (str: string): string => {
-        return str.slice(1, str.length - 1).trim();
+        return str.slice(2, str.length - 1).trim();
     };
 
     /**
@@ -113,7 +118,10 @@ export class LlmPromptBase {
             theoremsTokensSum -= this.countTokens(theorem.statement) + this.countTokens(theorem.proof.onlyText());
         }
 
-        return new SeparatedTheorems(admittedTheorems, provenTheorems);
+        const separated = new SeparatedTheorems(admittedTheorems, provenTheorems);
+        logger.info(`Admiited theorems: ${separated.admittedTheorems.map((th) => th.name)}`);
+        logger.info(`Training theorems: ${separated.trainingTheorems.map((th) => th.name)}`);
+        return separated;
     }
 
     getAdmittedTheorems(): string[] {

src/coqLspClient/flecheDocUtils.ts

@@ -91,6 +91,7 @@ function parseProof(
     const proof: ProofStep[] = [];
     let endPos: Range | null = null;
     let proofContainsAdmit = false;
+    let proofHoles: ProofStep[] = [];
 
     while (!proven && index < ast.length) {
         const span = ast[index];
@@ -111,22 +112,27 @@ function parseProof(
                 proofContainsAdmit = true;
             }
         } else {
+            const proofText = getTextInRange(span.range.start, span.range.end, lines);
             const proofStep = new ProofStep(
-                getTextInRange(span.range.start, span.range.end, lines),
+                proofText,
                 vernacType,
                 span.range
             );
 
             proof.push(proofStep);
             index += 1;
+
+            if (proofText.includes('admit')) {
+                proofHoles.push(proofStep);
+            }
         }
     }
 
     if (!proven || endPos === null) {
         throw new ProofViewError("Invalid or incomplete proof.");
     }
 
-    const proofObj = new TheoremProof(proof, endPos, proofContainsAdmit);
+    const proofObj = new TheoremProof(proof, endPos, proofContainsAdmit, proofHoles);
     return proofObj;
 }
 

src/coqLspClient/utils.ts

@@ -1,10 +1,12 @@
 import {
     Uri,
     Position as VPosition,
+    Range as VRange,
 } from 'vscode';
 
 import {
     Position,
+    Range
 } from "vscode-languageclient";
 
 import {
@@ -30,4 +32,8 @@ export function getTextBeforePosition(text: string, position: VPosition): string
 
 export function toVPosition(position: Position): VPosition {
     return new VPosition(position.line, position.character);
+}
+
+export function toVRange(range: Range): VRange {
+    return new VRange(toVPosition(range.start), toVPosition(range.end));
 }

src/editor/windowManager.ts

@@ -40,6 +40,12 @@ export function showSearchFailureMessage(theoremName: string) {
     );
 }
 
+export function showSearchFailureMessageHole(hole: vscode.Position) {
+    vscode.window.showInformationMessage(
+        `Coqpilot failed to find a proof for hole at line ${hole.line + 1}.`
+    );
+}
+
 export function showClientNotRunningMessage() {
     vscode.window.showInformationMessage(
         'Coqpilot is not running. Use the button in the bottom left corner to start it.'
@@ -77,9 +83,9 @@ export function showNoGoalMessage() {
     );
 }
 
-export function showSearchSucessMessage(editor: vscode.TextEditor, proof: string) {
+export function showSearchSucessMessage(editor: vscode.TextEditor, proof: string, position: vscode.Position) {
     editor.edit((editBuilder) => {
-        editBuilder.insert(editor.selection.active, proof);
+        editBuilder.insert(position, proof);
     });
 }
 

src/extension.ts

@@ -5,6 +5,7 @@ import {
     Disposable,
     TextEditor,
     window,
+    Position,
 } from "vscode";
 
 import {
@@ -18,11 +19,16 @@ import { LLMPrompt } from "./coqLlmInteraction/llmPromptInterface";
 import { CoqPromptKShot } from "./coqLlmInteraction/coqLlmPrompt";
 import { LLMInterface } from "./coqLlmInteraction/llmInterface";
 import { CoqpilotConfig } from "./extension/config";
-import { Interactor, GenerationStatus } from "./coqLlmInteraction/interactor";
+import { 
+    Interactor, 
+    GenerationStatus, 
+    GenerationResult, 
+} from "./coqLlmInteraction/interactor";
 import * as wm from "./editor/windowManager";
 import { VsCodeSpinningWheelProgressBar } from "./extension/vscodeProgressBar";
 import logger from "./extension/logger";
 import { makeAuxfname } from "./coqLspClient/utils";
+import * as lspUtils from "./coqLspClient/utils";
 
 export class Coqpilot implements Disposable {
 
@@ -56,6 +62,7 @@ export class Coqpilot implements Disposable {
         this.registerCommand("toggle", this.toggleLspClient.bind(this));
         this.registerEditorCommand("init_history", this.initHistory.bind(this));
         this.registerEditorCommand("run_generation", this.runGeneration.bind(this));
+        this.registerEditorCommand("prove_all_holes", this.runProveAllAdmitted.bind(this));
 
         this.context.subscriptions.push(this);
     }
@@ -139,30 +146,32 @@ export class Coqpilot implements Disposable {
         this.context.subscriptions.push(this.proofView);
     }
 
-    async runGeneration(editor: TextEditor) {
+    private async generateAtPoint(
+        editor: TextEditor, 
+        position: Position
+    ): Promise<GenerationResult<string>> {
         if (this.config.openaiApiKey === "None") {
-            wm.showApiKeyNotProvidedMessage(); return;
+            wm.showApiKeyNotProvidedMessage(); return GenerationResult.editorError();
         } else if (editor.document.languageId !== "coq") {
-            wm.showIncorrectFileFormatMessage(); return;
+            wm.showIncorrectFileFormatMessage(); return GenerationResult.editorError();
         } else if (!this.client.isRunning()) {
-            wm.showClientNotRunningMessage(); return;
+            wm.showClientNotRunningMessage(); return GenerationResult.editorError();
         }
 
         const auxFile = makeAuxfname(editor.document.uri);
-        const cursorPos = editor.selection.active;
         const auxThr = await this.proofView.getAuxTheoremAtCurPosition(
-            auxFile, editor.document.getText(), cursorPos
+            auxFile, editor.document.getText(), position
         );
 
         if (!auxThr) {
             wm.showNoGoalMessage();
-            return;
+            return GenerationResult.editorError();
         }
 
         const [thrStatement, thrName] = auxThr;
         if (!this.llmPrompt) {
             wm.fileSnapshotRequired();
-            return;
+            return GenerationResult.editorError();
         }
 
         const progressBar = new VsCodeSpinningWheelProgressBar();
@@ -181,18 +190,52 @@ export class Coqpilot implements Disposable {
             this.proofView.checkTheorems.bind(this.proofView)
         );
 
+        return proof;
+    }
+
+    async runGeneration(editor: TextEditor) {
+        const proof = await this.generateAtPoint(editor, editor.selection.active);
         switch (proof.status) {
             case GenerationStatus.success:
-                wm.showSearchSucessMessage(editor, proof.data);
+                wm.showSearchSucessMessage(editor, proof.data, editor.selection.active);
                 break;
             case GenerationStatus.searchFailed:
-                wm.showSearchFailureMessage(thrName);
+                wm.showSearchFailureMessageHole(editor.selection.active);
                 break; 
             default:
                 wm.showExceptionMessage(proof.toString());
                 break;
         }
+    }
 
+    async runProveAllAdmitted(editor: TextEditor) {
+        await this.initHistory(editor);
+        const admittedTheorems = this.llmPrompt?.admittedTheorems;
+        const proofHoles = admittedTheorems.map((thr) => thr.proof.holes).flat();
+        logger.info(`Proof holes: ${proofHoles.map((hole) => `${hole.range.start.line} ${hole.range.start.character}`).join(", ")}`);
+        for (const hole of proofHoles) {
+            // Run proof generation at the start of the hole
+            const position = lspUtils.toVPosition(hole.range.start);
+            const proof = await this.generateAtPoint(editor, position);
+            switch (proof.status) {
+                case GenerationStatus.success:
+                    // Remove the text of the hole from the editor
+                    const range = lspUtils.toVRange(hole.range);
+                    await editor.edit((editBuilder) => {
+                        editBuilder.delete(range);
+                    });
+
+                    const inlinedProof = proof.data.replace(/\n/g, " ");
+                    wm.showSearchSucessMessage(editor, inlinedProof, position);
+                    break;
+                case GenerationStatus.searchFailed:
+                    wm.showSearchFailureMessageHole(position);
+                    break; 
+                default:
+                    wm.showExceptionMessage(proof.toString());
+                    break;
+            }
+        }
     }
 
     toggleLspClient() {

src/lib/pvTypes.ts

@@ -124,6 +124,7 @@ export class TheoremProof {
         public proof_steps: ProofStep[],
         public end_pos: Range,
         public is_incomplete: boolean, 
+        public holes: ProofStep[], 
     ) { }
 
     public toString(): string {

src/test/coqLlmInteractionTests/proofView.test.ts

@@ -99,7 +99,6 @@ suite('ProofView auxTheorem tests', () => {
             const proofView = new ProofView(client, statusItem); 
 
             for (let i = 0; i < goals.length; i++) {
-                console.log("DEBUG: ", auxFile, text, positions[i], i);
                 const auxThr = await proofView.getAuxTheoremAtCurPosition(
                     auxFile, text, positions[i]
                 );