Bug#1038450: patch probably available

[Adrien Nader <adrien@notk.org>]

On Tue, Jun 20, 2023, julien.puydt@gmail.com wrote:
> Hi,
> 
> Le mardi 20 juin 2023 à 15:35 +0200, Adrien Nader a écrit :
> > I was looking at the migration for coq on Ubuntu and a build failure
> > on armhf is preventing it.
> > 
> > I expect that this issue is fixed by the following commit:
> >  
> > https://github.com/UniMath/UniMath/commit/1716c078b00c18dcabf63f671e414d7ba33cb23c
> > 
> >   Split the proof of associators_equiv to make sure it fits inside 32
> > b…
> > 
> >   …its (#1687)
> > 
> >   This is necessary to create a jscoq addon for UniMath
> >   (https://github.com/UniMath/UniMath-jsCoq).
> > 
> > I haven't tried the patch yet and wanted to ask first if you're
> > interested in restoring support for 32-bit arches. I honestly don't
> > know
> > if there's a lot of users on these (except maybe for JS).
> 
> If you can confirm that commit solves the issue, I'll add it as a patch
> to the Debian packaging and drop my latest change. I'm interested in
> having different platforms to detect subtle breakages.
> 
> Notice that I also reported to Coq upstream:
>   https://github.com/coq/coq/issues/17749

The patch seems to fix the issue. I say "seem" because the build
compiled the file that was failing to build but the build is not done
yet: emulated armhf isn't fast. :) 

But since I reprocued the build failure before, I am fairly confident
this build will succeed.

-- 
Adrien