From: "Stéphane Glondu" <steph@glondu.net>
To: caml-list <caml-list@inria.fr>
Subject: Architectures with natdynlink support...
Date: Fri, 28 May 2010 23:06:07 +0200 [thread overview]
Message-ID: <4C00303F.8010704@glondu.net> (raw)
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=5049
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=true;;
> i[3456]86-*-linux*) natdynlink=true;;
> x86_64-*-linux*) natdynlink=true;;
> esac
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=ssreflect
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,
--
Stéphane
next reply other threads:[~2010-05-28 21:06 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-28 21:06 Stéphane Glondu [this message]
2010-05-29 4:22 ` [Caml-list] " rixed
2010-05-31 10:04 ` Alain Frisch
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4C00303F.8010704@glondu.net \
--to=steph@glondu.net \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox