Proposal to move project GraphTheory to coq-community

[chdoc]

Project name: Graph Theory

Initial author(s): Christian Doczkal (@chdoc) and Damien Pous (@dpous)

Current URL: https://perso.ens-lyon.fr/damien.pous/covece/graphs/

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B (tbd)

Description: A library of formalized graph theory results, including various standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, and the excluded minor characterization of treewidth-two graphs) as well as some more recent results arising from the study of relation algebra within the ERC CoVeCe project (e.g., soundness and completeness of an axiomatization of graph isomorphism).

Status: under active development, contributions welcome

New maintainer: Christian Doczkal (@chdoc) and Damien Pous (@dpous)

This is a project that has been developed internally (mainly) by myself and Damien Pous over the last couple of years. We would like to move from our previous closed development model to a model that facilitates external contributions.

[palmskog]

This is a project that is very welcome to coq-community.

Do you already have a GitHub repo? I don't remember if non-owners can create repos directly in the organization, but if not, I can create an empty one and make you and Damien admins @chdoc.

We do encourage including repo history when this is available (e.g., for use in future research), but the choice is up to the repo owners.

Just to be clear, there seems to be two accounts for Damien: @damien-pous and @dpous - can you confirm that it's the latter I'm supposed to invite? For example, the relation-algebra project is tied to the former.

[chdoc]

Lets wait for Damien to comment, now that both accounts have been mentioned.

We have an internal git repository whose master-branch we would push here. The consensus was to do this with history (so that we can keep compatibility to the internal repository we may or may not continue to use occasionally).

Is graph-theory as repository name and GraphTheory as prefix acceptable? In OPAM coq-graphs is already taken, so we could go for coq-graph-theory. In any case, there should possibly be some further stabilization done before we do an OPAM release.

I think moving a repository requires the right to create repositories on the target side, so I may actually be able to do this by myself. This would feel a bit strange, because this would allow anyone to (accidentally) flatten/shadow forwards.

[palmskog]

Is graph-theory as repository name and GraphTheory as prefix acceptable?

Sounds good to me, and by our current conventions this would indeed imply a package name of coq-graph-theory.

I think moving a repository requires the right to create repositories on the target side, so I may actually be able to do this by myself.

Ah, right, good point. Then feel free to do this whenever ready, I will simply add the admin privileges when the repo shows up.

[dpous]

Hi, Please use the damien-pous account, indeed. Best, Damien Le ven. 28 févr. 2020 à 19:53, Karl Palmskog <[email protected]> a écrit :

…

Is graph-theory as repository name and GraphTheory as prefix acceptable? Sounds good to me, and by our current conventions this would indeed imply a package name of coq-graph-theory. I think moving a repository requires the right to create repositories on the target side, so I may actually be able to do this by myself. Ah, right, good point. Then feel free to do this whenever ready, I will simply add the admin privileges when the repo shows up. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#98?email_source=notifications&email_token=AAKVKV6MS5C3XAA6SODTGLDRFFMRRA5CNFSM4K5WJ7XKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOENJXTQI#issuecomment-592673217>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKVKVY5ZZZSD2ALJBWQYSTRFFMRRANCNFSM4K5WJ7XA> .

[palmskog]

Thanks, I have invited the damien-pous account to join coq-community.

[Zimmi48]

Out of curiosity, is the relationship to graph-basics and graphs known or documented somewhere? Can we deprecate these libraries in favor of your graph theory library?

Note that if you didn't do the comparison, I'm not asking you to do it. I'm only asking this because there are still 146 non-archived contribs, 135 of which were still maintained by @herbelin in the last year, and it would be great if we could identify those which have been made obsolete by newer and more complete replacements, so that they can be archived and stop being maintained.

[chdoc]

graph-basics is an almost 20-year old development by Duprat which contains a few basic definitions but, as far as I can tell, no interesting theorems. IIRC, this is the result of some student project and I am not aware of any uses of this contrib. In my own experience, if you don't do anything with your representation while developing it, then the representation will not be very usable.

graphs is, as far as I can tell, a reflective decision procedure for inequalities using an algorithm based on cycle-detection in graphs. (Synopsis of the opam package: "Satisfiability of inequality constraints and detection of cycles with negative weight in graphs"). As far as I can tell, they use graphs to compute and prove very little about them, while we prove properties of classes of graphs and do virtually no computations. Hence, I think that graphs is mostly a suboptimal choice of names here.

[Zimmi48]

Thanks for your answer! Maybe it would make sense to archive graph-basics and to rename graphs to some less confusing name then. WDYT @herbelin?

[herbelin]

I know basically nothing about graphs...

Would there be a comment that I could add to graph-basics to characterize the representation of graphs it chooses among the different possible representations of graphs?

Regarding graphs, again, I'm missing hindsight. Would graphs-bellman, or graphs-cycle-detection be relevant alternative names?

