On updating Coq/Rocq in Debian
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
Reply to: