# Agda in WebAssembly & Experiments on Language Servers

> [!Note] Update
> The author has revisited this topic at Functional Thursday in June 2024. [See the end of this document for updates.](#Revisit-2024-06-14) 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:

- https://gitlab.haskell.org/ghc/ghc/-/wikis/building/hadrian
- https://gitlab.haskell.org/ghc/ghc/-/tree/master/hadrian/doc

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](https://github.com/agda/agda/blob/no-zlib/.github/workflows/cabal.yml):

# "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://github.com/haskell/cabal/issues/9563).

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](https://github.com/WebAssembly/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:

- https://www.tweag.io/blog/2022-11-22-wasm-backend-merged-in-ghc/#template-haskell
- https://asterius.netlify.app/th
## 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](https://github.com/tkaitchuck/aHash/wiki/AHash-fallback-algorithm) 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](https://github.com/huangjunwen/agda-wasm/blob/df09a4518bfac5fb6b857ff39dbcbecfd80bd107/patches/Agda-2.6.3/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](https://hackage.haskell.org/package/directory-1.3.8.1/docs/System-Directory.html#v: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`](https://agda.readthedocs.io/en/v2.6.4.1-rc1/tools/command-line-options.html#cmdoption-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](https://github.com/WebAssembly/wasi-libc/blob/wasi-sdk-20/libc-top-half/musl/include/stdlib.h#L131) [`realpath`](https://github.com/WebAssembly/wasi-libc/blob/wasi-sdk-20/libc-top-half/musl/include/stdlib.h#L131).

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

1. Recurses until “/..” is not recognized and rejected (wasmtime, wazero);
2. Stucks in a loop into resolving endless `/../../../`… (wasmer).
See https://github.com/rust-lang/rust/issues/82339;
3. Like 2., but recurses forever at home directory instead ([WASI API](https://nodejs.org/docs/latest-v18.x/api/wasi.html) in Node.js).
Maybe Node considers it a boundary?

Suggested mitigations:

1. Stop looking upward whenever there is an IO error.
(Not sure about my usage of `catchIO` thingy is correct)
2. 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](https://stackoverflow.com/questions/12768371/why-is-root-directory-always-stored-in-inode-two)).
3. 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.](https://nodejs.org/docs/latest-v21.x/api/wasi.html#security)

(✨) **Patch for Agda**: None. See [this article](https://hackmd.io/@q/wasm-wasi-realpath-issue) (updated 2025/11/2).

----------

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

1. `Writing interface file with hash XXX.`
2. `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](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/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](https://wasmer.io/posts/introducing-the-wasmer-js-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 `poll`s. `(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](https://github.com/WebAssembly/wasi-libc/blob/wasi-sdk-20/libc-bottom-half/cloudlibc/src/libc/sys/select/pselect.c#L116). 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](https://github.com/bjorn3/browser_wasi_shim/issues/14#issuecomment-1621402153):

> […] 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:

1. Red-black tree as a course material from FLOLAC ’22: https://gist.github.com/andy0130tw/92e4d05fda6e16d16fbcd4fd966ceb27/.
2. Built-in modules in Agda 2.6.5.
3. 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

- [ ] Compile with `enable-cluster-counting` turned on
- [x] Make a benchmark plan (:heavy_check_mark: 2025)
- [x] Run the official test suite for Agda (:heavy_check_mark: 2025)
- [x] Add back zlib dep. for WASM (:heavy_check_mark: 2024-06-14 with v2.6.4.3)
- [x] Replace GitRev with some build system tweaks (:heavy_check_mark: TH is supported!)
- [ ] Try to get Agda built with GHC JS backend
- [ ] Organize patches to GHC upstream
- [x] Organize my take on scripts for ghc-wasm-meta (:heavy_check_mark: 2024-06-16)
- [ ] Setup GitHub action runner for mac OS for prebuilt GHCs
- [x] Build a CI pipeline for agda.wasm (:heavy_check_mark: 2024-06-16)

# 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.

See also:

- https://medium.com/@zw3rk/cross-compiling-template-haskell-7e38c00c2914
- https://engineering.iog.io/2022-05-17-javascript-template-haskell-external-interpreter/
- Official wiki explaining the idea of external interpreter: https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/external-interpreter (might be out-of-date)

In smalltt’s case, we remove the plugin: `-fplugin StrictImplParams` and add `-fexternal-interpreter`, because they are mutually exclusive!

The current (GHC 9.6-ish) status is that libiserv, iserv-proxy, remote-iserv are integrated into GHCi.

Relevant notes in GHC codebase regarding to TH/GHCi:

- Note [Remote Template Haskell] in `libraries/ghci/GHCi/TH.hs`
- Note [Remote GHCi] in `compiler/GHC/Runtime/Interpreter.hs`
- Note [External GHCi pointers] in `compiler/GHC/Runtime/Interpreter.hs`
- Note [TH recover with -fexternal-interpreter] in `GHC.Tc.Gen.Splice`

Surprisingly GHCJS seemingly supports this approach well; should see how GHCJS deal with this (keyword: `thrunner.js`); See “`withExtInterp`” and “`withExtInterpStatus`” has special handling of `ExtJS`.

- https://github.com/MrAdityaAlok/ghc-cross-tools
- https://github.com/tweag/asterius/blob/master/asterius/src/Asterius/GHCi/Internals.hs

# 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:

1. 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.
2. 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](https://code.visualstudio.com/blogs/2023/06/05/vscode-wasm-wasi), 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](https://github.com/chessai/semirings/commit/2631c542b57abc9bc9e92db273ab8e80ae88048c)) that cause compile errors.
- Convert all TH in `lsp-types` 😞

**List of TH splices**

- [x] build/generated/Language/LSP/Protocol/Internal/Lens.dump-splices
- [x] build/src/Language/LSP/Protocol/Message/Lens.dump-splices
- [x] build/src/Language/LSP/Protocol/Message/Method.dump-splices
- [x] build/src/Language/LSP/Protocol/Message/Registration.dump-splices
- [x] build/src/Language/LSP/Protocol/Message/Types.dump-splices
- [x] build/src/Language/LSP/Protocol/Types/Lens.dump-splices
- [x] 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:

1. If the code fails to type check, [a diagnostic message](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics) is published to client. Position information is extracted from flatparse if available.
2. Provides [hover popups](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_hover) 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.
3. Provides minimal [goto definition](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_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](https://wiki.portal.chalmers.se/agda/Main/AIMXXXVII) 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](https://docs.google.com/presentation/d/1NLwXPKkatNrCtzOok8cnI5IvbA9CsKZGd-az0upFdiU/edit?usp=sharing), 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)](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11700).
* compiling Template Haskell: \
[Draft: Wasm backend Template Haskell support (ghc!12555)](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12555).

I also did [a quick survey](https://hackmd.io/@q/wasi-nonblocking-stdin) on the support of non-blocking stdin, which was cruical for concurrent REPLs like Agda in interaction mode. See also [this MR (ghc!11697)](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/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](https://github.com/andy0130tw/vscode-wasm-example).

## Revisit 2025-03-03

TH is now [supported](https://www.tweag.io/blog/2024-11-21-ghc-wasm-th-ghci/) in WASM via a custom dynamic linker!

## Revisit 2025-11-02

Wrote up an article to address and to workaround [the realpath issue](https://hackmd.io/YRi23ws3SS2gbNQNkpAGcA?both).