From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 3CC21BBFB for ; Sat, 18 Jun 2005 09:48:16 +0200 (CEST) Received: from smtp3.adl2.internode.on.net (smtp3.adl2.internode.on.net [203.16.214.203]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j5I7mED7032037 for ; Sat, 18 Jun 2005 09:48:15 +0200 Received: from rosella (ppp35-43.lns1.syd2.internode.on.net [59.167.35.43]) by smtp3.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id j5I7lvQj024170; Sat, 18 Jun 2005 17:17:59 +0930 (CST) Subject: Re: [Caml-list] Running bytecode... From: John Skaller To: Alex Baretta Cc: felix-language@lists.sourceforge.net, Jonathan Roewen , caml-list@yquem.inria.fr In-Reply-To: <42B29E7A.9000104@barettadeit.com> References: <42B29C33.1010302@barettadeit.com> <42B29E7A.9000104@barettadeit.com> Content-Type: text/plain Date: Sat, 18 Jun 2005 17:47:57 +1000 Message-Id: <1119080877.6746.52.camel@rosella> Mime-Version: 1.0 X-Mailer: Evolution 2.3.3 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 42B3D1BE.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 bytecode:01 baretta:01 ocaml:01 byte-code:01 dynlink:01 dynlink:01 ocaml:01 scaml:01 -pack:01 binary:01 extern:01 compilation:01 compiler:01 ...:98 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: On Fri, 2005-06-17 at 11:57 +0200, Alex Baretta wrote: > Jonathan Roewen wrote: > >>The short answer is you can't. It's a pity, but to the present day the > >>vanilla Ocaml distribution does not support mixing native and byte-code. > >>Also, it is not possibile to Dynlink native code, which is even more of > >>a pity. > > > > > > Well, dynlink with native code probably isn't desirable, as can't > > really verify it. > > Actually, this is very desirable. Ask Jon Skaller, who is developing the > Felix language mainly because Ocaml does not have this feature. > Scaml does this, but there is no correctness proof for it. It is a patch > to 3.07. Unluckily Xavier wants to have an provably perfect solution to > this problem, which is definitely a good thing, but this delays such a > great feature as native dynlink. My opinion of the situation is: INRIA people like to have a mathematical basis for things, but that isn't the same as requiring a perfect solution or demanding a correctness proof. The usual reason for liking a constructive proof is that it actually tells the algorithm. I believe there are two reasons for not supporting native code dynamic loading in Ocaml: (1) It is a lot of work. The first step, dynamic loading of C parts of the system, has already been implemented. It makes sense to deal with the issues arising from this first. (2) A too hasty design would preclude a better one permanently .. an example is the -pack switch ;( As to Felix: it is designed to inter-operate with C/C++ on both source and binary levels. At this stage you can 'dlopen()' any C library and 'dlsym()' any function in it. However the binding is exactly as in C: you have to use string names for functions, which basically means you have to use extern "C" names. This is not very safe: the only error check is whether a symbol exists. There's no type checking, even less than what C++ would provide with typesafe linkage. The main difference to Ocaml is that it can actually be done, albeit unsafely, which is a correct first order solution for Felix, since binding to non-Felix C libraries is a requirement (and that can't be safe because C isn't). I will be working on better solutions, in particular leveraging C++ type safe linkage, however a full scale native Felix-Felix dynamic linkage has as a precondition separate compilation, which is currently not supported: Felix can generate and call C libraries of course: the compiler targets shared libraries, a program is just a library with an init function. There is an example of Felix plugins in the tutorial and in the Alioth Shootout. -- John Skaller Download Felix: http://felix.sf.net