v1.4.3

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Change Log
 
+### 1.4.3
+- Tiny patch with shuffling of the hole array.
+
 ### 1.4.2
 - Now no need to add dot in the end of the tactic, when configuring a single tactic solver.
 - Automatic reload settings on change in the settings file. Not all settings are reloaded automatically, 

package.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/K-dizzled/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "1.4.2",
+  "version": "1.4.3",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -153,6 +153,11 @@
             "type": "boolean", 
             "default": true, 
             "markdownDescription": "Whether to use gpt as one of the used LLMs."
+          }, 
+          "coqpilot.shuffleHoles": {
+            "type": "boolean", 
+            "default": false, 
+            "markdownDescription": "Whether to shuffle the order of proving the holes."
           }
         }
       }

src/extension.ts

@@ -31,6 +31,7 @@ import { makeAuxfname } from "./coqLspClient/utils";
 import * as lspUtils from "./coqLspClient/utils";
 import { ProofStep } from "./lib/pvTypes";
 import * as utils from "./coqLspClient/utils";
+import { shuffleArray } from "./coqLlmInteraction/utils";
 
 export class Coqpilot implements Disposable {
 
@@ -214,6 +215,10 @@ export class Coqpilot implements Disposable {
     }
 
     async proveHoles(editor: TextEditor, holes: ProofStep[]) {
+        if (this.config.config.shuffleHoles) {
+            shuffleArray(holes);
+        }
+
         for (const hole of holes) {
             // Run proof generation at the start of the hole
             const position = lspUtils.toVPosition(hole.range.start);

src/extension/config.ts

@@ -18,6 +18,7 @@ export interface CoqpilotConfig {
     coqLspPath: string;
     useGpt: boolean;
     extraCommandsList: string[];
+    shuffleHoles: boolean;
 }
 
 export class CoqpilotConfigWrapper {
@@ -68,7 +69,8 @@ export namespace CoqpilotConfig {
                 parseFileOnInit: wsConfig.parseFileOnInit, 
                 coqLspPath: wsConfig.coqLspPath, 
                 useGpt: wsConfig.useGpt, 
-                extraCommandsList: preprocessExtraCommands(wsConfig.extraCommandsList)
+                extraCommandsList: preprocessExtraCommands(wsConfig.extraCommandsList),
+                shuffleHoles: wsConfig.shuffleHoles
             };
         } catch (error) {
             console.error(error);

src/test/mock/mockConfig.ts

@@ -12,7 +12,8 @@ export function mockConfig(): CoqpilotConfig {
         parseFileOnEditorChange: false,
         coqLspPath: "coq-lsp",
         useGpt: false, 
-        extraCommandsList: []
+        extraCommandsList: [], 
+        shuffleHoles: false
     };
 }
 
@@ -28,7 +29,8 @@ export function mockConfigRealGpt(apikey: string): CoqpilotConfig {
         parseFileOnEditorChange: false,
         coqLspPath: "coq-lsp",
         useGpt: true, 
-        extraCommandsList: []
+        extraCommandsList: [], 
+        shuffleHoles: false
     };
 }
 
@@ -44,6 +46,7 @@ export function simpleSolverMockConfig(tactics: string[]): CoqpilotConfig {
         parseFileOnEditorChange: false,
         coqLspPath: "coq-lsp",
         useGpt: false, 
-        extraCommandsList: tactics
+        extraCommandsList: tactics, 
+        shuffleHoles: false
     };
 }