Avea: Another Visual studio code Extension for Agda

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.

Installation

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.

Supported commands

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.

1. Without ctrl+u every command will return expressions as-is;
2. With one ctrl+u, expressions are evaluated to weak head normal form;
3. With ctrl+u ctrl+u, expressions are evaluated to their full normal form.

Goal commands

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.

Non-goal commands

Unicode input

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.

Development

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.