tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp,
6 mathcomp-finmap,
7 mathcomp-algebra-tactics,
8 fourcolor,
9 stdlib,
10 version ? null,
11}:
12
13mkCoqDerivation {
14 pname = "graph-theory";
15
16 release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
17 release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU=";
18 release."0.9.2".sha256 = "sha256-DPYCZS8CzkfgpR+lmYhV2v20ezMtyWp8hdWpuh0OOQU=";
19 release."0.9.3".sha256 = "sha256-9WX3gsw+4btJLqcGg2W+7Qy+jaZtkfw7vCp8sXYmaWw=";
20 release."0.9.4".sha256 = "sha256-fXTAsRdPisNhg8Umaa7S7gZ1M8zuPGg426KP9fAkmXQ=";
21 release."0.9.6".sha256 = "sha256-fvGb970tRE4xj1pBIhNBDaqssDd6kNQ/+s0c+aOO5IE=";
22 release."0.9.7".sha256 = "sha256-rAZn326EdmS8fjGjk785BSJBFSpol6suwD3zO/tCBgk=";
23
24 releaseRev = v: "v${v}";
25
26 inherit version;
27 defaultVersion =
28 let
29 case = coq: mc: out: {
30 cases = [
31 coq
32 mc
33 ];
34 inherit out;
35 };
36 in
37 with lib.versions;
38 lib.switch
39 [ coq.coq-version mathcomp.version ]
40 [
41 (case (range "8.18" "9.1") (range "2.1.0" "2.5.0") "0.9.7")
42 (case (range "8.18" "9.0") (range "2.0.0" "2.4.0") "0.9.6")
43 (case (range "8.16" "8.19") (range "2.0.0" "2.3.0") "0.9.4")
44 (case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "0.9.3")
45 (case (range "8.14" "8.18") (range "1.13.0" "1.18.0") "0.9.2")
46 (case (range "8.14" "8.16") (range "1.13.0" "1.14.0") "0.9.1")
47 (case (range "8.12" "8.13") (range "1.12.0" "1.14.0") "0.9")
48 ]
49 null;
50
51 propagatedBuildInputs = [
52 mathcomp.algebra
53 mathcomp-finmap
54 mathcomp.fingroup
55 mathcomp-algebra-tactics
56 fourcolor
57 stdlib
58 ];
59
60 meta = {
61 description = "Library of formalized graph theory results in Coq";
62 longDescription = ''
63 A library of formalized graph theory results, including various
64 standard results from the literature (e.g., Menger’s Theorem, Hall’s
65 Marriage Theorem, and the excluded minor characterization of
66 treewidth-two graphs) as well as some more recent results arising from
67 the study of relation algebra within the ERC CoVeCe project (e.g.,
68 soundness and completeness of an axiomatization of graph isomorphism).
69 '';
70 maintainers = with lib.maintainers; [ siraben ];
71 license = lib.licenses.cecill-b;
72 };
73}