Agda Web

tl;dr

The aim of the Agda Web project is to make the proof assistant Agda available in web environments, including GitHub and online textbooks.

To use Agda with a GitHub repository (or any repository host supported by VS Code for the Web), follow the instructions below.

To start VS Code for the Web, either
- visit VS Code for the Web;
- visit any repository on GitHub such as the PLFA fork (as shown in the video) and press .
To install the required extensions, open the Extensions tab and install the following:
1. agda-mode by Ting-Gian LUA
2. Agda Language Server WASM Loader by Andy Pan
3. Submodule Cloner by Andy Pan
To install the standard/cubical library, run the command ALS WASM Loader: Manage libraries by
- selecting View/Command Palette... , or
- pressing Ctrl + Shift + P on Windows/Linux (or Cmd + Shift + P on macOS).
This step may take a while to finish. Note that if you open the PLFA fork then you should install v2.1 of the standard library.
(Optional) To open a GitHub repository, run the command: Remote Repositories: Open Remote Repository.
(Optional) To trust the workspace,
1. open the Extensions tab
2. click the icon
3. click Trust
For security reasons, you may need to perform this step the first time you open a repository.
To type check, open any .agda file and either run the command Agda: Load or press the keyboard shortcut Ctrl + C Ctrl + L.

The WebAssembly version of Agda is powered by GHC's WebAssembly backend and a few patches for Agda (already merged into Agda's codebase).

We are still working on integrating this WebAssembly build with the following web-first IDEs/editors:

VS Code (desktop/web): Use the agda-mode-vscode extension developed by banacorn.
CodeMirror 6: Still a work in progress! An experimental PoC for the Agda Language Server is available.

We are working on implementing Agda's interaction protocol over LSP to support all LSP-aware editors.