Clean-up

JetBrains-Research · Oct 17, 2024 · ad795e7 · ad795e7
1 parent 9125619
commit ad795e7
Showing 1 changed file with 0 additions and 49 deletions.
diff --git a/src/core/coqProofChecker.ts b/src/core/coqProofChecker.ts
@@ -1,6 +1,4 @@
 import { Mutex } from "async-mutex";
-// import { existsSync, unlinkSync, writeFileSync } from "fs";
-// import * as path from "path";
 import { Position } from "vscode-languageclient";
 
 import { CoqLspClientInterface } from "../coqLsp/coqLspClient";
@@ -65,53 +63,18 @@ export class CoqProofChecker implements CoqProofCheckerInterface {
         });
     }
 
-    // private buildAuxFileUri(
-    //     sourceDirPath: string,
-    //     holePosition: Position,
-    //     unique: boolean = true
-    // ): Uri {
-    //     const holeIdentifier = `${holePosition.line}_${holePosition.character}`;
-    //     const defaultAuxFileName = `hole_${holeIdentifier}_cp_aux.v`;
-    //     let auxFilePath = path.join(sourceDirPath, defaultAuxFileName);
-    //     if (unique && existsSync(auxFilePath)) {
-    //         const randomSuffix = Math.floor(Math.random() * 1000000);
-    //         auxFilePath = auxFilePath.replace(
-    //             /\_cp_aux.v$/,
-    //             `_${randomSuffix}_cp_aux.v`
-    //         );
-    //     }
-
-    //     return Uri.fromPath(auxFilePath);
-    // }
-
     private checkIfProofContainsAdmit(proof: Proof): boolean {
         return forbiddenAdmitTactics.some((tactic) => proof.includes(tactic));
     }
 
     private async checkProofsUnsafe(
         fileUri: Uri,
         documentVersion: number,
-        // sourceDirPath: string,
-        // sourceFileContentPrefix: string[],
         checkAtPosition: Position,
         proofs: Proof[]
     ): Promise<ProofCheckResult[]> {
-        // 1. Write the text to the aux file
-        // const auxFileUri = this.buildAuxFileUri(
-        //     sourceDirPath,
-        //     prefixEndPosition
-        // );
-        // const sourceFileContent = sourceFileContentPrefix.join("\n");
-        // writeFileSync(auxFileUri.fsPath, sourceFileContent);
-
         const results: ProofCheckResult[] = [];
-        // try {
-        // 2. Issue open text document request
-        // await this.coqLspClient.openTextDocument(fileUri);
-
-        // 3. Iterate over the proofs and сheck them
         for (const proof of proofs) {
-            // 3.1. Check if the proof contains admit
             if (this.checkIfProofContainsAdmit(proof)) {
                 results.push({
                     proof: proof,
@@ -121,7 +84,6 @@ export class CoqProofChecker implements CoqProofCheckerInterface {
                 continue;
             }
 
-            // 3.2 Check if proof is valid and closes the first goal
             const goalResult = await this.coqLspClient.getGoalsAtPoint(
                 checkAtPosition,
                 fileUri,
@@ -135,17 +97,6 @@ export class CoqProofChecker implements CoqProofCheckerInterface {
                 diagnostic: goalResult.err ? goalResult.val.message : undefined,
             });
         }
-        // } catch (error) {
-        //     console.log("Error in checkProofsUnsafe", error);
-        //     throw error;
-        // }
-        // finally {
-        // 4. Issue close text document request
-        // await this.coqLspClient.closeTextDocument(fileUri);
-
-        // 5. Remove the aux file
-        // unlinkSync(auxFileUri.fsPath);
-        // }
 
         return results;
     }