On Tue, Jun 20, 2023, julien.pu...@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