Or would it make sense to integrate it to GraphTheory?

Or, would it make sense to build a new level of structuration of libraries, say GraphLibraries which has several subcomponents, two of them being GraphTheory and GraphBellman (or whatever name is chosen for the latter).

[Zimmi48]

build a new level of structuration of libraries

I'm not in favor of having common namespaces that are shared across distinct and independent projects.

[chdoc]

I agree with @Zimmi48, that these projects are all distinct and independent. On the other hand, there is only one namespace for Coq libraries and one namespace of OPAM packages. In that regard, something as broad as graphs is generally a really poor choice of name, if you ask me. I'm fine with this package being called GraphTheory, because we are doing precisely that:: we have a few results from connectivity theory, something on minors and treewidth, algebras of graphs, etc. So its a diverse collection of graph theory results, and one reason to put this into Coq community is to allow for external contributions.

On the other hand, there is a lot of other work out there verifying some graph algorithm for some purpose. We may go into that direction in the future, but that isn't a priority for now.

[palmskog]

I would like to see both graphs and graph-basics renamed to something more specific, and basically leave everything else as is (no need to deprecate them, etc.). The global Coq namespace would also be a bit less polluted without Graphs or GraphBasics occupied by legacy projects.

Moreover, I would personally like to see a project with a collection of graph algorithms in various representations that is tied in to (but separate from) the GraphTheory package. In particular, there is quite a lot work on extraction-friendly algorithm representations.

[herbelin]

Personally, I like the idea of organizing the Coq libraries like a library of books is organized, e.g. following classifications such as ACM or MathSciNet. And this seems to be needed to some extent if one expects several libraries / packages to be simultaneously installable under the same user-contrib directory.

Is it a view that you also have in mind, @chdoc, @palmskog, @Zimmi48?

In any case, the name of graphs and graph-basics can certainly be changed. Should we then seize this opportunity to also rename (or museumify, or at least reposition in the context of today) other "contribs" which occupy a too general names? There is for instance a coq-contrib Algebra, a toy coq-contrib Groups, a small GroupTheory, or even, in the other direction, a not so explicitly named ConCat about category theory.

[palmskog]

As the number of Coq projects grows, I also believe it will become a priority to have some general enforced scheme for naming directories in user-contrib (and top-level path names inside Coq) - at least for the packages in the Coq OPAM package index. To this end, I opened coq/opam#1208 for further discussion.

It's not at all obvious to me how one would incorporate other classifications into the naming scheme. For example, one project may have multiple classifications.

However, regardless of the high-level discussion, I believe coq-contrib names are definitely low-hanging fruit to fix naming for. For example, we could follow MathComp and do Contrib.Algebra, Contrib.ConCat, etc. If an unmaintained coq-contrib gets maintained, the new maintainer can choose a good new namespace.

[chdoc]

I created the repository and pushed our master branch. I tried setting up CI (branch ci-setup), and everything seems to work except that I don't know how to add the finmap dependendy to the NIX job, so that job is still failing. @palmskog , can you have a look?

[Zimmi48]

@chdoc the finmap package is called coqPackages.mathcomp-finmap.

There is something weird in this part of the meta file:

[Zimmi48]

Sorry, truncated comment:

https://github.com/coq-community/graph-theory/blob/670748996c5526120408272f69588ed81af7739c/meta.yml#L65-L73

It seems that you would like to list two dependencies, but you are in fact listing a single one (one -). name and version are provided twice but the second one overrides the first. It still works because ssreflect is in fact a dependency of finmap.

[Zimmi48]

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{(>= "1.9" & < "1.11~") | (= "dev")}'
    name: coq-mathcomp-finmap
    version: '{>= "1.4.0"}'
  nix: ssreflect
  description: |-
    [MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)

should rather be:

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{(>= "1.9" & < "1.11~") | (= "dev")}'
  nix: mathcomp-ssreflect_1_9
  description: MathComp's SSReflect library, version 1.9 or later
- opam:
    name: coq-mathcomp-finmap
    version: '{>= "1.4.0"}'
  nix: mathcomp-finmap
  description: MathComp's finmap library

Although from what I can see on https://nixos.org/nixos/packages.html?channel=nixpkgs-unstable&query=coqPackages.mathcomp-finmap, the packaged version of finmap seems to be 1.2.1. @CohenCyril can provide further help with math-comp packages in nixpkgs.

Note that if you want, you can skip the Nix CI entirely (just remove https://github.com/coq-community/graph-theory/blob/670748996c5526120408272f69588ed81af7739c/meta.yml#L57-L59).

[chdoc]

I will give it one more try with what you suggested.

[Zimmi48]

(PS: don't forget to generate and commit the default.nix file)

[chdoc]

Thanks, that came right at the moment when I was wondering why the change in nix dependency information wasn't causing any finmap related changes in the .travis.yml.

[chdoc]

Thanks everyone!