Hi Everyone,
I am trying to call some Java functions from OCaml (Extracted from Coq if it matters). I am familiar with ocamljava [1], but it says that "
The generated code usually runs faster than OCaml bytecode but slower
than native code. Memory consumption and startup time are also higher,
but leveraging the multiple cores of a machine can help reaching the
performance level of native code.", and I don't want to leave the OCaml native code. One suggestion I got on #ocaml channel is using RPC and a quick Google search leads to ocaml-rpc [2]. I am wondering if experts from OCaml community could please give me some suggestions.
For the record, the performance of ocamljava-compiled code
heavily depends on the programming style. Numerical imperative
or i/o-bound code can be on par with ocamlopt-compiled code,
while code based on exceptions for control flow or abundant indirect
calls can be slower than ocamlc-compiled code. I am afraid
extracted code is likely to fall in the second category.
It is also noteworthy that you can run into problems with extracted
code. I suspect extracted code might contain call to "Obj.magic",
as the type system of Coq is slightly more powerful than the one
of OCaml. The issue is that that OCaml-Java uses a different
memory layout, so that "Obj.magic" might not yield the same result
as in vanilla OCaml.
Best regards,
Xavier Clerc
PS: if you are able to share your code, I might be able to give you
a less generic assessment.