Bug#1101476: coq: Please whitelist ocaml-native-compilers to supported architectures
Hi,
Le jeudi 09 octobre 2025 à 20:47 +0200, John Paul Adrian Glaubitz a
écrit :
> 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.
The set of coq packages in Debian isn't ready for an upload right now,
but we'll see how things turn :
https://salsa.debian.org/ocaml-team/coq/-/commit/d76e2b1240b77becd23b9d3bf93988a3cf516fbc
Cheers,
J.Puydt
Reply to: