Authors: Andrei Kozyrev and Anton Podkopaev, Programming Languages and Tools Lab at JetBrains Research.
Coqpilot is a Visual Studio Code 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 to typecheck them. It substitutes the proof in the editor only if a valid proof is found.
coqpilot is in early beta and seeks for feedbacks. Please feel free to open an issue regarding any problem you encounter or any feature you want to see in the future.
Brief technical overview
Coqpilot now supports fetching proofs from all open-ai gpt models, but is designed to be easily extensible to other models.
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 at a given cursor point inside theorem to try substitute the current goal.
coqpilot with some chosen selection to try substitute all admits in this selection.
coqpilot to try substitute all admits in the file.
coq-lsp version 0.1.7 is currently required to run the extension.
To make the extension running you will have to install
coq-lsp server. You can install it using opam:
opam install coq-lsp
For more information on how to install
coq-lsp please refer to coq-lsp.
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.
chmod +x 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.
This extension contributes the following settings:
open-ai api key. Is used to communicate with the open-ai api. You can get one here. It is required to run the extension.
coqpilot.proofAttemsPerOneTheorem: How many proof attempts should be generated for one theorem.
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.
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
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.
parseFileOnInit are NOT auto reloaded on setting change, they need plugin restart.
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.
It is planned to implement a proof repair feature for the proofs which will establish a dialogue between
coq-lsp and the LLM. When LLM generates an incorrect proof, the error would be sent to LLM as a next message and the process would be repeated until a valid proof is found or the limit of attempts is reached. Also it is planned to fetch proofs from different LLMs not at once in the beggining, but asynchronously and one by one, if it fails to find a proof in the first LLM, it will try the next one.
More detailed release notes could be found in the CHANGELOG.md file.
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.
Initial release of coqpilot.