Hi, Le mercredi 08 octobre 2025 à 10:11 +0200, John Paul Adrian Glaubitz a écrit : > On Wed, 2025-10-08 at 10:00 +0200, Stéphane Glondu wrote: > > Le 08/10/2025 à 09:49, John Paul Adrian Glaubitz a écrit : > > > > > 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? > > > > > > > > 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. > > > > > > I verified that it builds fine on multiple targets without native > > > compiler > > > support. > > > > > > > Did something change? > > > > > > Looks like as the failures are gone. > > > > Did you try reverse dependencies as well? > > 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. >
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
