Agda in WebAssembly & Experiments on Language Servers

Update

The author has revisited this topic at Functional Thursday in June 2024. See the end of this document for updates. Extra content will be gathered into a separate note.

2023/11/20~2024/1/31

GHC version: 9.8.1
Clang version: 18.0.0
Agda version: 2.6.5 (nightly)

The icon ✨ is used to mark sections that require patching code.

Building GHC WASM backend on Apple Silicone

ghc-wasm-meta contains a one-size-fit-all solution, but the script downloads lots of built artifacts from GitHub (which in turn are sourced from the official GitLab) that cannot run on macOS at all: https://github.com/amesgen/ghc-wasm-bindists/.

Besides the build script can be made compatible with macOS, it can also be greatly simplified, at least unused/incompatible WASM runtimes are ought to be skipped.

To compile a functional ghc, here are mandatory steps from setup.sh located at the root of ghc-wasm-meta:

Clone wasi-sdk to $PREFIX/wasi-sdk. Be sure to use the wasi-sdk_darwin artifact.
- Basically it’s a bundle of clang 18.
Clone libffi-wasm and then copy file to $PREFIX/wasi-sdk/share/wasi-sysroot.
Set up environment variables for compiling, like CC, AR, …, from wasi-sdk.
- Problem: If using system compiler toolchain, the configuring step will fail to find ffi.h.
  Wiki of GHC has a solution to this but I have not tried…
- To print the compiler’s default configurations, use the neat trick clang - -E -v < /dev/null for include path and others. Also clang -print-search-dirs for libraries.
Set up CONF_@@@_OPTS_STAGE@ for compiling ghc. All envs are written to $PREFIX/env so that you can source it in a fresh terminal.

On macOS, there is no prebuilt wasm32-wasi-ghc artifact yet. So we need to build it on our own:

Prepare a working ghc in your host system. Because of the dependency constraint of base, you must use an older version than our target 9.8.1. We use ghc 9.4.7 for the whole demonstration.

git clone https://github.com/ghc/ghc --depth=1 --branch ghc-9.8.1-release
cd ghc
git submodule update --init
./boot
./configure --host=aarch64-apple-darwin \
            --target=wasm32-wasi \
            --with-intree-gmp --with-system-libffi
./hadrian/build --flavour=quick stage2:exe:ghc-bin
./hadrian/build --flavour=quick stage2:exe:ghc-pkg

Note that the executable from stageN is to be found in the N-1 directory, because they are built from linking libraries of the N-1-th stage. stage0 links with libraries from the host, and all other stages link with those from the target, so some compilation problems might only show up in certain stages.

Links might be useful:

Time spent on my MBA M1 for reference:

./hadrian/build --flavour=quick stage1:exe:ghc-bin -j2  924.36s user 85.20s system 169% cpu 9:54.81 total
./hadrian/build --flavour=quick stage2:exe:ghc-bin -j2  1657.50s user 181.94s system 189% cpu 16:11.33 total
./hadrian/build --flavour=quick stage3:exe:ghc-bin -j2  1241.69s user 130.87s system 188% cpu 12:08.61 total

You may find some legacy docs building GHC with automake. Now the only supported way is to use Hadrian, which is a standalone executable. It is helpful to execute

path/to/hadrian --help

to get a list of all available targets, but not all make sense to be built.

Compiling cabal

Prebuilt cabal from ghcup might not run on the GHC in the custom build. Compile our own cabal executable in the GHC tree according to the guide: https://gitlab.haskell.org/ghc/packages/Cabal/-/blob/master/CONTRIBUTING.md. I use version 3.10.2.0.

I am not sure if this is the correct way:

cabal build cabal-install
cabal install cabal-install

Compiling Agda

Use the cabal built in the previous section. As per Agda’s CI:

# "Configure the build plan"
cabal configure -O0 --enable-tests -f debug \
      --with-compiler=/path/to/ghc-repo/_build/stage1/bin/wasm32-wasi-ghc \
      --with-hc-pkg=/path/to/ghc-repo/_build/stage1/bin/wasm32-wasi-ghc-pkg
cabal build --dry-run

Keep retrying until all dependencies are satisfied:

ghc-compact → stage1:lib:ghc-compact
unlit → stage2:exe:unlit

Next step: Build the Setup.hs

