Proposal to move project matrix-canonical-forms to coq-community

[ybertot]

Project name: matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s): Guillaume Cano

Current URL: https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano) https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description: This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot

[palmskog]

We seem to have converged to a standard for repository names that use lower case with - as a delimiter, so in my mind matrix-canonical-forms is a good name.

To give some context for why I think this project fits well in coq-community:

• There was a request to use this work as a dependency on the ssreflect mailing list.
• We are in the process of moving CoqEAL to coq-community (#127), so it should be easier to co-evolve the two projects here.

It should ultimately be decided on by CoqEAL maintainers, but to me it may even make sense to eventually move this work into the CoqEAL repo (packaged separately), for maintenance reasons.

[ybertot]

Incidentally, I just had a conversation with Guillaume Cano, the initial author, who also approves of this move.

[ybertot]

I had hesitations about this name because the main objective of Guillaume Cano's work goes well beyond normal forms of matrices. So do we choose the name that would encompass the whole of Guillaume's work or do we stick with this single piece, possible with the need to re-organize libraries when the other part of the work is ported (which may be delayed to an unknown date).

[palmskog]

Repository names can always be changed after a transfer, but if you can think of some more general name than one which has to do with mactrices, and change the repostiory name before the transfer, that's probably a good thing.

[palmskog]

Unless others (e.g., @Zimmi48) have some concern, I think we can let @ybertot transfer the repository to the coq-community organization when he feels it is ready. Recall that both repository transfer and renaming is done under "Settings"; renaming at the top and then "Danger Zone" for transfers at the bottom.

[Zimmi48]

Sounds good to me.

[palmskog]

The repo has been transferred, so I'm closing this issue. Further discussion can take place at a later time as issues in the repo itself: https://github.com/coq-community/matrix_canonical_forms

Thanks everyone!