Merge pull request #5 from K-dizzled/ui_improvements

UI/UX improvements

.github/workflows/coqpilot.yml

@@ -68,4 +68,19 @@ jobs:
       env:
           COQ_LSP_PATH: ${{ env.coqlsppath }}
       run: npm test -- -ex='simpleSolver.test.js'
-      if: runner.os != 'Linux'
+      if: runner.os != 'Linux'
+
+  create-release:
+    runs-on: ubuntu-latest
+    needs: [build]
+    if: github.ref == 'refs/heads/main'
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16.x
+      - name: Publish to Visual Studio Marketplace
+        uses: HaaLeo/publish-vscode-extension@v1
+        with:
+          pat: ${{ secrets.VSCE_ACCESS_TOKEN }}
+          registryUrl: https://marketplace.visualstudio.com

CHANGELOG.md

@@ -1,5 +1,12 @@
 # Change Log
 
+### 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, 
+but the most ones are. The ones that are not automatically reloaded: `useGpt`, `coqLspPath`, `parseFileOnInit`.
+- Added command that solves admits in selected region. Also added that command to the context menu (right click in the editor).
+- Fix toggle extension. 
+
 ### 1.4.1
 - Add a possibility to configure a single tactic solver.
 

README.md

@@ -12,13 +12,19 @@ Now `coqpilot` is in early beta and seeks for feedbacks. Please feel free to ope
 
 `Coqpilot` could be run to analyse the opened `coq` file, fetch proofs of successfully typechecked theorems inside it, parse them and use as a message history to present to LLM.
 
-Later on, on demand, it could perform a request to an LLM with an admitted theorem and a message history and get a list of potential proofs. It then uses `coq-lsp` to typecheck them and substitute the first valid proof in the editor.
+Later on, on demand, it could perform a request to an LLM with an admitted theorem and a message history and get a list of potential proofs. It then uses `coq-lsp` to typecheck them and substitute the first valid proof in the editor. Moreover, coqpilot was designed to fetch multiple LLMs, so that many ways of proof generation could be used at once. Right now, apart from GPT, coqpilot also tries substituting single-line proofs from the `coqpilot.extraCommandsList` setting. 
 
 User can:
 - Run `coqpilot` at a given cursor point inside theorem to try substitute the current goal.
 
 <img src="./etc/gif/prove-goal.gif"/> 
 
+- Run `coqpilot` with some chosen selection to try substitute all admits in this selection.
+
+<img src="./etc/gif/solve-in-selection.gif"/>
+
+- Run `coqpilot` to try substitute all admits in the file.
+
 ## Requirements
 
 * `coq-lsp` version 0.1.7 is currently required to run the extension.
@@ -56,18 +62,30 @@ This extension contributes the following settings:
 * `coqpilot.logFolderPath`: A path to the folder where logs should be saved. If `None` is specified and logAttemps is `true` then logs will be saved in the `coqpilot` plugin folder in the `logs` subfolder.
 * `coqpilot.parseFileOnInit`: Whether to start parsing the file into message history on extension startup.
 * `coqpilot.parseFileOnEditorChange`: Whether to start re-parsing the file each time the editor has changed.
+* `coqpilot.extraCommandsList`: A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment. Might or might not end with a dot, if it does not, then a dot will be added automatically.
+* `coqpilot.coqLspPath`: Path to the coq-lsp binary, by default, search in PATH.
+* `coqpilot.useGpt`: Whether to use gpt as one of the used LLMs. Right now otherwise only single tactics would be used to generate proofs. 
+
+**REMARK**: `useGpt`, `coqLspPath`, `parseFileOnInit` are NOT auto reloaded on setting change, they need plugin restart. 
 
 ## Contributed Commands
 
 * `coqpilot.init_history`: Parse current file and initialize llm gistory with theorems from it.
 * `coqpilot.run_generation`: Try to generate proof for the goal under the cursor.
+* `coqpilot.toggle`: Toggle the plugin.
+* `coqpilot.prove_all_holes`: Try to prove all holes (admitted goals) in the current file.
+* `coqpilot.prove_in_selection`: Try to prove holes in selection.
 
 ## Planned Features
 
