Twelf on Wasm

Twelf is an implementation, in Standard ML, of a logical framework based on the type theory LF.

Inspired by Twelf Live, and thanks to this PR against the MLton compiler, which adds a cross-compilation target for Wasm/WASI, you can now run twelf inside your browser.

Demo

Go here to interact with the twelf server.

Building for Local Development

From a fresh checkout, you can do

npm install
make build
make serve

to serve locally on port 8000.

Alternatively the default build target

make

runs a watch process, continually rebuilding javascript from typescript source.

Other make targets

make wasm

rebuilds the twelf.wasm asset in docker. This artefact is also checked into the repository, and it similarly does not need to be built from a fresh checkout.

make deploy

pushes to the deploy branch, which causes this Actions workflow to rebuild the static site.

make publish

pushes to the publish branch, which causes this Actions workflow to publish the npm package.