pkgs/development/coq-modules/graph-theory/default.nix

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