|
6 | 6 |
|
7 | 7 | # Table of Contents
|
8 | 8 |
|
9 |
| -- 🚀 [CoqPilot Overview](#coqpilot) |
| 9 | +- 🚀 [CoqPilot Overview](#coqpilot-version) |
10 | 10 | - 📋 [Requirements](#requirements)
|
| 11 | +- 📚 [Related papers](#related-papers) |
11 | 12 | - 🔍 [Brief Technical Overview](#brief-technical-overview)
|
12 | 13 | - 💡 [Example Usage](#example-usage)
|
13 | 14 | - 🛠 [Installation](#installation)
|
14 | 15 | - ▶️ [Coq-LSP Installation](#coq-lsp-installation)
|
15 | 16 | - 🤖 [Building Locally](#building-locally)
|
16 |
| -- ⚠️ [Important Information](#important) |
17 | 17 | - ⚙️ [Extension Settings](#extension-settings)
|
18 | 18 | - 📐 [Guide to Model Configuration](#guide-to-model-configuration)
|
19 | 19 | - 🎛 [How VSCode settings work](#how-vscode-settings-work)
|
|
30 | 30 |
|
31 | 31 | * `coq-lsp` version `0.2.2+8.19` is currently required to run the extension.
|
32 | 32 |
|
| 33 | +## Related papers |
| 34 | + |
| 35 | +- **[ASE Demo'24]** *CoqPilot, a plugin for LLM-based generation of proofs* |
| 36 | + <br /> |
| 37 | + [[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)] |
| 38 | +- **[AITP'24 & CoqWS'24]** *CoqPilot, a plugin for LLM-based generation of proofs* |
| 39 | + <br /> |
| 40 | + [[Extended Abstract](https://coq-workshop.gitlab.io/2024/files/EA2.pdf) | [CoqWS Slides](https://coq-workshop.gitlab.io/2024/files/SL2.pdf)] |
| 41 | + |
| 42 | + |
33 | 43 | ## Brief technical overview
|
34 | 44 |
|
35 | 45 | `CoqPilot` fetches proofs from multiple completion services. Now we support:
|
@@ -108,19 +118,6 @@ To run specific tests, you can use `npm run test -- -g="grep pattern"`.
|
108 | 118 |
|
109 | 119 | 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. -->
|
110 | 120 |
|
111 |
| -## Important |
112 |
| - |
113 |
| -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. |
114 |
| - |
115 |
| -Moreover, this repository contains a script for your convenience that adds the format of such files to the global gitignore file on your system. |
116 |
| -- Copy the [`set_gitignore.sh`](https://github.com/JetBrains-Research/coqpilot/blob/main/set_gitignore.sh) file to your computer. Then: |
117 |
| -```bash |
118 |
| -chmod +x set_gitignore.sh |
119 |
| -./set_gitignore.sh |
120 |
| -``` |
121 |
| -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. |
122 |
| -Comment: Such files are not visible in the VSCode explorer, because plugin adds them to the `files.exclude` setting on startup. |
123 |
| - |
124 | 121 | ## Extension Settings
|
125 | 122 |
|
126 | 123 | This extension contributes the following settings:
|
@@ -294,7 +291,6 @@ Then add the `hammer.`, `sauto.` or any other tactic from `CoqHammer` to the pre
|
294 | 291 | ## Future plans
|
295 | 292 |
|
296 | 293 | - 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.
|
297 |
| -- Get rid of the overhead due to hacks with coq-lsp and the aux files. |
298 | 294 |
|
299 | 295 | ## Release Notes
|
300 | 296 |
|
|
0 commit comments