Graph Theory is a library for graph theory based on the Mathematical Components library, including various standard results from the literature (e.g., Menger's Theorem, Hall's Marriage Theorem, the excluded minor characterization of treewidth-two graphs). The project is hosted in Coq-community, maintained by @chdoc and @damien-pous with occasional help from other organization members such as myself. The project has two packages:
coq-graph-theory, the core reusable library of graph definitions and results
coq-graph-theory-planar, graph planarity results depending on coq-fourcolor, i.e., Gonthier's proof of the Four Color Theorem
I propose that coq-graph-theory is included in the Coq Platform. The motivation is that graphs are a widely used formalism with many applications. And while the basic Mathematical Components library includes a form of finite graphs, coq-graph-theory goes much further with directed graphs, simple graphs, multigraphs, etc.
Note that all dependencies of coq-graph-theory (dune, coq-mathcomp-ssreflect, coq-mathcomp-algebra, coq-mathcomp-finmap, coq-hierarchy-builder) are already in the Platform.
@MSoegtropIMC I got a mandate from the main maintainer of graph-theory to do releases for the Platform here. Hopefully this will cover the "maintainer agreement" part of adding a new package.
Graph Theory is a library for graph theory based on the Mathematical Components library, including various standard results from the literature (e.g., Menger's Theorem, Hall's Marriage Theorem, the excluded minor characterization of treewidth-two graphs). The project is hosted in Coq-community, maintained by @chdoc and @damien-pous with occasional help from other organization members such as myself. The project has two packages:
coq-graph-theory
, the core reusable library of graph definitions and resultscoq-graph-theory-planar
, graph planarity results depending oncoq-fourcolor
, i.e., Gonthier's proof of the Four Color TheoremI propose that
coq-graph-theory
is included in the Coq Platform. The motivation is that graphs are a widely used formalism with many applications. And while the basic Mathematical Components library includes a form of finite graphs,coq-graph-theory
goes much further with directed graphs, simple graphs, multigraphs, etc.Note that all dependencies of
coq-graph-theory
(dune
,coq-mathcomp-ssreflect
,coq-mathcomp-algebra
,coq-mathcomp-finmap
,coq-hierarchy-builder
) are already in the Platform.