Adding more extras

[CohenCyril]

This is my wishlist for mathcomp extra packages (untested)

[corwin-of-amber]

Oh cool! Of course for actually having them they need to be added to the Makefile as well, and we need to see that they compile. I assume at least they all have 8.14-compatible versions by now?

[CohenCyril]

I assume at least they all have 8.14-compatible versions by now?

I also assume so. (I manually checked by I cannot tell for sure since I do not use opam)

[corwin-of-amber]

Do you know if they have Dune build files? This would make integration very easy.

[ejgallego]

Do you know if they have Dune build files? This would make integration very easy.

I can write the dune files, where's the repos?

[CohenCyril]

repo + version

• https://github.com/math-comp/real-closed 1.1.2
• https://github.com/math-comp/mczify 1.1.0+1.12+8.13
• https://github.com/math-comp/algebra-tactics 0.1.0
• https://github.com/math-comp/analysis 0.3.11

[CohenCyril]

none of them have dune build files

[ejgallego]

none of them have dune build files

Ok thanks, I'll add them as PRs

[CohenCyril]

(BTW all of these should work perfectly with any combination of Coq 8.13 or Coq 8.14 and mathcomp 1.12 and 1.13)

[CohenCyril]

Note that for mathcomp analysis you will need hierarchy-builder as well

https://github.com/math-comp/hierarchy-builder 1.2.0

[ejgallego]

Note that for mathcomp analysis you will need hierarchy-builder as well

Ups, that may go beyond the amount of time I have for it :( :(

All these plugins are, IMHO, an engineering nightmare.

[CohenCyril]

Then take out mathcomp analysis for now.

[corwin-of-amber]

Oh oops looks like we totally forgot about this little thing. Do you want to rebase for 8.16? sry... 😞

[corwin-of-amber]

actually I see now this is just a list. We need to revisit these packages; if they are a part of coq-universe this should be easy enough.