search

stedolan / malfunction

Malfunctional Programming
Other
326 stars 20 forks source link

Question: Compiling to OCaml byte code? #42

Open mkarup opened 2 months ago

mkarup commented 2 months ago

Is it possible to use malfunction to compile a .mlf file to OCaml byte code?

stedolan commented 2 months ago

Not currently, no, although it's probably not a huge amount of code to make it do so. What's the use case?

mkarup commented 2 months ago

I'm investigating different ways of extracting Coq programs to WebAssembly binaries. One way to do this is to extract to OCaml, and from there use wasm_of_ocaml. This uses the standard OCaml extraction, which still has a few issue.

A new verified extraction is being proposed as a replacement and at the moment it targets malfunction. I'm interested in using this and then compiling to WebAssembly, but wasm_of_ocaml compiles from OCaml bytecode.

I realize that the use case is quite niche/ obscure, so if it is not currently possible it's not of high priority. Out of curiosity, do you perhaps know of any other (relatively easy) ways to compile a .mlf file to a WebAssembly binary?

There is also wasocaml which is a drop-in replacement of ocamlopt (which I see that the malfunction compiler uses), but the last commit is ~6 month old, and the WebAssembly that is emitted is no longer valid (it emits files in an old version of the Wasm text format). I know that I could probably submit a PR to help fix that, but I don't currently have the time (as said, looking for relatively easy ways).

zapashcanon commented 1 month ago

@mkarup, Wasocaml was outputting the custom text format used by binaryen at the time. I believe it is now fixed in binaryen and we could output standard Wasm. If you open issues with the errors you encountered I can easily fix them.

stedolan commented 1 month ago

Right, that makes sense. The simplest thing would be to get Malfunction to generate cmo files, which are the bytecode-compiled versions of a single OCaml module. You'll then need to link the cmo file with any libraries in use to get a bytecode file, using an ocamlc invocation like the one on the page you linked (ocamlc accepts cmo files in the same places it accepts ml files of OCaml source code).

stedolan commented 1 month ago

I had a go at this in #43 . There are some instructions to try it out in the PR description, let me know whether it works with wasm_of_ocaml

mkarup commented 1 month ago

My apologies for the radio silence, vacation time.

I had a go at this in #43 . There are some instructions to try it out in the PR description, let me know whether it works with wasm_of_ocaml

Awesome, thank you! I will try it out and let you know. Also, thank you for the info on the OCaml compiler toolchain, I'm still a novice in that regard.

@mkarup, Wasocaml was outputting the custom text format used by binaryen at the time. I believe it is now fixed in binaryen and we could output standard Wasm. If you open issues with the errors you encountered I can easily fix them.

Right, I will try to gather the errors and open an issue.

mkarup commented 1 month ago

The bytecode compilation in the PR works for my purposes! (I haven't tested anything other than running the bytecode and compiling it to Wasm) I don't know if it will be useful for anyone else, but thank you so much for the effort, I really appreciate it!