Lean2Wasm
Tool to compile Lean4 code to WASM. Right now this is really just for me to test things out. So actually using it is a little scuffed right now :)
This is largely a translation of these instructions into something that can be executed.
This requires emcc to already be installed.
Usage
Run lake build test to build the test program. Then run lake build to build
the utility. Running lake exe lean2wasm will compile the Main program.
Once compiled, you can run node .lake/build/wasm/main.js to run the program.
Alternatively you can use lake run js.
If you want to change what is being compiled, in Lean2Wasm.lean just change
the root variable.
Example
Here is an example of embedding lean
into a webpage. Importantly, we have to use the MODULARIZE flag so that we
can invoke the main function multiple times since there are issues with doing
so without resetting the emscripten runtime (specifically, emscripten generates
a factory function which can then be invoked to initialise the runtime again
and call main).