Agda Web

Agda Web

dl;dr

The aim of Agda Web project is to make the proof assistant Agda avaiable in a web environment, including GitHub or inside an online textbook, on any device including tablets.

Demo: Type-Checking PLFA in VS Code for the Web

Usage

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

  1. To start VS Code for the Web, either
  2. Open the Extensions tab and install:
    1. agda-mode by Ting-Gian LUA
    2. Agda Language Server WASM Loader by Andy Pan
    3. Submodule Cloner by Andy Pan
  3. To install the standard/cubical library, run the commands ALS WASM Loader: Manager 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.
  4. (Optional) To open a GitHub repository, run the command: Remote Repositories: Open Remmote Repository ....
  5. (Optional) To trust the workspace,
    1. open the Extensions tab
    2. click the icon
    3. click Trust
    For security reasons, this step may be required for the first time when you open a repository.
  6. To type check .agda file, open any the file and run the command Agda: Load (or press ctrl + c ctrl+l).

Implementations

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 IDE/editors:

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

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

Other useful links