Add test for single-tactic solver

package.json

@@ -20,6 +20,20 @@
   ],
   "main": "./out/mainNode.js",
   "contributes": {
+    "languages": [
+      {
+        "id": "coq",
+        "aliases": [
+          "Coq",
+          "coq",
+          "Gallina",
+          "gallina"
+        ],
+        "extensions": [
+          ".v"
+        ]
+      }
+    ],
     "commands": [
       {
         "command": "coqpilot.init_history",

src/test/coqLlmInteractionTests/simpleSolver.test.ts

@@ -0,0 +1,52 @@
+import { 
+    workspace, 
+    commands, 
+    window, 
+    languages,
+    Range
+} from 'vscode';
+
+import * as path from 'path';
+import * as assert from 'assert';
+import * as common from '../common';
+
+suite('Simple single-tactic solver tests', () => {
+    const dirname = path.dirname(path.dirname(path.dirname(__dirname)));
+
+	test('Check prove using simple single-tactic prover', async () => {
+        const { filePath, tacticsToTry, solvedAmount } = {
+            filePath: path.join(dirname, 'src', 'test', 'resources', 'with_admits_test.v'),
+            tacticsToTry: ['auto.'], 
+            solvedAmount: 6, 
+        };
+
+        // change the setting of useGpt to false
+        await workspace.getConfiguration("coqpilot").update('useGpt', false);
+        await workspace.getConfiguration("coqpilot").update('extraCommandsList', tacticsToTry);
+
+        // vscode open filePath
+        const doc = await workspace.openTextDocument(filePath);
+        await window.showTextDocument(doc);
+        await languages.setTextDocumentLanguage(doc, "coq");
+
+        const text = doc.getText();
+        const admitsBeforeGeneration = text.match(/admit./g)?.length ?? 0;
+
+        await commands.executeCommand('coqpilot.init_history');
+        await common.sleep(2000);
+
+        await commands.executeCommand('coqpilot.prove_all_holes');
+        await common.sleep(5000);
+
+        // get the difference between document versions
+        const admitsAfterGeneration = window.activeTextEditor?.document.getText().match(/admit./g)?.length ?? 0;
+        const admitsDifference = admitsBeforeGeneration - admitsAfterGeneration;
+
+        // modify text back to original
+        await window.activeTextEditor?.edit(editBuilder => {
+            editBuilder.replace(new Range(0, 0, doc.lineCount, 0), text);
+        });
+
+        assert.strictEqual(admitsDifference, solvedAmount);
+    }).timeout(15000);
+});

src/test/resources/.vscode/settings.json

@@ -0,0 +1,15 @@
+{
+    "files.exclude": {
+        "**/*.vo": true,
+        "**/*.vok": true,
+        "**/*.vos": true,
+        "**/*.aux": true,
+        "**/*.glob": true,
+        "**/.git": true,
+        "**/.svn": true,
+        "**/.hg": true,
+        "**/CVS": true,
+        "**/.DS_Store": true,
+        "**/Thumbs.db": true
+    }
+}

src/test/resources/with_admits_test.v

@@ -0,0 +1,39 @@
+Theorem test : forall (A : Type) (P : A -> Prop) (x : A), P x -> P x.
+Proof.
+    (* auto. *)
+    admit.
+Admitted.
+
+Theorem test2 : forall (A : Type) (P : A -> Prop) (x : A), P x -> P x.
+Proof.
+    intros A P x H.
+    (* auto. *)
+    admit.
+Admitted.
+
+Theorem test2nat : forall n : nat, n = 0 \/ n <> 0.
+Proof.
+    intros n.
+    destruct n.
+    {
+        (* auto. *)
+        admit.
+    }
+    {
+        admit.
+    }
+Admitted.
+
+Theorem test_thr : forall n:nat, 0 + n = n.
+Proof.
+    intros n. Print plus.
+    (* auto. *)
+    admit.
+Admitted.
+
+Lemma test_thr1 : forall n:nat, 0 + n + 0 = n.
+Proof.
+    intros n. Print plus.
+    (* now rewrite <- plus_n_O. *)
+    admit.
+Admitted.