tjh.dev
1{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
2, fourcolor, hierarchy-builder, version ? null }:
3
4mkCoqDerivation {
5 pname = "graph-theory";
6
7 release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
8 release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU=";
9
10 releaseRev = v: "v${v}";
11
12 inherit version;
13 defaultVersion = with lib.versions; lib.switch coq.coq-version [
14 { case = range "8.14" "8.16"; out = "0.9.1"; }
15 { case = range "8.12" "8.12"; out = "0.9"; }
16 ] null;
17
18 propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup fourcolor hierarchy-builder ];
19
20 meta = with lib; {
21 description = "Library of formalized graph theory results in Coq";
22 longDescription = ''
23 A library of formalized graph theory results, including various
24 standard results from the literature (e.g., Menger’s Theorem, Hall’s
25 Marriage Theorem, and the excluded minor characterization of
26 treewidth-two graphs) as well as some more recent results arising from
27 the study of relation algebra within the ERC CoVeCe project (e.g.,
28 soundness and completeness of an axiomatization of graph isomorphism).
29 '';
30 maintainers = with maintainers; [ siraben ];
31 license = licenses.cecill-b;
32 };
33}