Merge pull request #25 from JetBrains-Research/v2.2.0-dev

release: v2.2.0+0.1.8+8.19

.eslintrc.json

@@ -5,23 +5,47 @@
         "ecmaVersion": 6,
         "sourceType": "module"
     },
-    "extends": [ "prettier" ],
-    "plugins": [
-        "@typescript-eslint",
-        "prettier"
-    ],
+    "extends": ["prettier"],
+    "plugins": ["@typescript-eslint", "prettier"],
     "rules": {
-        "@typescript-eslint/naming-convention": "warn",
+        /* Most of the rules here are just the default ones,
+         * the main changes are:
+         * - required UPPER_CASE for enum members;
+         * - allowed UPPER_CASE in general.
+         */
+        "@typescript-eslint/naming-convention": [
+            "warn",
+            { "selector": "default", "format": ["camelCase"] },
+            {
+                "selector": "variable",
+                "format": ["camelCase", "UPPER_CASE"],
+                "leadingUnderscore": "allow"
+            },
+            {
+                "selector": "property",
+                "format": ["camelCase", "UPPER_CASE"],
+                "leadingUnderscore": "allow"
+            },
+            {
+                "selector": "parameter",
+                "format": ["camelCase"],
+                "leadingUnderscore": "allow"
+            },
+            {
+                "selector": "typeLike",
+                "format": ["PascalCase"]
+            },
+            {
+                "selector": "enumMember",
+                "format": ["UPPER_CASE"]
+            }
+        ],
         "@typescript-eslint/semi": "warn",
         "curly": "warn",
         "eqeqeq": "warn",
         "no-throw-literal": "warn",
         "semi": "off",
         "prettier/prettier": "warn"
     },
-    "ignorePatterns": [
-        "out",
-        "dist",
-        "**/*.d.ts"
-    ]
+    "ignorePatterns": ["out", "dist", "**/*.d.ts"]
 }

.github/workflows/coqpilot.yml

@@ -2,46 +2,63 @@ name: Build and Test
 
 on: 
   push:
-    branches: [ main ]
+    branches:
+      - main
   pull_request:
-    branches: [ main ]
+    branches:
+      - main
+      - 'v[0-9]+.[0-9]+.[0-9]+-dev'
+  workflow_dispatch:
+
 env: 
-  coqlsppath: "coq-lsp"
+  coqlsp-path: "coq-lsp"
+  coqlsp-version: "0.1.8+8.19"
 
 jobs:
   build: 
     strategy:
       matrix:
-        os: [ubuntu-latest]
+        os: 
+          - ubuntu-latest
         ocaml-compiler:
           - "4.14"
+
     runs-on: ${{ matrix.os }}
+
     outputs:
       vsixPath: ${{ steps.packageExtension.outputs.vsixPath }}
+
     steps:
     - name: Checkout tree
       uses: actions/checkout@v4
+
+    # For some reason, the most significant thing for caching opam dependencies properly
+    # is `dune-cache: true` instead of this caching action.
+    - name: Restore cached opam dependencies
+      id: cache-opam
+      uses: actions/cache@v3
+      with:
+        path: ~/.opam/
+        key: opam-${{ matrix.os }}-${{ matrix.ocaml-compiler }}-${{ env.coqlsp-version }}
+        restore-keys: opam-${{ matrix.os }}-${{ matrix.ocaml-compiler }}-
 
     - name: Set-up OCaml ${{ matrix.ocaml-compiler }}
       uses: ocaml/setup-ocaml@v2
       with:
         ocaml-compiler: ${{ matrix.ocaml-compiler }}
-
+        dune-cache: true
+
     - name: Install opam dependencies
       env:
           OPAMYES: true
       run: |
         opam install coq-lsp.0.1.8+8.19
         eval $(opam env)
-    
-    - name: Opam eval 
-      run: eval $(opam env)
 
     - name: Install Node.js
-      uses: actions/setup-node@v3
+      uses: actions/setup-node@v4 
       with:
-        node-version: 16.x
-
+        node-version-file: ".nvmrc"
     - run: npm ci
 
     - name: Check coq-lsp version
@@ -64,15 +81,23 @@ jobs:
 
     - name: Test on Linux
       env:
-          COQ_LSP_PATH: ${{ env.coqlsppath }}
-      run: xvfb-run -a npm run test-ci
+          COQ_LSP_PATH: ${{ env.coqlsp-path }}
+      run: |
+        eval $(opam env)
+        xvfb-run -a npm run clean-test
       if: runner.os == 'Linux'
 
     - name: Test not on Linux
       env:
-          COQ_LSP_PATH: ${{ env.coqlsppath }}
-      run: npm run test-ci
+          COQ_LSP_PATH: ${{ env.coqlsp-path }}
+      run: |
+        eval $(opam env)
+        npm run clean-test
       if: runner.os != 'Linux'