$ cabal build
[1 of 2] Compiling Main             ( /.../dist-newstyle/build/wasm32-wasi/ghc-9.8.1/Agda-2.6.5/noopt/setup/setup.hs, /.../dist-newstyle/build/wasm32-wasi/ghc-9.8.1/Agda-2.6.5/noopt/setup/Main.o )
[2 of 2] Linking /.../dist-newstyle/build/wasm32-wasi/ghc-9.8.1/Agda-2.6.5/noopt/setup/setup.wasm
wasm-ld: error: unable to find library -lHSrts-1.0.2_thr
clang: error: linker command failed with exit code 1 (use -v to see invocation)
wasm32-wasi-ghc: `clang' failed in phase `Linker'. (Exit code: 1)
Error: cabal: Failed to build Agda-2.6.5. The failure occurred during the
configure step.

It turns out that the compiler argument to compile Setup.hs is appending -threaded. It is a non-portable assumption hardcoded in Cabal. See this issue.

https://gitlab.haskell.org/ghc/packages/Cabal/-/blob/eaa5245ef4949a9f02a82c7e225ab11cc64bba85/cabal-install/src/Distribution/Client/SetupWrapper.hs#L1012

Q: Can WASM or WASI leverage multithreading?
A: No. But there seems to be a proposal wasi-threads.

Q: Is it possible to compile/run setup.hs separately?
✨ A: IDK. Setup.hs does not do much stuff. Set build-type to Simple for now.

Template Haskell

Template Haskell (TH) is not supported by the WASM backend.

✨ Patch src/full/Agda/VersionCommit.hs to substitute the template parts with string literals. Effectively removing GitRev stuff. This is the only file that contains TH.

However, there is more in test suite, and compiling and AFAIK correctly running those programs is critical for QA. How to support TH in WASM is way beyond trivial:

Magic numbers in serialization

See hashWithSalt in src/full/Agda/TypeChecking/Serialise/Base.hs. The comment points out that it is a fallback algorithm of aHash under 64-bit systems.
Serialization algorithm assumes that the word size is at least 64 bits, while two integer literals are overflowing from 32 bits (u32/s32, resp.) when being compiled in WASM.
WASM is surely be able to handle 64-bit integers. Have something to do with platformMaxInt.

Missing tzset when linking

The Haskell time library, when built in WASM, does not contain the function tzset: https://github.com/haskell/time:

wasm-ld: error: /.../ghc/_build/stage1/lib/../lib/wasm32-wasi-ghc-9.8.1/time-1.12.2-inplace/libHStime-1.12.2-inplace.a(HsTime.o): undefined symbol: tzset

also

libraries/time/lib/cbits/HsTime.c:14:5: error:
     warning: call to undeclared function 'tzset'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
       14 |     tzset();
          |     ^

WASI has no intention to support timezone. In the wasi-libc's time.h we can remove a macro condition to expose this function. But wasi-sdk's library does not provide an implementation either, so in the end it could not link anyway.

✨ Hack: just comment out the tzset line in libraries/time.h. Should not do any harm. MR submission to GHC is pending…

Update 2024-06-14: Kudos to @huangjunwen's clever trick: 9999-Fix-missing-tzset.patch.

Mitigating Agda runtime errors

For the purpose of evaluation, the command line to run agda is as follows:

wasmtime run --env PWD --dir / \
         --env AGDA_DIR=$HOME/.config/agda
         $(cabal list-bin agda) --interaction

Errors during startup need to be first eliminated.

getAppUserDataDirectory failure

(agda2-info-action "*Error*" "Failed to read trusted executables.\ngetAppUserDataDirectory:getEffectiveUserID: unsupported operation (Operation is not supported)" nil)
(agda2-highlight-load-and-delete-action "/tmp/agda2-mode1-0")
(agda2-status-action "")

Getting the default path depends on a syscall to query the current user, which is not supported in WASI. If the AGDA_DIR environment variable is specified, Agda will not query the fallback value, circumventing this problem.

(agda2-info-action "*Error*" "/Users/xxx/ghc-wasm-project/agda/../../../../..:\ngetDirectoryContents:openDirStream: permission denied (Operation\nnot permitted)" nil)
(agda2-highlight-load-and-delete-action "/tmp/agda2-mode1-10")
(agda2-status-action "")

It is literally opening /..! In Linux and mac OS this is normalized to /. I suspect there is some bug about path handling in WASI libc.

The root cause is in expandEnvironmentVariables, which bails out when the home directory cannot be determined. According to the implementation of getHomeDirectory, the solution is always have $HOME set.

✨ Patch for Agda: to be updated.

Missing datadir

We need to prepare the content datadir to run Agda. While setting the environment variable Agda_datadir does the job, there is a new flag in 2.6.4.1 so we can do --print-agda-data-dir and then just put the built-in libraries there. The library can be found in the source tree under lib/. In Setup.hs all files are type-checked. You may want to mimic the setup script to achieve the same thing. Maybe the produced interface files can be bundled for distribution.

