Release v2.4.0+0.2.2+8.19

Merge pull request #50 from JetBrains-Research/v2.4.0-dev

.github/workflows/build-and-test.yml

@@ -20,7 +20,7 @@ on:
 
 env: 
   coqlsp-path: "coq-lsp"
-  coqlsp-version: "0.1.9+8.19"
+  coqlsp-version: "0.2.2+8.19"
   artifact-name: ubuntu-latest-build
 
 jobs:
@@ -60,7 +60,7 @@ jobs:
       env:
           OPAMYES: true
       run: |
-        opam install coq-lsp.0.1.9+8.19
+        opam install coq-lsp.0.2.2+8.19
         eval $(opam env)
 
     - name: Install Node.js

.prettierrc.json

@@ -7,5 +7,6 @@
     "printWidth": 80,
     "importOrder": ["^[./]*llm/(.*)$", "^[./]*coqLsp/(.*)$", "^[./]*core/(.*)$", "^../", "^./"],
     "importOrderSeparation": true,
-    "importOrderSortSpecifiers": true
+    "importOrderSortSpecifiers": true,
+    "importOrderParserPlugins": ["typescript", "@trivago/prettier-plugin-sort-imports", "decorators-legacy"]
 }

.vscode/settings.json

@@ -1,23 +1,26 @@
 // Place your settings in this file to overwrite default and user settings.
 {
     "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,
-        "**/*.vo": true,
-        "**/*.vok": true,
-        "**/*.vos": true,
-        "**/*.aux": true,
-        "**/*.glob": true,
-        "out": false,
-        "**/*_cp_aux.v": true
+        "out": false
     },
     "search.exclude": {
         "out": true // set this to false to include "out" folder in search results
     },
     // Turn off tsc task auto detection since we have the necessary tasks as npm scripts
-    "typescript.tsc.autoDetect": "off"
+    "typescript.tsc.autoDetect": "off",
+    "coq-lsp.check_only_on_request": false,
+    "eslint.options": {
+        "experimentalDecorators": true
+    }
 }

CHANGELOG.md

@@ -1,5 +1,21 @@
 # Changelog
 
