Closed womeier closed 5 months ago
Hi,
Currently, Wasocaml is starting from the Flambda
IR (FYI, in the future, probably before the end of the year, we're going to port it to Flambda2). And IIRC malfunction targets the Lambda
IR of the compiler. If that's the case, then it should be possible to write some glue code to call the compiler's internal that goes from Lambda
to Flambda
(closure_conversion
) in order to generate some Wasm code from Coq extracted code with Wasocaml.
Actually, it may even be possible to simply use a switch with Wasocaml as a compiler to get malfunction to compile to Wasm.
Also, TBH, for now, we're missing some pieces of the runtime (but we should be able to simply re-use what has been done in Wasm_of_ocaml) and the JS FFI has not yet been exposed (but we know it should be straightforward). If you're interested, please, drop us an e-mail. :)
Thanks a lot for the explanation! The figure with the IRs was quite helpful, as I'm not too familiar with OCaml's internals.
Currently, Wasocaml is starting from the
Flambda
IR (FYI, in the future, probably before the end of the year, we're going to port it to Flambda2). And IIRC malfunction targets theLambda
IR of the compiler. If that's the case, then it should be possible to write some glue code to call the compiler's internal that goes fromLambda
toFlambda
(closure_conversion
) in order to generate some Wasm code from Coq extracted code with Wasocaml.
This sounds like a good approach.
I think we'll wait for now, until the JS interface for WasmGC is settled...
I'd be curious to know if wasocaml supports compiling malfunction code or binary code to Wasm? (or if you plan to)
We'd like to use Coq's new OCaml extraction (which targets Malfunction instead of OCaml), and compile the result to Wasm.
Can we use wasocaml for that?
Thanks!