agda-wasm-dist

Distributions of Agda executable compiled into WebAssembly. An online demo can be seen here.

Quickstart

1. Install a WASI-compliant runtime. I suggest wasmer. Note that we maintain our own fork to mitigate bugs we have found along the way.
2. Grab the WASM module either from an artifact or a Docker image.
3. Run it with the runtime of your choice.

You need to specify a handful of configurations for it to work correctly:

• Filesystem layout: The directory specified in Built-in library path must be accessible. All other directories are optional.

• Current working directory: This is set by environment variable PWD. Forwarding it from the shell is sufficient.

• The home directory: This is used to expand ~ in paths. This setting is mandatory, otherwise Agda will fallback to probing the effective UID and fail.

• The global config directory: The value can be obtained via flag --print-agda-app-dir, serving as the source of Agda's library management system. The default path is $HOME/.config/agda, and you can override with the enviroment variable AGDA_DIR.

• Built-in library path: The value can be obtained via flag --print-agda-data-dir, but you can override it with the environment variable Agda_datadir. It must contain a directory structure lib/prim/Agda/.... The content can be copied from Agda's source tree under src/data or from the Docker image.
  Tip: The minimal requirement to run Agda is these two files Agda/Primitive.agda and Agda/Primitive/Cubical.agda.

Quirks of interaction mode

If you are running interaction mode, you need a runtime that supports switching stdin to nonblocking or something equivalent (i.e., never blocks on stdin), and use a newer artifact with an RTS option -V1 since the default value for WASM suffers from thrashing. Any value greater than zero works.

Sample commands

🔖 Type-checking a module:

wasmer run --dir $HOME \
           --env PWD=$PWD \
           --env HOME=$HOME \
           --env Agda_datadir=$HOME/.local/share/agda \
           ./agda.wasm -- test.agda

🔖 Interaction mode (note the RTS option):

wasmer run ./agda.wasm -- --interaction +RTS -V1

Send the line to stdin for testing: IOTCM "x.agda" None Direct (Cmd_show_version).

Versions

The repo contains the following version combinations:

Agda version	GHC version	Where to find
2.6.4.3	9.8.1	As tag v2.6.4.3-ghc9.8.1-r0.
2.6.4.3-r1	9.8.1	In branch ghc-9.8.
	9.10.0	As tag v2.6.4.3-r1-ghc9.10.1-r3.
	9.10.1	The master branch.

Known issues

I have mis-tagged most commits. The 2.6.4.3-r1-ghc9.10.1-r[0123] versions are built with GHC 9.10.0, not 9.10.1.