coqPackages.graph-theory: init at 0.9
This commit is contained in:
parent
bcaa89c691
commit
2f3c29cc68
33
pkgs/development/coq-modules/graph-theory/default.nix
Normal file
33
pkgs/development/coq-modules/graph-theory/default.nix
Normal file
|
@ -0,0 +1,33 @@
|
||||||
|
{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap
|
||||||
|
, hierarchy-builder, version ? null }:
|
||||||
|
|
||||||
|
with lib;
|
||||||
|
|
||||||
|
mkCoqDerivation {
|
||||||
|
pname = "graph-theory";
|
||||||
|
|
||||||
|
release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
|
||||||
|
|
||||||
|
releaseRev = v: "v${v}";
|
||||||
|
|
||||||
|
inherit version;
|
||||||
|
defaultVersion = with versions; switch coq.coq-version [
|
||||||
|
{ case = isGe "8.13"; out = "0.9"; }
|
||||||
|
] null;
|
||||||
|
|
||||||
|
propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ];
|
||||||
|
|
||||||
|
meta = {
|
||||||
|
description = "Library of formalized graph theory results in Coq";
|
||||||
|
longDescription = ''
|
||||||
|
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).
|
||||||
|
'';
|
||||||
|
maintainers = with maintainers; [ siraben ];
|
||||||
|
license = licenses.cecill-b;
|
||||||
|
};
|
||||||
|
}
|
|
@ -42,6 +42,7 @@ let
|
||||||
fourcolor = callPackage ../development/coq-modules/fourcolor {};
|
fourcolor = callPackage ../development/coq-modules/fourcolor {};
|
||||||
gappalib = callPackage ../development/coq-modules/gappalib {};
|
gappalib = callPackage ../development/coq-modules/gappalib {};
|
||||||
goedel = callPackage ../development/coq-modules/goedel {};
|
goedel = callPackage ../development/coq-modules/goedel {};
|
||||||
|
graph-theory = callPackage ../development/coq-modules/graph-theory {};
|
||||||
heq = callPackage ../development/coq-modules/heq {};
|
heq = callPackage ../development/coq-modules/heq {};
|
||||||
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
|
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
|
||||||
HoTT = callPackage ../development/coq-modules/HoTT {};
|
HoTT = callPackage ../development/coq-modules/HoTT {};
|
||||||
|
|
Loading…
Reference in a new issue