You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
@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.The text was updated successfully, but these errors were encountered: