Hi, I'm working on updating Coq (with an upcoming renaming to Rocq) in Debian ; here is where things stand on my box -- I'll upload as soon as I have a working set. Notice that rocq-stdlib is new, so will have to get through the NEW queue.
* Update Coq/Rocq in Debian [6/8] - [X] step 1 [2/2] - [X] elpi 3.1.0-1 - [X] coq 9.0.0-1 - [X] step 2 [1/1] - [X] rocq-stdlib 9.0.0-1 - [X] step 3 [17/17] - [X] aac-tactics 8.20.0-2 - [X] coq-bignums 9.0.0+rocq9.0-1 - [X] coq-dpdgraph 1.0+9.0-1 - [X] coq-elpi 3.1.0-1 - [X] coq-ext-lib 0.13.0-2 - [X] coq-hammer 1.3.2+8.20-2 - [X] coq-hott 9.0-2 - [X] coq-libhyps 2.0.8-5 - [X] coq-menhirlib 20240715+ds-2 - [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 - [X] coq-unimath 20240923-3 - [X] flocq 4.2.1-2 - [X] ott 0.34+ds-2 - [X] paramcoq 1.1.3+coq9.0-1 - [-] step 4 [7/8] - [X] coq-equations 1.3.1-9.0-1 - [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 FAIL [[https://github.com/Mtac2/Mtac2/issues/410][not compatible with Rocq]] - [X] coq-simple-io 1.11.0-2 - [X] coqprime 8.20.1-2 - [X] step 5 [2/2] - [X] ssreflect 2.4.0-1 - [X] coq-corn 8.20.0-2 - [-] step 6 [7/8] - [X] coq-deriving 0.2.2-1 - [X] coq-reglang 1.2.2-1 - [ ] coq-relation-algebra 1.7.11-2 FAIL [[https://github.com/damien-pous/relation-algebra/issues/50][not compatible with Rocq]] - [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.6-1 - [X] mathcomp-analysis 1.13.0-1 - [X] mathcomp-multinomials 2.4.0-1 - [X] mathcomp-real-closed 2.0.3-1 - [X] step 8 [1/1] - [X] coqeal 2.1.0-2 Cheers, J.Puydt
