Release v2.2.6+0.1.8+8.19

Merge pull request #38 from JetBrains-Research/v2.3.0-dev

Author: K-dizzled

CHANGELOG.md

@@ -1,5 +1,16 @@
 # Changelog
 
+## 2.2.6
+
+### Public changes
+
+- Allow manually modifying the location of the `coq-lsp` executable in the settings. This is useful when the `coq-lsp` executable is not in the PATH. Alongside, correctly handle the case when the `coq-lsp` executable is not found.
+- Improve proof extraction from the LLM services for proofs, containing `Proof using X Y Z.` and similar constructs. Improve the handling of the obfuscatedly generated proofs by small language models, such as `LLaMA` through `LMStudio`.
+- Add a hotkey for solving admits inside selection: `ctrl+shift+[BracketRight]` on Windows and Linux, `shift+cmd+[BracketRight]` on MacOS.
+
+### Internal changes
+- Update private headers, sent to JetBrains-AI services, to identify the client as CoqPilot.
+
 ## 2.2.5
 
 - Contribute the new benchmarking report for 300 theorems. 

README.md

@@ -11,7 +11,7 @@
 - 🔍 [Brief Technical Overview](#brief-technical-overview)
 - 💡 [Example Usage](#example-usage)
 - 🛠 [Installation](#installation)
-  - ▶️ [Coq-lsp Installation](#coq-lsp-installation)
+  - ▶️ [Coq-LSP Installation](#coq-lsp-installation)
   - 🤖 [Building Locally](#building-locally)
 - ⚠️ [Important Information](#important)
 - ⚙️ [Extension Settings](#extension-settings)
@@ -62,16 +62,18 @@ As soon as at least one valid proof is found, it is substituted in the editor an
 
 ## Installation
 
-### Coq-lsp installation
+### Coq-LSP installation
 
-To make the extension running you will have to install `coq-lsp` server. You can install it using opam: 
+To run the extension, you must install a `coq-lsp` server. Depending on the system used in your project, you should install it using `opam` or `nix`. A well-configured `nix` project should have the `coq-lsp` server installed as a dependency. To install `coq-lsp` using `opam`, you can use the following commands: 
 ```bash
 opam pin add coq-lsp 0.1.8+8.19.0
 opam install coq-lsp
 ```
 For more information on how to install `coq-lsp` please refer to [coq-lsp](https://github.com/ejgallego/coq-lsp). 
 
-With coq-lsp, extension should have everything it needs to run.
+Either way around, if the [coq-lsp](https://github.com/ejgallego/coq-lsp) extension works well and you can see the goals and theorems in the VSCode, then `CoqPilot` should work as well. However, using [coq-lsp](https://github.com/ejgallego/coq-lsp) as a plugin for Coq support is not mandatory for `CoqPilot` to work.
+
+If your installation of `coq-lsp` is not in the default path, you can specify the path to the `coq-lsp` server in the settings using the `coqpilot.coqLspServerPath` setting. Default value should work well for most of the cases.
 
 ### Building locally
 
@@ -93,7 +95,7 @@ npm install
 npm run compile
 ```
 
-To run the extension from the vscode, you can press `F5` or click on `Run extension` in the `Run and Debug` section. It will open a new window with the extension running.
+To run the extension from the VSCode, you can press `F5` or click on `Run extension` in the `Run and Debug` section. It will open a new window with the extension running.
 
 To run all tests properly (i.e. with rebuilding the resources and the code first), execute the following task:
 ```bash
@@ -111,20 +113,21 @@ The extension's architecture overview is stored in the [ARCHITECTURE.md](https:/
 CoqPilot generates aux files with `_cp_aux.v` suffix. Sometimes when generation fails with exception, it is possible that such file will not be deleted. When a project is open, extension shall show a window that asks if you want to add such files to the local project gitignore. 
 
 Moreover, this repository contains a script for your convenience that adds the format of such files to the global gitignore file on your system.  
-- Copy the [`set_gitignore.sh`](https://github.com/K-dizzled/coqpilot/blob/main/set_gitignore.sh) file to your computer. Then: 
+- Copy the [`set_gitignore.sh`](https://github.com/JetBrains-Research/coqpilot/blob/main/set_gitignore.sh) file to your computer. Then: 
 ```bash 
 chmod +x set_gitignore.sh
 ./set_gitignore.sh
 ```
 It will add the format of CoqPilot aux files to your global gitignore file on the system, so that even if CoqPilot forgets to clean files up, they will not be marked as new files in git.
-Comment: Such files are not visible in the vscode explorer, because plugin adds them to the `files.exclude` setting on startup.
+Comment: Such files are not visible in the VSCode explorer, because plugin adds them to the `files.exclude` setting on startup.
 
 ## Extension Settings
 
 This extension contributes the following settings:
 
 * `coqpilot.contextTheoremsRankerType` : The type of theorems ranker that will be used to select theorems for proof generation (when context is smaller than taking all of them). Either randomly, by Jacard index (similarity metric) or by distance from the theorem, with the currently observed admit. 
 * `coqpilot.loggingVerbosity` : Verbosity of the logs. Could be `info`, `debug`.
+* `coqpilot.coqLspServerPath` : Path to the coq-lsp server. By default, it is set to `coq-lsp`.
 
 * `coqpilot.predefinedProofsModelsParameters`, `coqpilot.openAiModelsParameters`, `coqpilot.grazieModelsParameters` and `coqpilot.lmStudioModelsParameters`:
 
@@ -227,11 +230,11 @@ First things first, the process of running the benchmark is not perfectly automa
     cachix use weakmemory
     ```
 
-3. Go to the `imm` subdirectory, apply the nix environment (without it the project will NOT build) and build the project: 
+3. Go to the `imm` subdirectory, apply the nix environment (without it the project will **NOT** build) and build the project: 
     ```bash
     cd dataset/imm 
-    nix-build
     nix-shell 
+    make
     ```
 4. Make sure the `_CoqProject` was successfully generated in the root of your project. Return to the project root not exiting the nix-shell. Run the benchmark: 
     ```bash

package-lock.json

@@ -1,14 +1,14 @@
 {
   "name": "coqpilot",
-  "displayName": "Сoqpilot",
+  "displayName": "СoqPilot",
   "description": "An ai based completion extension for Coq interactive prover.",
   "icon": "etc/img/logo.ico",
   "repository": {
     "type": "git",
-    "url": "https://github.com/K-dizzled/coqpilot"
+    "url": "https://github.com/JetBrains-Research/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "2.2.5",
+  "version": "2.2.6",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -37,15 +37,22 @@
     "commands": [
       {
         "command": "coqpilot.perform_completion_under_cursor",
-        "title": "Coqpilot: Try to generate proof for the goal under the cursor"
+        "title": "CoqPilot: Try to generate proof for the goal under the cursor"
       },
       {
         "command": "coqpilot.perform_completion_for_all_admits",
-        "title": "Coqpilot: Try to prove all holes (admitted goals) in the current file"
+        "title": "CoqPilot: Try to prove all holes (admitted goals) in the current file"
       },
       {
         "command": "coqpilot.perform_completion_in_selection",
-        "title": "Coqpilot: Try to prove holes (admitted goals) in the selection"
+        "title": "CoqPilot: Try to prove holes (admitted goals) in the selection"
+      }
+    ],
+    "keybindings": [
+      {
+        "command": "coqpilot.perform_completion_in_selection",
+        "key": "ctrl+shift+[BracketRight]",
+        "mac": "shift+cmd+[BracketRight]"
       }
     ],
     "menus": {
@@ -107,7 +114,7 @@
                 },
                 "modelName": {
                   "type": "string",
-                  "markdownDescription": "Model to use from the OpenAI platform. List of models known to Coqpilot: \n * gpt-4o \n * gpt-4o-2024-05-13 \n * gpt-4-turbo \n * gpt-4-turbo-2024-04-09 \n * gpt-4-turbo-preview \n * gpt-4-0125-preview \n * gpt-4-1106-preview \n * gpt-4-vision-preview \n * gpt-4-1106-vision-preview \n * gpt-4 \n * gpt-4-0314 \n * gpt-4-0613 \n * gpt-4-32k \n * gpt-4-32k-0314 \n * gpt-4-32k-0613 \n * gpt-3.5-turbo-0125 \n * gpt-3.5-turbo \n * gpt-3.5-turbo-1106 \n * gpt-3.5-turbo-instruct \n * gpt-3.5-turbo-16k \n * gpt-3.5-turbo-16k-0613 \n * gpt-3.5-turbo-0613 \n * gpt-3.5-turbo-0301",
+                  "markdownDescription": "Model to use from the OpenAI platform. List of models known to CoqPilot: \n * gpt-4o \n * gpt-4o-2024-05-13 \n * gpt-4-turbo \n * gpt-4-turbo-2024-04-09 \n * gpt-4-turbo-preview \n * gpt-4-0125-preview \n * gpt-4-1106-preview \n * gpt-4-vision-preview \n * gpt-4-1106-vision-preview \n * gpt-4 \n * gpt-4-0314 \n * gpt-4-0613 \n * gpt-4-32k \n * gpt-4-32k-0314 \n * gpt-4-32k-0613 \n * gpt-3.5-turbo-0125 \n * gpt-3.5-turbo \n * gpt-3.5-turbo-1106 \n * gpt-3.5-turbo-instruct \n * gpt-3.5-turbo-16k \n * gpt-3.5-turbo-16k-0613 \n * gpt-3.5-turbo-0613 \n * gpt-3.5-turbo-0301",
                   "default": "gpt-3.5-turbo-0301"
                 },
                 "temperature": {
@@ -132,12 +139,12 @@
                 },
                 "maxTokensToGenerate": {
                   "type": "number",
-                  "description": "Number of tokens that the model is allowed to generate as a response message (i.e. message with proof). For known models, Coqpilot provides a recommended default value, but it can be customized for more advanced proof generation. The default value is the maximum allowed value for the model if it takes no more than half of `tokensLimit`, otherwise the minimum of half of `tokensLimit` and 4096.",
+                  "description": "Number of tokens that the model is allowed to generate as a response message (i.e. message with proof). For known models, CoqPilot provides a recommended default value, but it can be customized for more advanced proof generation. The default value is the maximum allowed value for the model if it takes no more than half of `tokensLimit`, otherwise the minimum of half of `tokensLimit` and 4096.",
                   "default": 2048
                 },
                 "tokensLimit": {
                   "type": "number",
-                  "description": "Total length of input and generated tokens, it is determined by the model. For known models, Coqpilot provides a recommended default value (the maximum model context length), but it can be customized for more advanced proof generation.",
+                  "description": "Total length of input and generated tokens, it is determined by the model. For known models, CoqPilot provides a recommended default value (the maximum model context length), but it can be customized for more advanced proof generation.",
                   "default": 4096
                 },
                 "multiroundProfile": {
@@ -358,6 +365,12 @@
             "description": "The verbosity of the logs.",
             "default": "info",
             "order": 5
+          },
+          "coqpilot.coqLspServerPath": {
+            "type": "string",
+            "description": "Path to the Coq LSP server. If not specified, CoqPilot will try to find the server automatically at the default location: coq-lsp at PATH.",
+            "default": "coq-lsp",
+            "order": 6
           }
         }
       }