Path canonicalization issue

Agda has a procedure to find the project config file recursively, up to the root directory. In each, the path is canonized This is an unfortunate scenario, since that WASI does not expose realpath.

Thus, WASI runtimes will not canonicalize “foo/bar/..” to “foo”. The runtime exhabits various weird behaviors:

Recurses until “/..” is not recognized and rejected (wasmtime, wazero);
Stucks in a loop into resolving endless /../../../… (wasmer).
See https://github.com/rust-lang/rust/issues/82339;
Like 2., but recurses forever at home directory instead (WASI API in Node.js).
Maybe Node considers it a boundary?

Suggested mitigations:

Stop looking upward whenever there is an IO error.
(Not sure about my usage of catchIO thingy is correct)
Query the device number and inode number in POSIX API. Under the assumption that a (st_dev, st_ino) is unique across the whole UNIX file system, it can be used to determine whether we are at the root.
- This introduces an extra dependency unix-compat, and I don’t know the semantics of these numbers on Windows.
- wasmer does not report real inode numbers and incorrectly reports 1 for root (should be 2).
This involves some dirty patching around WASI APIs.
- The idea: proxy path_open and path_filestat_get; reject if the (normalized) paths are home directories.
- Just do not mess with it until a proper FS sandbox is implemented. Maybe never.

✨ Patch for Agda: to be determined.

To test, create an empty file x.agda and use the interaction mode with input:

IOTCM "x.agda" None Indirect (Cmd_load "x.agda" [])

Memory exceptions

It throws no matter what files are passed, even an empty file.

Error: failed to run main module `dist-newstyle/build/wasm32-wasi/ghc-9.8.1/Agda-2.6.5/x/agda/noopt/build/agda/agda.wasm`

Caused by:
    0: failed to invoke command default
    1: error while executing at wasm backtrace:
           0: 0x234e063 - agda.wasm!prmtvzm0zi9zi0zi0zmdb62ef4c_DataziPrimitiveziTypes_zdfPrimIntzuzdcreadByteArrayzh_entry
           1: 0x269986d - agda.wasm!StgRun
           2: 0x267a167 - agda.wasm!scheduleWaitThread
           3: 0x266d05f - agda.wasm!rts_evalLazyIO
           4: 0x266f531 - agda.wasm!hs_main
           5: 0x105944 - agda.wasm!main
           6: 0x26bd5e3 - agda.wasm!__main_void
           7: 0x1057eb - agda.wasm!_start
    2: memory fault at wasm address 0x2ae15f4 in linear memory of size 0x1900000
    3: wasm trap: out of bounds memory access

Run with --verbose=1000. It seems like the crashes are near

Writing interface file with hash XXX.
Building interface...

Things break down when attempting to write interface files. From the odd symbol prmtvzm0…readByteArrayzh_entry I suspect that maybe serializations are using too much memory.

My anticipation was wrong. There is some issue in vector-hashtables that selects the 64-bit mask for hash code, likely resulting some UBs. GHC WASM backend only has 32-bit address space.

✨ Patch accepted: https://github.com/klapaucius/vector-hashtables/pull/20. Has been released on Hackage.

Test-driving Agda in WASI runtimes

WASM engines usually compiles WASM bytecode into some more efficient intermediate formats and cache them, and the compilation phase may take a very long time. A cold start can even take >10s. Thus all timestamps are measured after 2~3 rounds of warming up.

wasmtime

wasmtime run --dir / --env PWD --env AGDA_DIR=$HOME/.config/agda \
         $(cabal list-bin agda) x.agda

→ OK, 0.83s for an empty file.

When including the patch for the inode number check, it sometimes triggers a bug and crashes: https://github.com/bytecodealliance/wasmtime/issues/6978.
Workaround: Do not mount the entire system. Avoid /dev specifically on macOS.

wazero

wazero run -mount=/:/ -env PWD=$PWD -env AGDA_DIR=$HOME/.config/agda \
       $(cabal list-bin agda) x.agda

→ OK, 3.06s for an empty file.

wasmer

Applied a patch to work around the inode number issue.

wasmer run --dir / --env PWD=$PWD --env AGDA_DIR=$HOME/.config/agda \
       $(cabal list-bin agda) -- x.agda

→ OK, 0.68s for an empty file.

Node.js 21 (broken; working after patched)

Use Node v21.2.0 with the wrapper script: https://gist.github.com/andy0130tw/63a3bf17c4ac0ae0717fb210f025ee16.
→ Bugged. Cannot even load an empty file. V8 itself crashes…

See the path issue above. Can be patched with user code. I guess that somehow the resources are exhausted during the infinite loop.

