From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 7D653BC57 for ; Fri, 28 May 2010 23:06:01 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqcDAFLN/0uK54gDgWdsb2JhbACDGJsgFQEBFiIiiC6mP5BqgSaDBWoE X-IronPort-AV: E=Sophos;i="4.53,320,1272837600"; d="scan'208";a="63603060" Received: from rouge.crans.org ([138.231.136.3]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 28 May 2010 23:06:01 +0200 Received: from localhost (localhost.crans.org [127.0.0.1]) by rouge.crans.org (Postfix) with ESMTP id 98C3485D6 for ; Fri, 28 May 2010 23:06:00 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at crans.org Received: from rouge.crans.org ([10.231.136.3]) by localhost (rouge.crans.org [10.231.136.3]) (amavisd-new, port 10024) with LMTP id 4pUzLu2NpPOW for ; Fri, 28 May 2010 23:06:00 +0200 (CEST) Received: from [192.168.39.1] (fbx.up7.fr [88.185.141.188]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by rouge.crans.org (Postfix) with ESMTPSA id 6D25F806D for ; Fri, 28 May 2010 23:06:00 +0200 (CEST) Message-ID: <4C00303F.8010704@glondu.net> Date: Fri, 28 May 2010 23:06:07 +0200 From: =?UTF-8?B?U3TDqXBoYW5lIEdsb25kdQ==?= User-Agent: Mozilla-Thunderbird 2.0.0.22 (X11/20091109) MIME-Version: 1.0 To: caml-list Subject: Architectures with natdynlink support... X-Enigmail-Version: 0.95.7 OpenPGP: id=49881AD3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; bug:01 frisch:01 -cygwin:01 esac:01 restrictive:01 coq:01 ocaml:01 powerpc:01 powerpc:01 buildd:01 xavier's:01 phane:98 steph:98 0.3:98 phane:98 Hello, This is a follow-up on PR#5049 [1], but the bug has been closed and it seems no longer possible to comment on it now (and reopening doesn't seem relevant). [1] http://caml.inria.fr/mantis/view.php?id=3D5049 Alain Frisch wrote: > The list of platforms where natdynlink is supported is given in > the configure script. Currently, the list is quite > conservative, but it should be extended with feedback from > users who can test natdynlink on other platforms: Is there a practical test to be sure whether natdynlink works or not? What kind of "feedback" do you expect? > case "$host" in > *-*-cygwin*) natdynlink=3Dtrue;; > i[3456]86-*-linux*) natdynlink=3Dtrue;; > x86_64-*-linux*) natdynlink=3Dtrue;; > esac=20 That seems overly restrictive. As far as Debian is concerned, Coq dynamically loading ssreflect and compiling stuff works on all native architectures [2] (as of OCaml 3.11.2), that means: - powerpc (powerpc64-unknown-linux-gnu) - sparc (sparc-unknown-linux-gnu) - kfreebsd-i386 (i686-unknown-kfreebsd*-gnu) - kfreebsd-amd64 (x86_64-unknown-kfreebsd*-gnu) - hurd-i386 (i386-unknown-gnu0.3) - amd64, i386 (linux kernel) [2] https://buildd.debian.org/status/package.php?p=3Dssreflect If I understand correctly Xavier's explanation in [1], it should work on any x86-GNU-based system where shared libraries are supported (and not only Linux!). Natdynlink working on sparc and powerpc seems to be a surprise, but not the other ones AFAIU. Maybe people on this list can also report working natdynlink on other systems. Maybe adding a ./configure option would be more flexible? Best regards, --=20 St=C3=A9phane