Bug#1038450: patch probably available

[julien.puydt@gmail.com]

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

Thanks!

J