I had a quick look at how things have progressed since last time I had a look, and some things got fixed, so the current situation is:

```
Level 1
coq... ok
Level 2
elpi... ok
aac-tactics... ok
coq-bignums... ok
coq-dpdgraph... ok
coq-elpi... ok
coq-ext-lib... ok
coq-hammer... ok
coq-hott... ok
coq-libhyps... ok
coq-menhirlib... ok
coq-record-update... ok
coq-reduction-effects... ok
coq-stdpp... ok
coq-unicoq... ok
coq-unimath... ok
flocq... ok
ott... ok
paramcoq... ok
Level 3
coq-equations... ok
coq-gappa... ok
coq-hierarchy-builder... ok
coq-iris... ok
coq-math-classes... ok
coq-mtac2... error!
coq-simple-io... ok
coqprime... ok
Level 4
ssreflect... ok
coq-corn... error!
Level 5
coq-deriving... ok
coq-reglang... ok
coq-relation-algebra... ok
coquelicot... ok
mathcomp-bigenough... ok
mathcomp-finmap... ok
mathcomp-zify... ok
coq-quickchick... ok
Level 6
coq-extructures... ok
coq-interval... ok
mathcomp-algebra-tactics... ok
mathcomp-analysis... error!
mathcomp-multinomials... ok
mathcomp-real-closed... ok
Level 7
coqeal... ok
mathcomp-abel... error!
```

(Notice that those are local tests: the main Debian archive is still using Coq 8.17)

Out of curiosity, which versions?

All latest upstreams as far as I know:

```
aac-tactics_8.18.0-1.dsc coq-equations_1.3-8.18-1.dsc coq-math-classes_8.18.0-1.dsc coq-relation-algebra_1.7.9-2.dsc mathcomp-abel_1.2.1-3.dsc ott_0.33+ds-2.dsc
coq_8.18.0+dfsg-1.dsc coq-extructures_0.4.0-1.dsc coq-menhirlib_20230608+ds-2.dsc coq-simple-io_1.8.0-4.dsc mathcomp-algebra-tactics_1.2.1-1.dsc paramcoq_1.1.3+coq8.18-1.dsc
coq-bignums_9.0.0+coq8.18-1.dsc coq-gappa_1.5.4-1.dsc coq-mtac2_1.4+8.17-2.dsc coq-stdpp_1.8.0-6.dsc mathcomp-analysis_0.6.5-1.dsc ssreflect_2.0.0-1.dsc
coq-corn_8.16.0-4.dsc coq-hammer_1.3.2+8.17-2.dsc coqprime_8.17-2.dsc coquelicot_3.4.0-1.dsc mathcomp-finmap_2.0.0-1.dsc
coq-deriving_0.2.0-1.dsc coq-hierarchy-builder_1.6.0-1.dsc coq-quickchick_2.0.1-1.dsc coq-unicoq_1.6-8.18-1.dsc mathcomp-multinomials_2.0.0-1.dsc
coq-dpdgraph_1.0+8.17-2.dsc coq-interval_4.8.1-1.dsc coq-record-update_0.3.2-2.dsc coq-unimath_20230420-5.dsc mathcomp-real-closed_2.0.0-1.dsc
coqeal_2.0.0-1.dsc coq-iris_4.0.0-5.dsc coq-reduction-effects_0.1.5-1.dsc elpi_1.17.3-1.dsc mathcomp-zify_1.5.0+2.0+8.16-1.dsc
coq-elpi_1.19.0-1.dsc coq-libhyps_2.0.6-4.dsc coq-reglang_1.2.0-1.dsc flocq_4.1.3-1.dsc mistune_3.0.1-1.dsc
```

Abel is just waiting for a merge here and a tag: https://github.com/math-comp/Abel/pull/75

and for the record, CoqPrime has a new version out: https://github.com/coq/opam/blob/master/released/packages/coq-coqprime/coq-coqprime.1.4.0/opam

@Karl Palmskog Ah, a new version of coqprime is out? It's ready to get in, then. As are the new coq-stdpp and coq-iris - thanks for the heads up!

There are also new versions of a few others... I'll work through them too, even if that won't fix the broken ones

Final status for today:

- coq-mtac2 and coq-corn are broken by Coq 8.18
- mathcomp-analysis and mathcomp-abel by MC 2

The versions I have ready for upload to the Debian archive when the above issues are fixed are:

```
aac-tactics_8.18.0-1.dsc coq-elpi_1.19.0-1.dsc coq-iris_4.1.0-1.dsc coq-record-update_0.3.3-1.dsc coq-unicoq_1.6-8.18-1.dsc mathcomp-multinomials_2.0.0-1.dsc
coq_8.18.0+dfsg-1.dsc coq-equations_1.3-8.18-1.dsc coq-libhyps_2.0.6-4.dsc coq-reduction-effects_0.1.5-1.dsc coq-unimath_20231010-1.dsc mathcomp-real-closed_2.0.0-1.dsc
coq-bignums_9.0.0+coq8.18-1.dsc coq-extructures_0.4.0-1.dsc coq-math-classes_8.18.0-1.dsc coq-reglang_1.2.0-1.dsc flocq_4.1.3-1.dsc mathcomp-zify_1.5.0+2.0+8.16-1.dsc
coq-corn_8.16.0-4.dsc coq-gappa_1.5.4-1.dsc coq-menhirlib_20230608+ds-2.dsc coq-relation-algebra_1.7.9-2.dsc mathcomp-abel_1.2.1-3.dsc ott_0.33+ds-2.dsc
coq-deriving_0.2.0-1.dsc coq-hammer_1.3.2+8.17-2.dsc coq-mtac2_1.4+8.17-2.dsc coq-simple-io_1.8.0-4.dsc mathcomp-algebra-tactics_1.2.1-1.dsc paramcoq_1.1.3+coq8.18-1.dsc
coq-dpdgraph_1.0+8.17-2.dsc coq-hierarchy-builder_1.6.0-1.dsc coqprime_8.18-1.dsc coq-stdpp_1.9.0-1.dsc mathcomp-analysis_0.6.5-1.dsc ssreflect_2.0.0-1.dsc
coqeal_2.0.0-1.dsc coq-interval_4.8.1-1.dsc coq-quickchick_2.0.1-1.dsc coquelicot_3.4.0-1.dsc mathcomp-finmap_2.0.0-1.dsc
```

For Analysis, the port may not be merged before January so I'm not sure you want to wait for it.

But MC 1 still works on 8.18 so that'd be an option?

Yes, I can probably just push Coq 8.18 ; perhaps I'll do that if mtac2 and corn get compatible with it. For now, since I don't have a clear path, I'll just stay put.

@Julien Puydt is there a permanent page/URL for Coq-related Debian packages that gets updated with latest packaged version? I ask because this could be a good idea to list in Awesome Coq among other package collections

@Karl Palmskog I update this page regularly, but it's not automatic...

OK, "regularly" is good enough for me

Last updated: Oct 13 2024 at 01:02 UTC