-It is planned to implement a proof repair feature for the proofs which will establish a dialogue between `coq-lsp` and the LLM. When LLM generates an incorrect proof, the error would be sent to LLM as a next message and the process would be repeated until a valid proof is found or the limit of attempts is reached.
+### Milestone 2.0.0
+
+It is planned to implement a proof repair feature for the proofs which will establish a dialogue between `coq-lsp` and the LLM. When LLM generates an incorrect proof, the error would be sent to LLM as a next message and the process would be repeated until a valid proof is found or the limit of attempts is reached. Also it is planned to fetch proofs from different LLMs not at once in the beggining, but asynchronously and one by one, if it fails to find a proof in the first LLM, it will try the next one.
 
 ## Release Notes
 
+More detailed release notes could be found in the [CHANGELOG.md](https://github.com/K-dizzled/coqpilot/blob/main/CHANGELOG.md) file.
+
 ### 1.1.0
 
 Now proof generation could be run in any position inside the theorem. There is no need to retake file snapshot after each significant file change. 

package.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/K-dizzled/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "1.4.1",
+  "version": "1.4.2",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -43,31 +43,28 @@
         "command": "coqpilot.run_generation",
         "title": "Coqpilot: Try to generate proof for the goal under the cursor."
       },
-      {
-        "command": "coqpilot.coq-lsp.restart",
-        "title": "Coqpilot: Restart the underlying coq-lsp server."
-      },
-      {
-        "command": "coqpilot.coq-lsp.toggle",
-        "title": "Coqpilot: Toggle the underlying coq-lsp server."
-      },
-      {
-        "command": "coqpilot.coq-lsp.stop",
-        "title": "Coqpilot: Stop the coq-lsp server."
-      },
       {
         "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."
-      }, 
+      },
       {
-        "command": "coqpilot.reload_config", 
-        "title": "Reload the settings (trigger this if you have changed the settings after plugin start and want to see the updates)."
+        "command": "coqpilot.prove_in_selection",
+        "title": "Coqpilot: Try to prove holes in selection."
       }
     ],
+    "menus": {
+      "editor/context": [
+        {
+          "command": "coqpilot.prove_in_selection",
+          "when": "editorTextFocus && editorHasSelection && resourceLangId == coq",
+          "group": "queries"
+        }
+      ]
+    },
     "configuration": [
       {
         "type": "object",
@@ -131,7 +128,7 @@
           },
           "coqpilot.parseFileOnInit": {
             "type": "boolean",
-            "default": true,
+            "default": false,
             "markdownDescription": "Whether to start parsing the file into message history on extension startup."
           },
           "coqpilot.parseFileOnEditorChange": {
@@ -145,7 +142,7 @@
               "type": "string"
             },
             "default": [],
-            "markdownDescription": "A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment and must finish with a dot."
+            "markdownDescription": "A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment."
           },
           "coqpilot.coqLspPath": {
             "type": "string",

src/coqLlmInteraction/gpt35.ts

@@ -2,24 +2,32 @@ import { LLMInterface } from "./llmInterface";
 import { LLMPrompt } from "./llmPromptInterface";
 import OpenAI from 'openai';
 import logger from "../extension/logger";
+import { CoqpilotConfigWrapper } from "../extension/config";
 
 type GptRole = "function" | "user" | "system" | "assistant";
 
 export class GPT35 implements LLMInterface {
     history: { role: GptRole; content: string; }[];
-    readonly apiKey: string;
     readonly requestAttempts: number;
-    readonly model: string;
+    readonly config: CoqpilotConfigWrapper;
     openai: OpenAI;
+    apiKey: string;
 
-    constructor(apiKey: string, requestAttempts: number = 3, model: string = "gpt-3.5-turbo-0301") {
-        this.apiKey = apiKey;
+    constructor(config: CoqpilotConfigWrapper, requestAttempts: number = 3) {
+        this.config = config;
         this.requestAttempts = requestAttempts;
-        this.model = model;
         this.history = [];
+        this.apiKey = config.config.openaiApiKey;
         this.openai = new OpenAI({ apiKey: this.apiKey });
     }
 
+    private updateOpenAi() {
+        if (this.config.config.openaiApiKey !== this.apiKey) {
+            this.apiKey = this.config.config.openaiApiKey;
+            this.openai = new OpenAI({ apiKey: this.apiKey });
+        }
+    }
+
     initHistory(llmPrompt: LLMPrompt): void {
         this.history = [];
         const prompt = llmPrompt.getSystemMessage();
@@ -34,6 +42,7 @@ export class GPT35 implements LLMInterface {
     }
 
     async sendMessageWithoutHistoryChange(message: string, choices: number): Promise<string[]> {
+        this.updateOpenAi();
         let attempts = this.requestAttempts;
         let completion = null;
         logger.info("Start sending message to open-ai");
@@ -42,7 +51,7 @@ export class GPT35 implements LLMInterface {
                 logger.info("Sending request with history: " + JSON.stringify(this.history.concat([{role: "user", content: message}])));
                 completion = await this.openai.chat.completions.create({
                     messages: this.history.concat([{role: "user", content: message}]),
-                    model: this.model,
+                    model: this.config.config.gptModel,
                     n: choices
                 });
                 logger.info("Request to open-ai succeeded");

src/coqLlmInteraction/singleTacticSolver.ts

@@ -1,19 +1,20 @@
 import { LLMInterface } from "./llmInterface";
 import { LlmPromptInterface } from "./llmPromptInterface";
+import { CoqpilotConfigWrapper } from "../extension/config";
 
 export class SingleTacticSolver implements LLMInterface {
-    private tactics: string[];
+    private configWrapped: CoqpilotConfigWrapper; 
 
-    constructor(tactics: string[]) {
-        this.tactics = tactics;
+    constructor(configWrapped: CoqpilotConfigWrapper) {
+        this.configWrapped = configWrapped;
     }
 
     initHistory(_llmPrompt: LlmPromptInterface): void {
         // Do nothing
     }
 
     async sendMessageWithoutHistoryChange(_message: string, _choices: number): Promise<string[]> {
-        return this.tactics.map((tactic) => {
+        return this.configWrapped.config.extraCommandsList.map((tactic) => {
             return `Proof. ${tactic} Qed.`;
         });
     }

src/coqLspClient/coqLspClient.ts

@@ -13,15 +13,15 @@ import {
 import logger from "../extension/logger";
 import { CoqLspServerConfig } from "./config";
 import { StatusBarButton } from "../editor/enableButton";
-import { CoqpilotConfig } from "../extension/config";
+import { CoqpilotConfigWrapper } from "../extension/config";
 
 export class CoqLspClient extends LanguageClient {
     private statusItem: StatusBarButton;
 
     constructor(
         statusItem: StatusBarButton, 
         wsConfig: WorkspaceConfiguration, 
-        extensionConfig: CoqpilotConfig,
+        extensionConfig: CoqpilotConfigWrapper,
         path?: Uri
     ) {
         const initializationOptions = CoqLspServerConfig.create();
@@ -36,7 +36,7 @@ export class CoqLspClient extends LanguageClient {
             markdown: { isTrusted: true, supportHtml: true },
             middleware: {
                 handleDiagnostics: (uri, diagnostics, _next) => {
-                    logger.info(`Diagnostics received for file ${uri}: ${diagnostics.map((d) => d.message).join(", ")}`);
+                    logger.debug(`Diagnostics received for file ${uri}: ${diagnostics.map((d) => d.message).join(", ")}`);
                 }
             }
         };
@@ -52,13 +52,14 @@ export class CoqLspClient extends LanguageClient {
             };
         }
 
+        const extConfig = extensionConfig.config;
         const serverOptions: ServerOptions = {
-            command: extensionConfig.coqLspPath,
+            command: extConfig.coqLspPath,
             args: wsConfig.args,
         };
 
         super(
-            extensionConfig.coqLspPath,
+            extConfig.coqLspPath,
             "Coq LSP Server",
             serverOptions,
             clientOptions