+
+    - name: Setup tmate session
+      if: ${{ failure() }}
+      uses: mxschmitt/action-tmate@v3
 
     - name: Package Extension
       id: packageExtension
@@ -93,9 +118,9 @@ jobs:
     if: github.ref == 'refs/heads/main'
     steps:
       - uses: actions/checkout@v4
-      - uses: actions/setup-node@v3
+      - uses: actions/setup-node@v4
         with:
-          node-version: 16.x
+          node-version-file: ".nvmrc"
       - name: Install Dependencies
         run: npm ci
       - name: Download Build Artifact

.nvmrc

@@ -0,0 +1 @@
+20.13.1

CHANGELOG.md

@@ -1,95 +1,148 @@
-# Change Log
+# Changelog
+
+## 2.2.0
+
+### Public changes
+
+- Support time estimation for LLM services to become available after failure via logging proof-generation requests. This information is shown to the user. 
+- Set up interaction between `LLMService`-s and UI to report errors that happened during proof-generation.
+- Improve LLM services' parameters: their naming, transparency, and description.
+    - Introduce `modelId` to distinguish a model identifier from the name of an OpenAI / Grazie model.
+    - Rename `newMessageMaxTokens` to `maxTokensToGenerate` for greater clarity.
+    - Update the settings description, and make it more user-friendly.
+- Significantly improve settings validation.
+    - Use parameters resolver framework to resolve parameters (with overrides and defaults) and validate them.
+    - Support messages about parameter resolution: both failures and unexpected overrides.
+    - Clarify existing error messages.
+    - Add some general checks: input models have unique `modelId`-s, there are models to generate proofs with.
+- Improve interaction with OpenAI.
+    - Notify the user of configuration errors (invalid model name, incorrect API key, maximum context length exceeded) and connection errors.
+    - Support resolution of `tokensLimit` and `maxTokensToGenerate` with recommended defaults for known models.
+- Fix minor bugs and make minor improvements detected by thorough testing.
+
+### Internal changes
+
+- Rework and document LLMService architecture: `LLMServiceInternal`, better facades, powerful typing.
+- Introduce hierarchy for LLMService errors. Support proper logging and error handling inside `LLMService`-s.
+- Rework settings validation.
+    - Refactor `SettingsValidationError`, move all input parameters validation to one place and make it coherent.
+    - Design and implement a powerful and well-documented parameters resolver framework.
+
+### Testing infrastructure changes
+
+- Test the LLM Services module thoroughly. 
+- Improve test infrastructure in general by introducing and structuring utils.
+- Fix the issue with building test resources on CI. 
+- Set up CI debugging, and enable launching CI manually. 
+  Double the speed of CI by setting caches.
+
+## 2.1.0
 
-### 2.1.0
 Major: 
 - Create a (still in development and improvement) benchmarking system. A guide on how to use it is in the README.
-- Conduct an experiment on the performance of different LLMs, using the developed infrastructure. Benchmarking report is located in the [docs folder](etc/docs/benchmarking_report01.md).
-- Correctly handle and display settings which occur when the user settings are not correctly set.
+- Conduct an experiment on the performance of different LLMs, using the developed infrastructure. The benchmarking report is located in the [docs folder](etc/docs/benchmarking_report01.md).
 
 Minor: 
-- Set order of contributed settings.
+- Set the order of contributed settings.
 - Add a comprehensive user settings guide to the README. 
-- Fix issue with Grazie service not being able to correctly accept coq ligatures.
-- Fix issue that occured when generated proof contained `Proof using {...}.` construct. 
+- Fix the issue with Grazie service not being able to correctly accept coq ligatures.
+- Fix the issue that occurred when the generated proof contained the `Proof using {...}.` construct. 
 
-### 2.0.0
-- Added multiple strategies for ranking theorems from the working file. As LLM context window is limited, we sometimes should somehow choose a subset of theorems we want to provide as references to the LLM. Thus, we have made a few strategies for ranking theorems. Now there are only 2 of them, but there are more to come. Now we have a strategy that randomly picks theorems, and also the one that ranks them depending on the distance from the hole.
+## 2.0.0
+
+- Added multiple strategies for ranking theorems from the working file. As the LLM context window is limited, we sometimes should somehow choose a subset of theorems we want to provide as references to the LLM. Thus, we have made a few strategies for ranking theorems. Now there are only 2 of them, but there are more to come. Now we have a strategy that randomly picks theorems, and also the one that ranks them depending on the distance from the hole.
 - Now different holes are solved in parallel. This is a huge improvement in terms of performance.
-- Implemented multi-round fixing procedure for the proofs from the LLM. It can now be configured in the settings. One can set the amount of attempts for the consequtive proof fixing with compiler feedback. 
+- Implemented multi-round fixing procedure for the proofs from the LLM. It can now be configured in the settings. One can set the number of attempts for the consecutive proof fixing with compiler feedback. 
 - Added an opportunity to use LM Studio as a language model provider.
