Add overlays

Author: proux01

.nix/coq-overlays/graph-theory/default.nix

@@ -0,0 +1,70 @@
+{
+  lib,
+  mkCoqDerivation,
+  coq,
+  mathcomp,
+  mathcomp-finmap,
+  fourcolor,
+  stdlib,
+  version ? null,
+}:
+
+mkCoqDerivation {
+  pname = "graph-theory";
+
+  release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI=";
+  release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU=";
+  release."0.9.2".sha256 = "sha256-DPYCZS8CzkfgpR+lmYhV2v20ezMtyWp8hdWpuh0OOQU=";
+  release."0.9.3".sha256 = "sha256-9WX3gsw+4btJLqcGg2W+7Qy+jaZtkfw7vCp8sXYmaWw=";
+  release."0.9.4".sha256 = "sha256-fXTAsRdPisNhg8Umaa7S7gZ1M8zuPGg426KP9fAkmXQ=";
+  release."0.9.6".sha256 = "sha256-fvGb970tRE4xj1pBIhNBDaqssDd6kNQ/+s0c+aOO5IE=";
+
+  releaseRev = v: "v${v}";
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mc: out: {
+        cases = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.18" "9.0") (range "2.0.0" "2.4.0") "0.9.6")
+        (case (range "8.16" "8.19") (range "2.0.0" "2.3.0") "0.9.4")
+        (case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "0.9.3")
+        (case (range "8.14" "8.18") (range "1.13.0" "1.18.0") "0.9.2")
+        (case (range "8.14" "8.16") (range "1.13.0" "1.14.0") "0.9.1")
+        (case (range "8.12" "8.13") (range "1.12.0" "1.14.0") "0.9")
+      ]
+      null;
+
+  propagatedBuildInputs = [
+    mathcomp.ssreflect
+    mathcomp.fingroup
+    mathcomp.algebra
+    mathcomp-finmap
+    fourcolor
+    stdlib
+  ];
+
+  meta = with lib; {
+    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;
+  };
+}

.nix/coq-overlays/mathcomp-infotheo/default.nix

@@ -0,0 +1,70 @@
+{
+  coq,
+  mkCoqDerivation,
+  mathcomp-analysis,
+  mathcomp-analysis-stdlib,
+  interval,
+  lib,
+  version ? null,
+}:
+
+(mkCoqDerivation {
+  namePrefix = [
+    "coq"
+    "mathcomp"
+  ];
+  pname = "infotheo";
+  owner = "affeldt-aist";
+  inherit version;
+
+  defaultVersion =
+    let
+      case = coq: mc: out: {
+        cases = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-analysis.version ]
+      [
+        (case (range "8.20" "9.1") (isGe "1.12") "0.9.4")
+        (case (range "8.19" "8.20") (range "1.10" "1.11") "0.9.3")
+        (case (range "8.19" "8.20") (isGe "1.9") "0.9.1")
+        (case (range "8.19" "8.20") (isGe "1.7") "0.7.7")
+        (case (range "8.19" "8.20") (isGe "1.7") "0.7.5")
+        (case (range "8.18" "8.20") (isGe "1.5") "0.7.3")
+        (case (range "8.18" "8.19") (isGe "1.2") "0.7.2")
+        (case (range "8.17" "8.19") (isGe "1.0") "0.7.1")
+        (case (isGe "8.17") (range "0.6.6" "0.7.0") "0.6.1")
+        (case (range "8.17" "8.18") (range "0.6.0" "0.6.7") "0.5.2")
+        (case (range "8.15" "8.16") (range "0.5.4" "0.6.5") "0.5.1")
+      ]
+      null;
+  release."0.9.4".sha256 = "sha256-btHOBNMdXvlG2jxC04+4qmIjeyuaqtyugm2Ruj3lQr8=";
+  release."0.9.3".sha256 = "sha256-8+cnVKNAvZ3MVV3BpS8UmCIxJphsQRBv3swek1eEBjE=";
+  release."0.9.1".sha256 = "sha256-WI20HxMHr1ZUwOGPIUl+nRI8TxVUa2+F1xcGjRDHO9g=";
+  release."0.7.7".sha256 = "sha256-kEbpMl7U+I2kvqi1VrjhIVFkZFO6h0tTHEUZRbHYG7E=";
+  release."0.7.5".sha256 = "sha256-pzPo+Acjx3vlyqOkSZQ8uT2BDLSTfbAnRm39e+/CqE0=";
+  release."0.7.3".sha256 = "sha256-7+qPtE1KfDmo9ZsQtWMzoR2MYnFpTjFHK/yZYVm+GxA=";
+  release."0.7.2".sha256 = "sha256-dekrdVmuTcqXXmKhIb831EKtMhbPrXHJZhzmGb9rdRo=";
+  release."0.7.1".sha256 = "sha256-/4Elb35SmscG6EjEcHYDo+AmWrpBUlygZL0WhaD+fcY=";
+  release."0.6.1".sha256 = "sha256-tFB5lrwRPIlHkP+ebgcJwu03Cc9yVaOINOAo8Bf2LT4=";
+  release."0.5.1".sha256 = "sha256-yBBl5l+V+dggsg5KM59Yo9CULKog/xxE8vrW+ZRnX7Y=";
+  release."0.5.2".sha256 = "sha256-8WAnAV53c0pMTdwj8XcUDUkLZbpUgIQbEOgOb63uHQA=";
+
+  propagatedBuildInputs = [ mathcomp-analysis-stdlib ];
+
+  meta = with lib; {
+    description = "Coq formalization of information theory and linear error-correcting codes";
+    license = licenses.lgpl21Plus;
+  };
+}).overrideAttrs
+  (o: {
+    propagatedBuildInputs =
+      o.propagatedBuildInputs
+      ++ lib.optional (lib.versions.isGe "0.7.2" o.version || o.version == "dev") interval;
+  })