From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 9F97F82416 for ; Thu, 12 Apr 2018 12:01:12 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f178.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.216.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.216.178 as permitted sender) identity=mailfrom; client-ip=209.85.216.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qt0-f178.google.com) identity=helo; client-ip=209.85.216.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-qt0-f178.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ax8kCsR3uRytJron1smDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?seIULPad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnii?= =?us-ascii?q?kHOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZA42z?= =?us-ascii?q?dZAAD/AAPelGq4n2ukYAoge+BQayHuPg1CVIjWLx0K01yesuChvG3A0+ENIKqn?= =?us-ascii?q?jUt8n6NKcMXuCv0qbI1y7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGQ3CjlWV?= =?us-ascii?q?s4PlPjWV2/wKs2eH9eVgUOavi2w9pAFvuDej3MAsipPGho4NxVDE9Dl5wIYoJd?= =?us-ascii?q?KjUkJ0fdmkEJ5WuiqHNIV2WtsvT390tCs+0LELup62cDIUxJg6xhPTceGLfoqL?= =?us-ascii?q?7x/lSe2fOy13hGh/d7K6nxuy8Vavyun7VsSs1VZFtCtFkt3VunAUyxzf9tGLSv?= =?us-ascii?q?Vg8kqj2juDzQ/T6uZDIUA7karUNYQtzaI3lpoWqUjDHyn2l1vqjKKOaEko5uyl?= =?us-ascii?q?5/7kb7jmvJOQKZJ4hwDkPqgzmMGyAvw0Mg0UUGia/eS82qfj/Ur8QLhSgf05iL?= =?us-ascii?q?LWsIrbJcsFoq61GRRV3Zoj6xmhFTepzs4YkGIILFJAYh2HjozpN0vSL/D/CPez?= =?us-ascii?q?m06snytzx/DaIr3hBY3AIWTZn7fkebZx8kpcyAsozdBD/J9UEbEAIPfrWkDrrt?= =?us-ascii?q?DYDxk5Mxa1w+n9Etl92JkeCiqzBfqcLaDfql/A+uMwKvONLNsQpTXwMPg55uHn?= =?us-ascii?q?l35/mF4cYayB0p4eaXT+FfNjdRa3e33p1/gIG30Lsw52d+fqhUePS3YHaH+4Ra?= =?us-ascii?q?Mx4ncgA4KrF4rZbo+oib2Fmiy8G8sFNSh9FlmQHCKwJM2/UPAWZXfKe54zonk/?= =?us-ascii?q?TbGkDrQZ+1SrvQ7+xaBgK7ONqCIdvJPnktNy4r+KzE1gxXlPF82Yllq1YSRshG?= =?us-ascii?q?pRHm052al+pQp2zVLRifEl0cwdLsRa4rZyail/NZPYyLYkWdX7WwaEZ8vRDVj/?= =?us-ascii?q?HYXgDjY2QdY8hdQJZhQlFg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AfAQCZLc9ahrLYVdFcg0hPPW8VEwqDW?= =?us-ascii?q?YEdglCRI4F0gQ+SYxSBZwsjhGACgiAHGQcBBDAYAQIBAQEBAQEBAQETAQEBCAs?= =?us-ascii?q?LCCgjDII1IoJMAQICASMdARsPDgEDAQsGBQs3AgIhAQERAQUBHAYTCQsHhFkBA?= =?us-ascii?q?w0ID5wBPIsFgX8FAReCbwWDTAoZJg1UV4InAgYSh2uBVD+DbC6CT0ICgSRpglO?= =?us-ascii?q?CVAKXMSwIgWCDdoVkgn2BM4NahzeJIz2GIw8DHoEEHGuBHzMaI08xghIJgWcwD?= =?us-ascii?q?gl6AQiCQoUUhUA9MI8BAQE?= X-IPAS-Result: =?us-ascii?q?A0AfAQCZLc9ahrLYVdFcg0hPPW8VEwqDWYEdglCRI4F0gQ+?= =?us-ascii?q?SYxSBZwsjhGACgiAHGQcBBDAYAQIBAQEBAQEBAQETAQEBCAsLCCgjDII1IoJMA?= =?us-ascii?q?QICASMdARsPDgEDAQsGBQs3AgIhAQERAQUBHAYTCQsHhFkBAw0ID5wBPIsFgX8?= =?us-ascii?q?FAReCbwWDTAoZJg1UV4InAgYSh2uBVD+DbC6CT0ICgSRpglOCVAKXMSwIgWCDd?= =?us-ascii?q?oVkgn2BM4NahzeJIz2GIw8DHoEEHGuBHzMaI08xghIJgWcwDgl6AQiCQoUUhUA?= =?us-ascii?q?9MI8BAQE?= X-IronPort-AV: E=Sophos;i="5.48,441,1517871600"; d="scan'208,217";a="322511618" Received: from mail-qt0-f178.google.com ([209.85.216.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 12 Apr 2018 12:01:11 +0200 Received: by mail-qt0-f178.google.com with SMTP id s48so5488386qtb.10 for ; Thu, 12 Apr 2018 03:01:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=kDRiZoKekDj0OdJtD56E4OoqoTdPyoG23ycWnk/2abQ=; b=eSW9MBLSUyIUygTpdhE0hO90yaWibuZ2TE7UhLqv1laOs/5k2diaXHBfu/tt0tXQUc GFbX6qsAa0ycwpylDP+53HYR/c5WTvr8EPgafpSrHRBfxs3ARelwkBRvaia7Ui/k5Ccw 7mVaxFfdMEEPWCwU+sIlE5urf1g9pMdeXTlPmQGoI5zztZoOIn0lr9Ea2Ei5laMlgBAc YetVTOVCdydPZvb3WM/f9boNoQYCpOiaT2TFAONHQ6K7n8fzhZfPrAGIyPXeNz02O7a9 TYVh/sY7eKoNuMefeDWPokTOmhFRrdyLQIyH5hDbMdTNVnS7xCkbcrDoaRpSz6BIKBHb v7pw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=kDRiZoKekDj0OdJtD56E4OoqoTdPyoG23ycWnk/2abQ=; b=PAQsTIK+PYzGGlGGp4RshrHjBhRDyK75OeJwBS7Tk6yYi2pgrt38aifEg8f3nevTwB 12aneJth8OYrcv2aQ9yLb7JN9OYXR5YMILlzEshZcVokrsK71E0pR93EPyZ8eMdHKWYn hQjFehmXqKpx6LpLyafc34r8E3DtowdAQnuo90fR4H8iWL2IPT55DyuWiLrD8+3QrWJ3 Av2z+xHwiYA9w27JHaJCw/bRQDEZ4+9mCzlpoU23u/nTmc01ZyMCyNRlFezznW8LA4Z7 h8JsySpom9Nyxb2S2gFkJX9P6J+B/6a+nNsZiDN39C0qcKWSfUOBW9mBZuJ6TGwFRVuY jPwQ== X-Gm-Message-State: ALQs6tDnn3M27PnWmQv1piENtrYHvp/1Ta4rtQn0ApjtJEjE2fZBksct kcgEr9eL+msoEUYo5MozRISihmWJ2oAHRcpBmeA= X-Google-Smtp-Source: AIpwx48LNhSXskYArbWlcrRPNRatZblxyoM+abyXs672a6kblGD3n+aYQuFXASovJ+lE7JKkDABFx0uLSWfoZl79UCQ= X-Received: by 10.237.37.202 with SMTP id y10mr328612qtc.62.1523527270258; Thu, 12 Apr 2018 03:01:10 -0700 (PDT) MIME-Version: 1.0 Received: by 10.12.132.3 with HTTP; Thu, 12 Apr 2018 03:00:29 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Thu, 12 Apr 2018 12:00:29 +0200 Message-ID: To: mukesh tiwari Cc: caml users Content-Type: multipart/alternative; boundary="001a11420908bfddcf0569a3d558" Subject: Re: [Caml-list] Calling Java function from OCaml --001a11420908bfddcf0569a3d558 Content-Type: text/plain; charset="UTF-8" Remote procedure calls are a generic solution to cross-language computations that works in many settings. It is a perfectly reasonable thing to do. Another option is to use Foreign Function Interfaces on both sides to do cross-language computation in a single system process (instead of RPCs and communicating processes). For Java, the FFI layer in the JNI (Java Native Interface), and there exists a library to make OCaml and Java functions communicate through the JNI (without changing the OCaml compilation backend): https://github.com/xavierleroy/camljava That said, this library seems to currently lack active users, and in particular nobody did the work of packaging it on opam ( https://github.com/ocaml/opam-repository/issues/7519 ). If you are willing to give this library a try, it could be a useful thing to contribute. In either cases, I would recommend being very careful in designing the interface between Coq code and untrusted code (pure OCaml, or OCaml+Java code using whichever coordination system). It is easy to shoot yourself in the foot by exporting untrusted functions with an optimistic type (eg. using the Coq function type for the untrusted functions that may not be total / strongly terminating). If you can design the interface between Coq and untrusted code as primarily based on exchanging ground *data* (events, queries reified as algebraic datatypes...), with an explicit loop orchestrating the coordination between both, you can get a system where the correctness guarantees (or lack thereof) are much easier to reason about. Incidentally, this design also makes the in-process data exchange more similar to what an inter-process communication system would look like, so it allows implement both solutions (in-process or remote communication) against a single Coq codebase, with minimal changes. (As an aside: the #ocaml channel is also populated by experts from the OCaml community, so its advice is probably as good as the list.) On Thu, Apr 12, 2018 at 11:40 AM, mukesh tiwari < mukeshtiwari.iiitm@gmail.com> wrote: > 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. > > > Best regards, > Mukesh Tiwari > > > [1] http://www.ocamljava.org/ > [2] https://github.com/mirage/ocaml-rpc > --001a11420908bfddcf0569a3d558 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Remote procedure calls are a generic soluti= on to cross-language computations that works in many settings. It is a perf= ectly reasonable thing to do.

Another option is to use Foreign= Function Interfaces on both sides to do cross-language computation in a si= ngle system process (instead of RPCs and communicating processes). For Java= , the FFI layer in the JNI (Java Native Interface), and there exists a libr= ary to make OCaml and Java functions communicate through the JNI (without c= hanging the OCaml compilation backend):

=C2=A0 https://github.com/xa= vierleroy/camljava

That said, this library seems to curren= tly lack active users, and in particular nobody did the work of packaging i= t on opam ( https://github.com/ocaml/opam-repository/issues/75= 19 ). If you are willing to give this library a try, it could be a usef= ul thing to contribute.

In either cases, I would recommend bei= ng very careful in designing the interface between Coq code and untrusted c= ode (pure OCaml, or OCaml+Java code using whichever coordination system). I= t is easy to shoot yourself in the foot by exporting untrusted functions wi= th an optimistic type (eg. using the Coq function type for the untrusted fu= nctions that may not be total / strongly terminating). If you can design th= e interface between Coq and untrusted code as primarily based on exchanging= ground *data* (events, queries reified as algebraic datatypes...), with an= explicit loop orchestrating the coordination between both, you can get a s= ystem where the correctness guarantees (or lack thereof) are much easier to= reason about. Incidentally, this design also makes the in-process data exc= hange more similar to what an inter-process communication system would look= like, so it allows implement both solutions (in-process or remote communic= ation) against a single Coq codebase, with minimal changes.

(As an aside: the #ocaml channel is also populated by expe= rts from the OCaml community, so its advice is probably as good as the list= .)



=
On Thu, Apr 12, 2018 at 11:40 AM, mukesh tiwari = <mukeshtiwari.iiitm@gmail.com> wrote:
Hi Everyone,
I am trying to call some Java functions from OCaml (Extracted from Coq i= f it matters). I am familiar with ocamljava [1], but it says that "= The generated code usually runs faster than OCaml bytecode but slower=20 than native code. Memory consumption and startup time are also higher,=20 but leveraging the multiple cores of a machine can help reaching the=20 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].=C2=A0 I am wondering if e= xperts from OCaml community could please give me some suggestions.

=
Best regards,
Mukesh Tiwari

--001a11420908bfddcf0569a3d558--