Significant proof checking refactoring

.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,19 @@
 # Changelog
 
+## 2.3.1
+
+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`
+
 ## 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,6 +1,4 @@
-# CoqPilot
-
-![Version](https://img.shields.io/badge/version-v2.3.0-blue?style=flat-square)
+# CoqPilot ![Version](https://img.shields.io/badge/version-v2.3.1-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.
 
@@ -30,7 +28,7 @@
 
 ## 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.
 
 ## Brief technical overview
 
@@ -68,7 +66,7 @@ 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). 

package.json

@@ -8,7 +8,7 @@
     "url": "https://github.com/JetBrains-Research/coqpilot"
   },
   "publisher": "JetBrains-Research",
-  "version": "2.3.0",
+  "version": "2.3.1",
   "engines": {
     "vscode": "^1.82.0"
   },
@@ -392,6 +392,7 @@
     "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",
@@ -441,7 +442,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 +451,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"
   }

src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts

@@ -7,6 +7,7 @@ import {
 } from "../../../../../../core/coqProofChecker";
 
 import { stringifyAnyValue } from "../../../../../../utils/printers";
+import { Uri } from "../../../../../../utils/uri";
 import { BenchmarkingLogger } from "../../../../logging/benchmarkingLogger";
 import { LogsIPCSender } from "../../../../utils/subprocessUtils/ipc/onParentProcessCallExecutor/logsIpcSender";
 import { TimeMark } from "../../measureUtils";
@@ -37,12 +38,20 @@ export namespace CheckProofsImpl {
 
         try {
             const timeMark = new TimeMark();
+            const fileUri = Uri.fromPath(args.fileUri);
+
+            // TODO: [@Gleb Solovev] Pay Atteniton that it was previously done by the CoqProofChecker
+            await coqLspClient.openTextDocument(fileUri);
+
             const proofCheckResults = await coqProofChecker.checkProofs(
-                args.sourceFileDirPath,
-                args.sourceFileContentPrefix,
-                args.prefixEndPosition,
+                fileUri,
+                args.documentVersion,
+                args.checkAtPosition,
                 args.preparedProofs
             );
+
+            await coqLspClient.closeTextDocument(fileUri);
+
             const proofsValidationMillis = timeMark.measureElapsedMillis();
             return buildSuccessResult(
                 proofCheckResults,