+## 2.4.0
+
+The version increment is minor, yet the changes are significant. The main focus of this release was to improve interaction with the `coq-lsp` server. We now completely got rid of temporary files in the `extension` part of `CoqPilot`. This was done thanks to [ejgallego](https://github.com/ejgallego) and his improvements in `coq-lsp`. Now checking of proofs is done via the `proof/goals` request via `command` parameter, which is much more reliable and faster. Now a single `lsp` server is created for the plugin until being explicitly closed, and it tracks changes in the file. If you are using `coq-lsp` plugin itself, it will help you to always keep track of whether file is checked or not. When `CoqPilot` is ran on a completely checked file, it will not bring any significant overhead apart from requests to the Completion Services. 
+
+### Public changes
+- Added a toggle button to enable/disable the extension
+- Using the toggle switch, user can now abort the proof generation process
+- Significant performance improvements in proof checking that are especially easy to see for large files
+
+### Internal changes
+- Get rid of temporary files in the `extension` part of `CoqPilot`
+- Refactor `CoqLspClient` 
+- Make computation of `initialGoal` for premises optional to avoid unnecessary requests to `coq-lsp`
+- Introduce `with-coq-lsp` wrappers to encapsulate correct `CoqLspClient` disposal
+- Introduce `CoqLspClient.withTextDocument(...)` wrapper to encapsulate opening and closing a document with `coq-lsp`
+
 ## 2.3.0
 
 **A major upgrade of the benchmarking system**: At the moment, only a little **new** functionality is provided; moreover, the ability to run benchmarks on Tactician/CoqHammer is temporarily unavailable. However, it will soon be restored and improved. Excessive work has been done to make the benchmarking system more flexible, secure, robust, self-contained, and easy to use. Experiments via our benchmarking framework have been made more accessible than ever. The configurability and reliability of the pipeline have been improved drastically. In a nutshell, the main features of the improved benchmarking system include:

README.md

@@ -1,21 +1,19 @@
-# CoqPilot
-
-![Version](https://img.shields.io/badge/version-v2.3.0-blue?style=flat-square)
+# CoqPilot ![Version](https://img.shields.io/badge/version-v2.4.0-blue?style=flat-square)
 
 *Authors:* Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev, [Programming Languages and Tools Lab](https://lp.jetbrains.com/research/plt_lab/) at JetBrains Research.
 
 `CoqPilot` is a [Visual Studio Code](https://code.visualstudio.com/) extension that is designed to help automate writing of Coq proofs. It uses Large Language Models to generate multiple potential proofs and then uses [coq-lsp](https://github.com/ejgallego/coq-lsp) to typecheck them. It substitutes the proof in the editor only if a valid proof is found. 
 
 # Table of Contents
 
-- 🚀 [CoqPilot Overview](#coqpilot)
+- 🚀 [CoqPilot Overview](#coqpilot-version)
 - 📋 [Requirements](#requirements)
+- 📚 [Related papers](#related-papers)
 - 🔍 [Brief Technical Overview](#brief-technical-overview)
 - 💡 [Example Usage](#example-usage)
 - 🛠 [Installation](#installation)
   - ▶️ [Coq-LSP Installation](#coq-lsp-installation)
   - 🤖 [Building Locally](#building-locally)
-- ⚠️ [Important Information](#important)
 - ⚙️ [Extension Settings](#extension-settings)
 - 📐 [Guide to Model Configuration](#guide-to-model-configuration)
   - 🎛 [How VSCode settings work](#how-vscode-settings-work)
@@ -30,7 +28,17 @@
 
 ## Requirements
 
-* `coq-lsp` version `0.1.9+8.19` is currently required to run the extension.
+* `coq-lsp` version `0.2.2+8.19` is currently required to run the extension.
+
+## Related papers
+
+- **[ASE Demo'24]** *CoqPilot, a plugin for LLM-based generation of proofs*
+  <br />
+  [[Paper](https://dl.acm.org/doi/10.1145/3691620.3695357) | [arXiv](https://arxiv.org/abs/2410.19605) | [Video (5min)](https://www.youtube.com/watch?v=oB1Lx-So9Lo) | [Video (10min)](https://www.youtube.com/watch?v=P-LHXf7vntM)]
+- **[AITP'24 & CoqWS'24]** *CoqPilot, a plugin for LLM-based generation of proofs*
+  <br />
+  [[Extended Abstract](https://coq-workshop.gitlab.io/2024/files/EA2.pdf) | [CoqWS Slides](https://coq-workshop.gitlab.io/2024/files/SL2.pdf)]
+
 
 ## Brief technical overview
 
@@ -68,14 +76,26 @@ As soon as at least one valid proof is found, it is substituted in the editor an
 
 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.9+8.19
+opam pin add coq-lsp 0.2.2+8.19
 opam install coq-lsp
 ```
 For more information on how to install `coq-lsp` please refer to [coq-lsp](https://github.com/ejgallego/coq-lsp). 
 
 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.
+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 `opam`.
+
+**IMPORTANT**: If you are using `nix` in your project, make sure to **UPDATE** the path of the `coq-lsp` server in the settings. The default path is set to `coq-lsp`, which is the default path for `opam`. If you are using `nix`, you should run the following command from inside of the `nix-shell`: 
+```bash
+which coq-lsp
+```
+And then copy the path to the `coq-lsp` server and paste it into the `coqpilot.coqLspServerPath` setting. 
+
+In the benchmark the same rule applies, but the path to the `coq-lsp` server should be set as an environment variable `COQ_LSP_PATH`: 
+```bash
+export COQ_LSP_PATH=$(which coq-lsp)
+```
+
 
 ### Building locally
 
@@ -110,19 +130,6 @@ To run specific tests, you can use `npm run test -- -g="grep pattern"`.
 
 The extension's architecture overview is stored in the [ARCHITECTURE.md](https://github.com/JetBrains-Research/coqpilot/blob/refactor/ARCHITECTURE.md) file. It will be extended and updated as the project evolves. -->
 
-## Important 
-
-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/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.
-
 ## Extension Settings
 
 This extension contributes the following settings:
@@ -253,7 +260,7 @@ The process of running the benchmark is not perfectly automated and we are worki
     npm run benchmark
     ```    
 
-If you aim to run the benchmark with the use of `Tactician`, you should install the `imm` project and `Tactician` with `opam`. For `opam` installation instrustion, you can refer to the [Tactician website](https://coq-tactician.github.io/manual/installation/) and [imm repository](https://github.com/weakmemory/imm/tree/master?tab=readme-ov-file#installation-via-opam-supported-up-to-the-15-version-of-imm) (this part of the README file is a little outdated, but the installation process for `coq-8.19.0` is still the same).
+If you aim to run the benchmark with the use of `Tactician`, you should install the `imm` project and `Tactician` with `opam`. For `opam` installation instruction, you can refer to the [Tactician website](https://coq-tactician.github.io/manual/installation/) and [imm repository](https://github.com/weakmemory/imm/tree/master?tab=readme-ov-file#installation-via-opam-supported-up-to-the-15-version-of-imm) (this part of the README file is a little outdated, but the installation process for `coq-8.19.0` is still the same).
 
 ## Integrating other solutions
 
@@ -296,7 +303,6 @@ Then add the `hammer.`, `sauto.` or any other tactic from `CoqHammer` to the pre
 ## Future plans
 
 - Currently the user needs to manually enter the nix shell to get the correct environment for the benchmarks. We are working on automating this process.
-- Get rid of the overhead due to hacks with coq-lsp and the aux files.
 
 ## Release Notes
 

etc/docs/benchmark/BENCHMARKING_FRAMEWORK_GUIDE.md

@@ -40,6 +40,7 @@ This experiment must be run within the workspace environment, which the user act
 cd dataset/imm
 nix-build # builds the 'imm' project
 nix-shell # activates its environment
+export COQ_LSP_PATH=$(which coq-lsp) # sets up the proper coq-lsp server path
 cd ../..
 npm run single-workspace-benchmark
 ```

package.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/JetBrains-Research/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "2.3.0",
+  "version": "2.4.0",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -392,15 +392,18 @@
     "pretest": "npm run compile && npm run lint",
     "test": "npm run test-only",
     "clean": "rm -rf out",
+    "rebuild": "npm run clean && npm run compile && npm run format",
     "rebuild-test-resources": "cd ./src/test/resources/coqProj && make clean && make",
     "preclean-test": "npm run clean && npm run rebuild-test-resources && npm run compile && npm run lint",
     "clean-test": "npm run test-only",
     "prebenchmark": "npm run preclean-test",
-    "premulti-workspace-benchmark": "npm run prebenchmark",
+    "premulti-workspaces-benchmark": "npm run prebenchmark",
     "multi-workspaces-benchmark": "node ./out/benchmark/multiWorkspacesSetup.js",
     "presingle-workspace-benchmark": "npm run prebenchmark",
     "single-workspace-benchmark": "npm run test-executables-unsafe -- -g=\"[SourceExecutable] Single Workspace Benchmark\"",
     "benchmark": "npm run single-workspace-benchmark",
+    "prebenchmark-test": "rm -rf benchmarksOutput",
+    "benchmark-test": "npm run benchmark",
     "preteamcity-benchmark-setup": "npm run prebenchmark",
     "teamcity-benchmark-setup": "node ./out/benchmark/teamCitySetup.js",
     "teamcity-benchmark-agent": "npm run test-executables-unsafe -- -g=\"[SourceExecutable] Team City Benchmark Agent\"",
@@ -441,7 +444,7 @@
     "event-source-polyfill": "^1.0.31",
     "i": "^0.3.7",
     "mocha-param": "^2.0.1",
-    "node-ipc": "^11.1.0",
+    "node-ipc": "^12.0.0",
     "npm": "^10.4.0",
     "openai": "^4.6.0",
     "path": "^0.12.7",
@@ -450,6 +453,7 @@
     "tiktoken": "^1.0.17",
     "tmp": "^0.2.3",
     "toml": "^3.0.0",
+    "ts-results": "^3.3.0",
     "vscode-languageclient": "^9.0.1",
     "yargs": "^17.7.2"
   }