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