Le 12 avr. 2018 à 10:40, mukesh tiwari <mukeshtiwari.iiitm@gmail.com> a écrit :

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.