Bug#1101476: coq: Please whitelist ocaml-native-compilers to supported architectures
Le mercredi 08 octobre 2025 à 10:11 +0200, John Paul Adrian Glaubitz a
écrit :
> On Wed, 2025-10-08 at 10:00 +0200, Stéphane Glondu wrote:
> > Le 08/10/2025 à 09:49, John Paul Adrian Glaubitz a écrit :
> > > > > Could you therefore limit the ocaml-native-compilers build-
> > > > > dependency to the
> > > > > architectures which actually have a native OCaml compiler and
> > > > > allow the other
> > > > > architectures to use byte-code?
> > > >
> > > > The goal to put ocaml-native-compilers in Build-Depends was
> > > > exactly to
> > > > avoid builds on bytecode architecture... Because at that time,
> > > > coq was
> > > > randomly broken and upstream did not want to support that
> > > > configuration.
> > >
> > > I verified that it builds fine on multiple targets without native
> > > compiler
> > > support.
> > >
> > > > Did something change?
> > >
> > > Looks like as the failures are gone.
> >
> > Did you try reverse dependencies as well?
>
> I actually uploaded coq 9.1.0 to unreleased for sparc64 and I had
> hoped for
> the packages to start building, but it still shows BD-Uninstallable
> for coq-hott,
> so I will have to try manually.
>
> I will report back.
>
> Adrian
Ah, I forgot to answer about the whitelisting : unless they changed
their mind, they are not interested in supporting non-native
compilation, so even if it happens to work at the moment, I'm reluctant
to start shipping packages on architectures which I know upstream
doesn't care about: I don't feel I would be able to do anything by my
own if some broke at some point.
I might close this bug as a won't-fix eventually - keeping it open for
now to make it clear I'm not against the idea per se. I reject it for
some good reasons, but I'd like to be proven wrong.
Cheers,
J.Puydt
Reply to: