Agda Language Server WASM Loader

A helper extension to load and spin up a functional instance of the WebAssembly build of Agda Language Server.

Designed to work jointly with Agda mode for VS Code, this extension contains a patched instance of the WASM WASI Core Extension. Consequently, the consumer of this package is expected to prepare a WASM module that is compiled with WebAssembly.compile, along with all data files and interface files, placed in a in-memory VFS.

Sample usage

Use this in your extension activation script as a starting point:

import { LanguageClient, LanguageClientOptions } from 'vscode-languageclient'

const ext = extensions.getExtension('qbane.als-wasm-loader')

if (!ext.isActive) {
  await ext.activate()
}

const {
  AgdaLanguageServerFactory,
  WasmAPILoader,
  createUriConverters,
} = ext.exports

const wasm = WasmAPILoader.load()
const alsWasmRaw = await workspace.fs.readFile(Uri.joinPath(context.extensionUri, 'path/to/als.wasm'))
const mod = WebAssembly.compile(alsWasmRaw)

const factory = new AgdaLanguageServerFactory(wasm, mod)
const memfsAgdaDataDir = await wasm.createMemoryFileSystem()
// TODO: may need to populate memfsAgdaDataDir;
// see the note section "Preparing the memory filesystems" below

const serverOptions = () => factory.createServer(memfsAgdaDataDir, {
  // TODO: extra process options for vscode-wasm
}, {
  // env: { ENV: 'EXTRA_ENVS' },
  // args: [
  //   '+RTS', '-V1', '-RTS',  /* the default args */
  //   '+AGDA', '... Agda args here ...', '-AGDA'
  // ],
  // async presetupCallback({ memfsTempDir, memfsHome }) {
  //   // you might want to put configs or libraries in the file system
  // },
  // runSetupFirst: true,
  // setupCallback(code, stderr) {},
})
const clientOptions = {
  // TODO: add more client options
  uriConverters: createUriConverters(),
}

const client = new LanguageClient('als', 'Agda Language Server', serverOptions, clientOptions)
client.registerProposedFeatures()

client.onRequest('agda', (res, opts) => {
  // TODO: add your own callback handling logic
})

Note: Preparing the memory filesystems

You need a copy of Agda's built-in files to be extracted in the memfs for Agda to function properly. This loader provides a helper function memfsUnzip for this task:

// const ext = extensions.getExtension('qbane.als-wasm-loader')
const resp = await fetch('path/to/agda-data.zip')
await ext.exports.memfsUnzip(memfsAgdaDataDir, await resp.bytes())

You can setup other memfs' in the hook presetupCallback. Be careful of mount points!

The setup step (Agda v2.8.0 or later)

Starting with newer ALS (containing this patch) powered by Agda v2.8.0 or later, you can skip the memfs preparation step with the option runSetupFirst. The factory will run command als --setup before actually running the server, extracting data files (in v2.8.0 this is ~600 kB) to the memfs' datadir. The downside is that no interface file for Agda built-ins will be written due to memfs being read-only at runtime (for now).

The setup step can be monitored by passing a function to setupCallback, which is called once the setup process is exited, with the exit code and the piped content of stderr as parameters, respectively. If this step fails and the callback is not set, the server will crash before its start.

Acknowledgements

The included WASM WASI Core Extension fixes some WASM/WASI issues to satisfy Haskell-based WASM modules' need, including but not limited to:

• https://github.com/microsoft/vscode-wasm/pull/226