release: v1.9.0

v1.9.0

.eslintrc.json

@@ -5,16 +5,19 @@
         "ecmaVersion": 6,
         "sourceType": "module"
     },
+    "extends": [ "prettier" ],
     "plugins": [
-        "@typescript-eslint"
+        "@typescript-eslint",
+        "prettier"
     ],
     "rules": {
         "@typescript-eslint/naming-convention": "warn",
         "@typescript-eslint/semi": "warn",
         "curly": "warn",
         "eqeqeq": "warn",
         "no-throw-literal": "warn",
-        "semi": "off"
+        "semi": "off",
+        "prettier/prettier": "warn"
     },
     "ignorePatterns": [
         "out",

.github/workflows/coqpilot.yml

@@ -29,7 +29,7 @@ jobs:
       env:
           OPAMYES: true
       run: |
-        opam install coq-lsp.0.1.7+8.18
+        opam install coq-lsp.0.1.8+8.19
         eval $(opam env)
     
     - name: Opam eval 

.prettierrc.json

@@ -0,0 +1,7 @@
+{
+    "trailingComma": "es5",
+    "tabWidth": 4,
+    "semi": true,
+    "singleQuote": false,
+    "printWidth": 80
+  }

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Change Log
 
+### 1.9.0 
+- Huge refactoring done. Project re organized.
+
 ### 1.5.3
 - Fix Grazie service request headers and endpoint. 
 

README.md

@@ -1,6 +1,6 @@
 # coqpilot
 
-*Authors:* Andrei Kozyrev and Anton Podkopaev, [Programming Languages and Tools Lab](https://lp.jetbrains.com/research/plt_lab/) at JetBrains Research.
+*Authors:* Andrei Kozyrev, Gleb Solovev 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. 
 
@@ -14,13 +14,9 @@ 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. 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. 
+It performs 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 open-ai models, coqpilot also tries substituting single-line proofs from the predefined tactics list.
 
 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"/>
@@ -29,7 +25,7 @@ User can:
 
 ## Requirements
 
-* `coq-lsp` version 0.1.7 is currently required to run the extension.
+* `coq-lsp` version 0.1.8 is currently required to run the extension.
 
 ## Coq-lsp installation
 
@@ -56,27 +52,38 @@ Comment: Such files are not visible in the vscode explorer, because plugin adds
 
 This extension contributes the following settings:
 
-* `coqpilot.openaiApiKey`: An `open-ai` api key. Is used to communicate with the open-ai api. You can get one [here](https://platform.openai.com/account/api-keys). It is required to run the extension.
-* `coqpilot.proofAttemsPerOneTheorem`: How many proof attempts should be generated for one theorem.
-* `coqpilot.gptModel`: Which `open-ai` model should be used to generate proofs.
-* `coqpilot.maxNumberOfTokens`: What is your token per minute limit for `open-ai` api. It is used to calculate how many proofs could be used as a message history. For more information please refer to [open-ai](https://platform.openai.com/account/rate-limits). 
-* `coqpilot.logAttempts`: Whether to log proof attempts. 
-* `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. 
+* `coqpilot.openAiModelsParameters`, `coqpilot.predefinedProofsModelsParameters` and `coqpilot.grazieModelsParameters`. 
+
+Each of these settings are modified in `settings.json` and contain an array of models from this service. Each model will be used for generation independantly. Multiple models for a single service could be defined. For example, you can define parameters for two open-ai gpt models. One would be using `gpt-3.5` and the other one `gpt-4`. CoqPilot will first try to generate proofs using the first model, and if it fails, it will try the second one. This way coqpilot iterates over all services (currently 3 of them) and for each service it iterates over all models.
+
+Here are parameters each of the service contributes:
+
+### Open-ai Service Parameters
+
+* `coqpilot.openAiModelsParameters.prompt`: System prompt for the `open-ai` model.
+* `coqpilot.openAiModelsParameters.apiKey`: An `open-ai` api key. Is used to communicate with the open-ai api. You can get one [here](https://platform.openai.com/account/api-keys). It is required to run the extension.
+* `coqpilot.openAiModelsParameters.choices`: How many proof attempts should be generated for one theorem.
+* `coqpilot.openAiModelsParameters.model`: Which `open-ai` model should be used to generate proofs.
+* `coqpilot.openAiModelsParameters.maxTokens`: What is your token per minute limit for `open-ai` api. It is used to calculate how many proofs could be used as a message history. For more information please refer to [open-ai](https://platform.openai.com/account/rate-limits). 
+* `coqpilot.openAiModelsParameters.temperature`: How much randomness should be added to the generated proofs. The higher the temperature, the more random the generated proofs will be.
+
+### Predefined Proofs Service Parameters
+
+* `coqpilot.predefinedProofsModelsParameters.tactics`: An array of tactics that will be used to generate proofs. For example `["auto."]`. This service is tried at the very beginning of the proof generation process.
+
+### Grazie Service Parameters
+
+* `coqpilot.grazieModelsParameters.prompt`: System prompt for the models. 
+* `coqpilot.grazieModelsParameters.apiKey`: An `grazie` api key. Is used to communicate with the grazie api. 
+* `coqpilot.grazieModelsParameters.choices`: How many proof attempts should be generated for one theorem.
+* `coqpilot.grazieModelsParameters.model`: Which model should 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.
+* `coqpilot.perform_completion_under_cursor`: Try to generate proof for the goal under the cursor.
+* `coqpilot.perform_completion_for_all_admits`: Try to prove all holes (admitted goals) in the current file.
+* `coqpilot.perform_completion_in_selection`: Try to prove holes (admitted goals) in selection.
 
 ## Planned Features
 
@@ -86,13 +93,4 @@ It is planned to implement a proof repair feature for the proofs which will esta
 
 ## 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. 
-More communication with `coq-lsp` is added. Saperate package `coqlsp-client` no longer used.
-
-### 1.0.0
-
-Initial release of coqpilot. 
+Release notes could be found in the [CHANGELOG.md](https://github.com/JetBrains-Research/coqpilot/blob/refactor/CHANGELOG.md) file.