Hello, I just tried building coq on ppc64 by overriding the build-dependencies and it's generally supported, there is just a warning about byte-code being used. 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? Thanks, Adrian
Hi, attaching a patch which allowed me to build coq 9.1.0+dfsg-1 on architectures without a native OCaml compiler. Could you please apply this patch for the next upload of coq in experimental? Thanks, Adrian
Hello, Le 28/03/2025 à 08:16, John Paul Adrian Glaubitz a écrit : 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. Did something change? If bytecode is fully supported, then the simplest would be to remove ocaml-native-compilers from Build-Depends altogether. Cheers,
Hi Stéphane, I verified that it builds fine on multiple targets without native compiler support. Looks like as the failures are gone. OK. Adrian
Le 08/10/2025 à 09:49, John Paul Adrian Glaubitz a écrit : Did you try reverse dependencies as well? Cheers,
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
Hi, Le mercredi 08 octobre 2025 à 10:11 +0200, John Paul Adrian Glaubitz a écrit : I'm actually actively maintaining the Coq/Rocq related packages in Debian, even if it doesn't show that much. :-/ There is a big transition (renaming from Coq to Rocq), which is partial in the various upstreams and which for this reason shouldn't appear in Debian yet. Indeed, I'd rather make a complete transition at once rather than handle a continuous mess! My current status on updating the packages is at the end of this paragraph, but it doesn't show: - the rocq-stdlib package stands in the NEW queue, so it's a roadblock until it clears ; - the paramcoq package is obsolete upstream so will need removal (already not in my to-work-on below) ; - but the current coqeal in Debian still depends on paramcoq, so it's too eatrly for a RM bug ; - the next coqeal doesn't build correctly with Coq/Rocq 9.1 yet ; - the dh-coq package will need a new version too to cope with the new deps ; - I have a metacoq package in store (I thought I had uploaded it already, but apparently not...). Here is my org-mode chunk on the matter: * Update Coq/Rocq in Debian [5/8] - [X] step 1 [2/2] - [X] elpi 3.4.1-1 - [X] rocq 9.1.0-1 - [X] step 2 [1/1] - [X] rocq-stdlib 9.0.0-1 - [X] step 3 [16/16] - [X] aac-tactics 8.20.0-2 - [X] coq-bignums 9.0.0+rocq9.1-1 - [X] coq-dpdgraph 1.0+9.0-1 PATCH - [X] coq-elpi 3.4.0-1 BEWARE touchy compilation? - [X] coq-ext-lib 0.13.0-2 - [X] coq-hammer 1.3.2+9.0 PATCH - [X] coq-hott 9.0-2 PATCH - [X] coq-libhyps 2.0.8-5 - [X] coq-menhirlib 20250912+ds-1 - [X] coq-record-update 0.3.6-1 - [X] coq-reduction-effects 0.1.6-1 - [X] coq-stdpp 1.12.0-1 - [X] coq-unicoq 1.6-8.20-2 PATCH - [X] coq-unimath 20240923-1 - [X] flocq 4.2.1-2 - [X] ott 0.34+ds-2 - [-] step 4 [6/8] - [ ] coq-equations 1.3.1-9.0-1 FAIL Sorts.family unbound type constructor - [X] coq-gappa 1.7.1-1 - [X] coq-hierarchy-builder 1.10.0-1 - [X] coq-iris 4.4.0-1 - [X] coq-math-classes 9.0.0-1 - [ ] coq-mtac2 1.4+8.20-2 PATCH - [X] coq-simple-io 1.11.0-2 - [X] coqprime 8.20.1-2 - [-] step 5 [2/3] - [X] coq-corn 9.0.0-1 - [ ] metacoq 1.4-9.0-1 WAIT coq-equations - [X] ssreflect 2.4.0-1 - [X] step 6 [8/8] - [X] coq-deriving 0.2.2-1 - [X] coq-reglang 1.2.2-1 - [X] coq-relation-algebra 1.8.0-1 - [X] coquelicot 3.4.4-1 - [X] mathcomp-bigenough 1.0.3-1 - [X] mathcomp-finmap 2.2.1-1 - [X] mathcomp-zify 1.5.0+2.0+8.16-5 - [X] coq-quickchick 2.1.1-1 - [X] step 7 [6/6] - [X] coq-extructures 0.5.0-2 - [X] coq-interval 4.11.3-1 - [X] mathcomp-algebra-tactics 1.2.7-1 - [X] mathcomp-analysis 1.13.0-1 - [X] mathcomp-multinomials 2.4.0-1 - [X] mathcomp-real-closed 2.0.3-1 - [ ] step 8 [0/1] - [ ] coqeal 2.1.0-2 PATCH but still FAIL!? We will get somewhere at some point, but for now most of the work is behind the scene. Cheers, J.Puydt
Le mercredi 08 octobre 2025 à 10:11 +0200, John Paul Adrian Glaubitz a écrit : 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
I have to admit that I don't understand why OCaml upstream is so hostile against other architectures. They have removed basically every architecture from native support except for x86_64, arm64, ppc64el, riscv64 and s390x and they also refusing to add new ones like loongarch64. Plus, they're making it hard to use the byte compiler. Really strange attitude towards downstreams. But I guess I'll just ignore OCaml stuff for now. Adrian
Le mercredi 08 octobre 2025 à 10:58 +0200, John Paul Adrian Glaubitz a écrit : I don't know if it's really hostility -- perhaps just missing the hands and hardware to cover as much ground as they'd like... J.Puydt
There are projects like the GCC Compile Farm that provide access to various hardware and software platforms for testing. No one needs to own all of that hardware. I also don't think they own a s390x mainframe which costs a couple of millions of Dollars, so I doubt it's this. On the other hand, they could even get free LoongArch hardware if they bothered to add LoongArch support [1]. I guess it's a works-for-me project and not a community project. At least that's the impression of the OCaml project I have from what I have seen so far. Adrian
Le mercredi 08 octobre 2025 à 11:07 +0200, John Paul Adrian Glaubitz a écrit : I see the discussion is still ongoing, and I notice that my point about spreading thin has been made by upstream. I don't think they completely closed the door to the contribution, it's just that this new arch isn't on their radar yet... Cheers, J.Puydt
»The lack of support for Rocq on bytecode-only architectures looks to me like a potential issue with the packaging of Rocq, rather than a fundamental issue with the OCaml compiler. As far as I know, it is perfectly possible to use Rocq in bytecode mode (of course it is slower than in native mode, but usable), and there is support in the Rocq configure script for this scenario.« Source: https://github.com/ocaml/ocaml/pull/11974#issuecomment-3381299696 Can we give it a try? I mean, we still have a lot of time for testing until forky gets frozen. We can still revert it if it doesn't work. Adrian
Hi, Le jeudi 09 octobre 2025 à 20:47 +0200, John Paul Adrian Glaubitz a écrit : The set of coq packages in Debian isn't ready for an upload right now, but we'll see how things turn : https://salsa.debian.org/ocaml-team/coq/-/commit/d76e2b1240b77becd23b9d3bf93988a3cf516fbc Cheers, J.Puydt
Great, thank you! Much appreciated. Adrian