Avea is a Visual Studio Code extension meant to provide the same development experience as Agda's Emacs mode. What stands out about Avea compared to other vscode extensions is that Avea is written in Agda itself.
The current version of the extension only supports Agda 2.9.0. You need to have Agda installed on your path, or set a custom path to the Agda binary in the vscode settings for the extension.
The extension itself can be installed via the official Visual Studio Code marketplace, the Open VSX Registry (the vscodium marketplace) and via a manual installation of the VSIX file. VSIX files are built on every commit on the master branch, and can be found under the artifacts section of a workflow run on the Github Actions page.
Warning
This extension has some conflicts with other extensions, most notably the Vim extension. Please disable the Vim extension to make sure this extension works without issues.
Some commands can be prefixed by a number of ctrl+u to specify the level of normalisation of the output. One exception is the compute command (ctrl+c ctrl+n), where each ctrl+u switches between DefaultCompute, IgnoreAbstract, UseShowInstance and HeadCompute.
- Without ctrl+u every command will return expressions as-is;
- With one ctrl+u, expressions are evaluated to weak head normal form;
- With ctrl+u ctrl+u, expressions are evaluated to their full normal form.
All of these commands operate on a goal, however some commands also work outside of a goal and display an input prompt to ask for a term or variable name instead.
| Command | Keybind | Has ctrl+u prefixes? | Works outside goal? |
|---|---|---|---|
| Goal context | ctrl+c ctrl+e | ✅ | ❌ |
| Goal type | ctrl+c ctrl+t | ✅ | ❌ |
| Goal type and context | ctrl+c ctrl+, | ✅ | ❌ |
| Goal type, context and inferred type | ctrl+c ctrl+. | ✅ | ❌ |
| Goal type, context and checked term | ctrl+c ctrl+; | ✅ | ❌ |
| Refine | ctrl+c ctrl+r | ✅ | ❌ |
| Give | ctrl+c ctrl+spc | ✅ | ❌ |
| Auto solve | ctrl+c ctrl+a | ✅ | ❌ |
| Make case | ctrl+c ctrl+c | ❌ | ❌ |
| Infer | ctrl+c ctrl+d | ✅ | ✅ |
| Compute | ctrl+c ctrl+n | ✅ | ✅ |
| Module contents | ctrl+c ctrl+o | ✅ | ✅ |
| Why in scope | ctrl+c ctrl+w | ❌ | ✅ |
| Search about | ctrl+c ctrl+z | ✅ | ✅ |
| Command | Keybind | Has ctrl+u modifiers? |
|---|---|---|
| Load file | ctrl+c ctrl+l | ❌ |
| Show all goals | ctrl+c ctrl+? | ✅ |
| Show constraints | ctrl+c ctrl+= | ✅ |
| Next goal | ctrl+c ctrl+f | ❌ |
| Previous goal | ctrl+c ctrl+b | ❌ |
| Toggle hidden arguments | ctrl+c ctrl+x ctrl+h | ❌ |
| Toggle irrelevant arguments | ctrl+c ctrl+x ctrl+i | ❌ |
| Restart Agda process | ctrl+c ctrl+x ctrl+r | ❌ |
| Compile file | ctrl+c ctrl+x ctrl+c | ❌ |
| Switch version | ctrl+c ctrl+x ctrl+s | ❌ |
The unicode input works similarly to the one in the Emacs mode. Type \ to enable input mode and then type the unicode characters code to input it into the buffer. There is a status bar at the bottom of the window which shows what characters can be inputted next, and which alternatives can be selected using the arrow keys.
Before running this extension make sure you have installed the following dependencies:
- Agda
- Visual Studio Code
- Node.js, which could be installed via nvm
To run the extension locally, open the cloned folder in vscode and execute the "Run Extension" debug profile. This will open a new vscode window with the extension loaded into it.