-- More accurate token count. Tiktoken is now used for open-ai models.
-- Different logging levels now supported. 
+- More accurate token count. Tiktoken is now used for OpenAI models.
+- Different logging levels are now supported. 
 - The LLM iterator now supports adding a sequence of models for each service. This brings freedom to the user to experiment with different model parameters.
 - Now temperature, prompt, and other parameters are configurable in the settings.
 
-### 1.9.0 
-- Huge refactoring done. Project re organized.
+## 1.9.0
+
+- Huge refactoring is done. Project reorganized.
+
+## 1.5.3
 
-### 1.5.3
 - Fix Grazie service request headers and endpoint. 
 
-### 1.5.2
+## 1.5.2
+
 - Fix issue with double document symbol provider registration (@Alizter, [#9](https://github.com/JetBrains-Research/coqpilot/issues/9))
 
-### 1.5.1
-- Add support of the Grazie platform as an llm provider.  
+## 1.5.1
+
+- Add support for the Grazie platform as an LLM provider.  
 
-### 1.5.0
-- Now when the hole can be solved by a single tactic solver, using predefined tactics, gpt will not be called, LLMs are now fetched consequently. 
+## 1.5.0
+
+- Now when the hole can be solved by a single tactic solver, using predefined tactics, OpenAI and Grazie will not be called, LLMs are now fetched consequently. 
 - Parallel hole completion is unfortunately postponed due to the implementation complexity. Yet, hopefully, will still be implemented in milestone `2.0.0`.
 
-### 1.4.6
-- Fix issue with plugin breaking after parsing a file containing theorem without `Proof.` keyword.
+## 1.4.6
+
+- Fix the issue with the plugin breaking after parsing a file containing theorem without the `Proof.` keyword.
+
+## 1.4.5
 
-### 1.4.5
 - Fix formatting issues when inserting the proof into the editor.
 
-### 1.4.4
-- Do not require a theorem to be `Admitted.` for coqpilot to prove holes in it.
-- Correctly parse theorems that are declared with `Definition` keyword.
+## 1.4.4
+
+- Do not require a theorem to be `Admitted.` for CoqPilot to prove holes in it.
+- Correctly parse theorems that are declared with the `Definition` keyword.
 
-### 1.4.3
-- Tiny patch with shuffling of the hole array.
+## 1.4.3
 
-### 1.4.2
-- Now no need to add dot in the end of the tactic, when configuring a single tactic solver.
+- Tiny patch with the shuffling of the hole array.
+
+## 1.4.2
+
+- Now no need to add a dot at 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).
+but most ones are. The ones that are not automatically reloaded: `useGpt`, `coqLspPath`, `parseFileOnInit`.
+- Added a command that solves admits in a selected region. Also added that command to the context menu (right-click in the editor).
 - Fix toggle extension. 
 
-### 1.4.1
+## 1.4.1
+
 - Add a possibility to configure a single tactic solver.
 
-### 1.4.0
-- Add command to solve all admitted holes in the file.
+## 1.4.0
+
+- Add a command to solve all admitted holes in the file.
 - Fixing bugs with coq-lsp behavior. 
 
-### 1.3.1
+## 1.3.1
+
 - Test coverage increased.
-- Refactoring client and ProofView.  
+- Refactoring client and ProofView.  
 - Set up CI. 
 
-### 1.3.0
+## 1.3.0
+
 - Fix bug while parsing regarding the updated Fleche doc structure in coq-lsp 0.1.7.
 - When GPT generated a response containing three consecutive backtick symbols it tended to 
 break the typecheking of the proof. Now solved. 
 - Speed up the file parsing process. 
 
-### 1.2.1
+## 1.2.1
+
 - Add clearing of aux file after parsing. 
 
-### 1.2.0
-- Fix error with llm silently failing. Now everything that comes from llm that is not handled inside plugin is presented to user as a message (i.e. incorrect apiKey exception). 
-- Fix toggle button.
-- Fix diagnostics being shown to non coq-lsp plugin coq users. 
-- Add output stream for the logs in vscode output panel.
+## 1.2.0
+
+- Fix error with llm silently failing. Now everything that comes from LLM that is not handled inside the plugin is presented to the user as a message (i.e. incorrect apiKey exception). 
+- Fix the toggle button.
+- Fix diagnostics being shown to non-`coq-lsp` plugin coq users. 
+- Add output stream for the logs in the vscode output panel.
 
-### 1.1.0
+## 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. 
-More communication with `coq-lsp` is added. Saperate package `coqlsp-client` no longer used.
+Now proof generation could be run in any position inside the theorem. There is no need to retake a file snapshot after each significant file change. 
+More communication with `coq-lsp` is added. The separate package `coqlsp-client` is no longer used.
 
-### 0.0.1
+## 0.0.1
 
-Initial release of coqpilot. 
+The initial release of CoqPilot.