Other runtimes

To test: wasmedge, Bun, Deno.

The browser?

PoC done with horrible hacks. By WASI’s async nature, we only support the case the WASM is run in a web worker with SharedArrayBuffer available.

ghc-wasm-meta mentioned wasi-js.
Looks like an unfinished shim around WASI API is available for the browser: https://github.com/bjorn3/browser_wasi_shim.

New: @wasmer/sdk is released Dec 2023. Looks very promising, but my discovery is so close to my deadline that I have not done a PoC.

Interaction mode

Run without problem when stdin is from a file. The RTS (scheduler) seems to emit an excessive number of poll_oneoff calls and they hinder the actual work.

RTS calls select to poll on IO availability in non-threaded Haskell programs, and these call corresponding to poll_oneoff calls in WASI. Even if the poll_oneoff is implemented accurately, this is not very performant.

wasi-js’ hack is that to simply report unsupported for any poll on file descriptors (FD). It is the program’s job to figure out what to do next. However, this hack only works on polls. (p)select's limited interface does not support error reporting on individual FD, and because bailing out in this situation is unrealistic, the libc wrapper swallows most error code. As a result, we must implement the concrete logic to prevent select from breaking. I consider it a trade-off in wasi-libc.

What do other runtimes do? See for example, bjorn3/browser_wasi_shim#14's comment:

[…] An easy workaround […] is to just avoid stdin/stdout altogether and compile the application as a WASI reactor instead. However, I’ve since realised that this issue blocks any kind of asynchronicity on the Haskell side at all (e.g. halting a computation on a timeout). It would be really nice to get this fixed!

✨ Patch to wasi-js: https://gitlab.com/qbane/wasi-monorepo/-/commit/b8efbafda260000b22af9bff3c008e0cfdf5cd4e.

Studying RTS code (off-topic)

See note “No timer on wasm32” in rts/include/rts/Flags.h. In WASM32 the variable DEFAULT_TICK_INTERVAL is hardcoded to zero, effectively turning off the context switch timer altogether. This is equivalent to -V0.

Seemingly setting -V to non-zero in CLI RTS options makes Agda assume (?) a non-blocking stdin, and we have to handle excessive probing of stdin again. So just don’t.

Timer tick interval: RtsFlags.MiscFlags.tickInterval. It is also assigned to itimer_interval.
Context switch time: RtsFlags.ConcFlags.ctxtSwitchTime.

If GHCJS uses similar technique, maybe it is easier to diagnose under JS environment.

Fine-tuning Agda

Profiled build

Rebuilt everything with profiling turned on (ghc + agda). It was originally planned to use a debugger to dissect the illegal memory access issue. The problem was that the memory access violation did not happen. The program just hung.

Long warm-up time

ghc-wasm-meta suggests wizer, but with a “proper” WASI implementation, this is not needed as it does not add any new functionality for self-contained executables like agda.

Binary size

Baseline: ~45MB for a production build.

Proposal: https://github.com/WebAssembly/binaryen
The size is reduced to ~23MB with wasm-opt -O3 -Oz (!) despite a long (~5 minutes) build time.

Benchmarking

The compiled WASM binary is tested against these sources:

Red-black tree as a course material from FLOLAC ’22: https://gist.github.com/andy0130tw/92e4d05fda6e16d16fbcd4fd966ceb27/.
Built-in modules in Agda 2.6.5.
agda-stdlib v1.7.3 (only partially).

The modules are loaded in interaction mode to allow simultaneously loading multiple modules and avoid option conflicts of one another.

Future works to support Agda in browsers

Porting smalltt to WASM

smalltt has the following direct dependencies:

dynamic-array
strict-implicit-params
primdata
flatparse (v0.5.1.0)

flatparse requires integer-gmp since the mid of version 0.2.1.0. Note that if the GMP is not built for GHC (like for our custom backend), Cabal silently chooses 0.2.1.0, so you probably would not notice.

./hadrian/build --flavour=quick stage1:lib:integer-gmp

smalltt’s lexer and parser made heavy use of Template Haskell, so the compilation cannot proceed. However, since we know that they are indeed stateless, we can expand with compiler argument -ddump-splices, examine the output and substitute them manually.

The challange to compile TH into WASM

I have not made up my mind for this challange, but I can provide some context…

https://www.tweag.io/blog/2020-11-25-asterius-th/

https://github.com/reflex-frp/reflex-platform/blob/4b8b2f4dc748fda642137c982888088f4bd9c226/haskell-overlays/splices-load-save/load-splices.nix

When -ddump-splices flag is turned on, GHC outputs the expanded splices to stderr. Adding -ddump-to-file further redirect these messages into individual files. Unfortunately, automating this process seems difficult. Extra work is needed to complete missing imports or types.

iserv

This is GHC’s standard solution for understanding TH in cross-compilations. It works like an interpreter, reading instructions issued from the compiler and compute under the target’s architecture. However, iserv cannot build on wasm environment (unable to do dynamic linking), so we need to proxy it through: https://gitlab.haskell.org/ghc/iserv-proxy.

Implementing a language server in Haskell

I read the following tutorials and code for inspirations:

rzk:
- https://github.com/rzk-lang/rzk for the language server support and
- https://github.com/rzk-lang/vscode-rzk/ for the client
https://github.com/dhall-lang/vscode-dhall-lsp-server/
Possibility to run LSP in browsers, without a backend: https://hjr265.me/blog/codemirror-lsp/

Our focus is to maintain a mono-language codebase as possible. This means that we need to build our LSP server with pure Haskell and minimize code in other languages at the same time. For the scope of this project, two routes are explored:

Build the language server as a native binary and communicate with the language extension through TCP. Only minimal amount of JS code is required for the language server extension, which serves as the client.
Build the language server in WASM, and initiate the binary with WASI environment built into VS Code. The support is advertised on VS Code’s blog post, but as far as I know, few language server extension is implemented this way.

Compile Haskell’s lsp package to WASM

Extra work required:

Some dependencies of uuid cannot be built: it turns out that depending on only uuid-types is sufficient as UUIDv4 is all lsp needs.
Bump semirings to master to eliminate some redundant UNIX constants (commit) that cause compile errors.
Convert all TH in lsp-types 😞

List of TH splices

build/generated/Language/LSP/Protocol/Internal/Lens.dump-splices
build/src/Language/LSP/Protocol/Message/Lens.dump-splices
build/src/Language/LSP/Protocol/Message/Method.dump-splices
build/src/Language/LSP/Protocol/Message/Registration.dump-splices
build/src/Language/LSP/Protocol/Message/Types.dump-splices
build/src/Language/LSP/Protocol/Types/Lens.dump-splices
build/src/Language/LSP/VFS.dump-splices

The finished codebase is located at https://github.com/agda-web/lsp/tree/replace-th.

Proof of concept

A simple language server extension for smalltt is built for evaluation. It preforms type checks at each save, and cache the resulting context for future requests. Implemented features are:

If the code fails to type check, a diagnostic message is published to client. Position information is extracted from flatparse if available.
Provides hover popups on top definitions for peeking resolved terms and types. This is done by inspecting the symbol underneath the mouse cursor and querying it from the symbol table.
Provides minimal goto definition support on top definitions.

In practical language servers, the parsing and type-checking processes are done on the fly: introspection and diagnostics are updated as the user edits the code. Smalltt does not provide such functionality, and we do not want to show stale information, so the snapshot is taken every time the source file is saved and invalidated as soon as the buffer changes.

Acknowledgements

Courtesy of people in AIM (Agda Implementors' Meeting) XXXVII for discussing the idea. Special thanks to Andreas Abel for resolving some of the difficulties on the road of materializing the Agda WASM port. Also to Liang-Ting Chen for his presentation during the same week.

Addendum

Revisit 2024-06-14

I presented my findings at Functional Thursday #96. The slides are here, in Chinese (Taiwan).

I tried the setup script ghc-wasm-meta under Linux x86-64 and could confirm it working. It now supports {Linux,Darwin}-{x86_64,aarch64} (was Linux x86_64 only. Also, BSD utilities like tar, awk may not work, linking gtar, gawk are safer). One might not need the extra tools (Node.js, Deno, …) though.

At the beginning of this project, I crafted a slim Python script that aims at a minimal driver for setting up a cross compiler. Revisiting this was a good time to update my version to match the official shell script.

Also, there is some progress toward…

the fuzzy concurrent file I/O:
Draft: Remove the classic select() I/O manager (ghc!11700).
compiling Template Haskell:
Draft: Wasm backend Template Haskell support (ghc!12555).

I also did a quick survey on the support of non-blocking stdin, which was cruical for concurrent REPLs like Agda in interaction mode. See also this MR (ghc!11697) (not sure if it is useful for porting though).

Revisit 2024-12-15

After the Functional Thursday #100 party, I made a PoC as an attempt to see if Agda can run in interactive mode inside VS Code's extension environment (our eventual target is VS Code for the Web). It suffers from the exact same compatibility defect as most runtimes. Nevertheless, the sample extension is available on GitHub.

Revisit 2025-03-03

TH is now supported in WASM via a custom dynamic linker!