Bug#1101476: coq: Please whitelist ocaml-native-compilers to supported architectures
On Thu, 2025-10-09 at 20:43 +0200, Julien Puydt wrote:
> I see the discussion is still ongoing, and I notice that my point about
> spreading thin has been made by upstream.
>
> I don't think they completely closed the door to the contribution, it's
> just that this new arch isn't on their radar yet...
FWIW, they claim that coq with byte compilers is supposed to work, quoting:
»The lack of support for Rocq on bytecode-only architectures looks to me like
a potential issue with the packaging of Rocq, rather than a fundamental issue
with the OCaml compiler. As far as I know, it is perfectly possible to use Rocq
in bytecode mode (of course it is slower than in native mode, but usable), and
there is support in the Rocq configure script for this scenario.«
Source: https://github.com/ocaml/ocaml/pull/11974#issuecomment-3381299696
Can we give it a try? I mean, we still have a lot of time for testing until forky
gets frozen. We can still revert it if it doesn't work.
Adrian
--
.''`. John Paul Adrian Glaubitz
: :' : Debian Developer
`. `' Physicist
`- GPG: 62FF 8A75 84E0 2956 9546 0006 7426 3B37 F5B5 F913
Reply to: