coqPackages: refactor mathcomp packages

Closes #61456

6 files changed, 273 insertions, 186 deletions

diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
deleted file mode 100644
index 8c315371229..00000000000
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ /dev/null
@@ -1,30 +0,0 @@
-{ stdenv, fetchFromGitHub, coq, mathcomp-bigenough, mathcomp-finmap }:
-
-stdenv.mkDerivation rec {
-  version = "0.2.0";
-  name = "coq${coq.coq-version}-mathcomp-analysis-${version}";
-
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "analysis";
-    rev = version;
-    sha256 = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
-  };
-
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp-bigenough mathcomp-finmap ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = {
-    description = "Analysis library compatible with Mathematical Components";
-    inherit (src.meta) homepage;
-    inherit (coq.meta) platforms;
-    license = stdenv.lib.licenses.cecill-c;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" ];
-  };
-}
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
deleted file mode 100644
index e1f58edc9cb..00000000000
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ /dev/null
@@ -1,29 +0,0 @@
-{ stdenv, fetchFromGitHub, coq, mathcomp }:
-
-stdenv.mkDerivation rec {
-  version = "1.0.0";
-  name = "coq${coq.coq-version}-mathcomp-bigenough-${version}";
-
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "bigenough";
-    rev = version;
-    sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
-  };
-
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp ];
-
-  installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = {
-    description = "A small library to do epsilon - N reasonning";
-    inherit (src.meta) homepage;
-    inherit (mathcomp.meta) platforms license;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
-  };
-}
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
deleted file mode 100644
index c36b72711ff..00000000000
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ /dev/null
@@ -1,40 +0,0 @@
-{ stdenv, fetchFromGitHub, coq, mathcomp }:
-
-let param =
-  if stdenv.lib.versionAtLeast mathcomp.version "1.8.0"
-  then {
-    version = "1.2.0";
-    sha256 = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
-  } else {
-    version = "1.1.0";
-    sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
-  }
-; in
-
-stdenv.mkDerivation rec {
-  inherit (param) version;
-  name = "coq${coq.coq-version}-mathcomp-finmap-${version}";
-
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "finmap";
-    rev = version;
-    inherit (param) sha256;
-  };
-
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp ];
-
-  installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = {
-    description = "A finset and finmap library";
-    inherit (src.meta) homepage;
-    inherit (mathcomp.meta) platforms license;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
-  };
-}
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 85678a4c6a9..aa6da1a1e28 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -1,70 +1,146 @@
-{ stdenv, fetchFromGitHub, coq, ncurses, which
-, graphviz, withDoc ? false
+{ stdenv, fetchFromGitHub, ncurses, which, graphviz, coq,
+  recurseIntoAttrs, withDoc ? false
 }:
-
-let param =
-
-  if stdenv.lib.versionAtLeast coq.coq-version "8.7" then
-  {
-    version = "1.8.0";
-    sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
-  }
-  else if stdenv.lib.versionAtLeast coq.coq-version "8.6" then
-  {
-    version = "1.7.0";
-    sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
-  }
-  else if stdenv.lib.versionAtLeast coq.coq-version "8.5" then
-  {
-    version = "1.6.1";
-    sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
-  }
-  else throw "No version of math-comp is available for Coq ${coq.coq-version}";
-
-in
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-mathcomp-${version}";
-
-  # used in ssreflect
-  inherit (param) version;
-
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "math-comp";
-    rev = "mathcomp-${param.version}";
-    inherit (param) sha256;
+with builtins // stdenv.lib;
+let
+  # sha256 of released mathcomp versions
+  mathcomp-sha256 = {
+    "1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
+    "1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
+    "1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
+  };
+  # versions of coq compatible with released mathcomp versions
+  mathcomp-coq-versions = {
+    "1.8.0" = flip elem ["8.7" "8.8" "8.9"];
+    "1.7.0" = flip elem ["8.6" "8.7" "8.8" "8.9"];
+    "1.6.1" = flip elem ["8.5"];
   };
+  # computes the default version of mathcomp given a version of Coq
+  min-mathcomp-version = head (naturalSort (attrNames mathcomp-coq-versions));
+  default-mathcomp-version = last (naturalSort ([min-mathcomp-version]
+     ++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions))));
 
-  nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+  # list of core mathcomp packages sorted by dependency order
+  mathcomp-packages =
+    [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
+  # compute the dependencies of the core package pkg
+  # (assuming the total ordering above, rewrite if necessary)
+  mathcomp-deps = pkg: if pkg == "single" then [] else
+    (split (x: x == pkg) mathcomp-packages).left;
 
-  enableParallelBuilding = true;
+  # generic split function (TODO: move to lib?)
+  split = pred: l:
+    let loop = v: l: if l == [] then {left = v; right = [];}
+      else let hd = builtins.head l; tl = builtins.tail l; in
+      if pred hd then {left = v; right = tl;} else loop (v ++ [hd]) tl;
+    in loop [] l;
 
-  buildFlags = stdenv.lib.optionalString withDoc "doc";
+  # exported, documented at the end.
+  mathcompGen = mkMathcompGenFrom (_: {}) mathcomp-packages;
 
-  COQBIN = "${coq}/bin/";
+  # exported, documented at the end.
+  mathcompGenSingle = mkMathcompGen (_: {}) "single";
 
-  preBuild = ''
-    patchShebangs etc/utils/ssrcoqdep || true
-    cd mathcomp
-  '';
+  # mkMathcompGen: internal mathcomp package generator
+  # returns {error = ...} if impossible to generate
+  # returns {${mathcomp-pkg} = <derivation>} otherwise
+  mkMathcompGenFrom = o: l: mcv: fold (pkg: pkgs: pkgs // mkMathcompGen o pkg mcv) {} l;
+  mkMathcompGen = overrides: mathcomp-pkg: mathcomp-version:
+    let
+      coq-version-check = mathcomp-coq-versions.${mathcomp-version} or (_: false);
+      pkgpath = {single = "mathcomp";}.${mathcomp-pkg} or "mathcomp/${mathcomp-pkg}";
+      pkgname = {single = "mathcomp";}.${mathcomp-pkg} or "mathcomp-${mathcomp-pkg}";
+      pkgallMake = ''
+      echo "all.v" > Make
+      echo "-I ." >> Make
+      echo "-R . mathcomp.all" >> Make
+      '';
 
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '' + stdenv.lib.optionalString withDoc ''
-    make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
-  '';
+      # the base set of attributes for mathcomp
+      attrs = rec {
+        name = "coq${coq.coq-version}-${pkgname}-${mathcomp-version}";
 
-  meta = with stdenv.lib; {
-    homepage = http://ssr.msr-inria.inria.fr/;
-    license = licenses.cecill-b;
-    maintainers = [ maintainers.vbgl maintainers.jwiegley ];
-    platforms = coq.meta.platforms;
-  };
+        # used in ssreflect
+        version = mathcomp-version;
 
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
-  };
+        src = fetchFromGitHub {
+          owner = "math-comp";
+          repo = "math-comp";
+          rev = "mathcomp-${mathcomp-version}";
+          sha256 = mathcomp-sha256.${mathcomp-version};
+        };
+
+        nativeBuildInputs = optionals withDoc [ graphviz ];
+        buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+        propagatedBuildInputs = [ coq ] ++
+           attrValues (mkMathcompGenFrom overrides (mathcomp-deps mathcomp-pkg) mathcomp-version);
+        enableParallelBuilding = true;
+
+        buildFlags = optionalString withDoc "doc";
+
+        COQBIN = "${coq}/bin/";
+
+        preBuild = ''
+          patchShebangs etc/utils/ssrcoqdep || true
+          cd ${pkgpath}
+        '' + optionalString (mathcomp-pkg == "all") pkgallMake;
+
+        installPhase = ''
+          make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
+        '' + optionalString withDoc ''
+          make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
+        '';
+
+        meta = with stdenv.lib; {
+          homepage = http://ssr.msr-inria.inria.fr/;
+          license = licenses.cecill-b;
+          maintainers = [ maintainers.vbgl maintainers.jwiegley ];
+          platforms = coq.meta.platforms;
+        };
+
+        passthru = {
+          compatibleCoqVersions = coq-version-check;
+          currentOverrides = overrides;
+          overrideMathcomp = moreOverrides:
+            (mkMathcompGen (old: let new = overrides old; in new // moreOverrides new)
+                          mathcomp-pkg mathcomp-version).${mathcomp-pkg};
+          mathcompGen = moreOverrides:
+            (mkMathcompGenFrom (old: let new = overrides old; in new // moreOverrides new)
+                          mathcomp-packages mathcomp-version);
+        };
+      };
+    in
+    {"${mathcomp-pkg}" = stdenv.mkDerivation (attrs // overrides attrs);};
+
+getAttrOr = a: n: a."${n}" or (throw a.error);
+
+mathcompCorePkgs_1_7 = mathcompGen "1.7.0";
+mathcompCorePkgs_1_8 = mathcompGen "1.8.0";
+mathcompCorePkgs     = recurseIntoAttrs
+  (mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
+
+in rec {
+# mathcompGenSingle: given a version of mathcomp
+# generates an attribute set {single = <drv>;} with the single mathcomp derivation
+inherit mathcompGenSingle;
+mathcomp_1_7_single = getAttrOr (mathcompGenSingle "1.7.0") "single";
+mathcomp_1_8_single = getAttrOr (mathcompGenSingle "1.8.0") "single";
+mathcomp_single     = dontDistribute
+ (getAttrOr (mathcompGenSingle default-mathcomp-version) "single");
+
+# mathcompGen: given a version of mathcomp
+# generates an attribute set {ssreflect = <drv>; ... character = <drv>; all = <drv>;}.
+# each of these have a special attribute overrideMathcomp which
+# must be used instead of overrideAttrs in order to also fix the dependencies
+inherit mathcompGen mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs;
+
+mathcomp_1_7 = getAttrOr mathcompCorePkgs_1_7 "all";
+mathcomp_1_8 = getAttrOr mathcompCorePkgs_1_8 "all";
+mathcomp     = getAttrOr mathcompCorePkgs     "all";
+
+ssreflect     = getAttrOr mathcompCorePkgs     "ssreflect";
 
-}
+} //
+(mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = pkg;}) mathcompCorePkgs) //
+(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_7"; value = pkg;}) mathcompCorePkgs_1_7) //
+(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_8"; value = pkg;}) mathcompCorePkgs_1_8)
diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix
new file mode 100644
index 00000000000..ef387985e06
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp/extra.nix
@@ -0,0 +1,138 @@
+{ stdenv, fetchFromGitHub, coq, mathcomp, coqPackages,
+  recurseIntoAttrs }:
+with builtins // stdenv.lib;
+let current-mathcomp = mathcomp; in
+let
+# configuring packages
+param = {
+  finmap = {
+    version-sha256 = {
+      "1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
+      "1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+      "1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+    };
+    description = "A finset and finmap library";
+  };
+  bigenough = {
+    version-sha256 = {"1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";};
+    description = "A small library to do epsilon - N reasonning";
+  };
+  multinomials = {
+    version-sha256 = {
+      "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+      "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+      "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+    };
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+  };
+ analysis = {
+    version-sha256 = {
+      "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
+      "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
+    };
+    description = "Analysis library compatible with Mathematical Components";
+  };
+};
+versions = {
+  "1.8.0" = {
+    finmap.version = "1.2.0";
+    bigenough.version = "1.0.0";
+    analysis = {
+      version = "0.2.0";
+      core-deps = with coqPackages; [ mathcomp_1_8-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
+    };
+    multinomials = {
+      version = "1.2";
+      core-deps = with coqPackages; [ mathcomp_1_8-algebra ];
+      extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
+    };
+  };
+  "1.7.0" = {
+    finmap.version = "1.1.0";
+    bigenough.version = "1.0.0";
+    analysis = {
+      version = "0.1.0";
+      core-deps = with coqPackages; [ mathcomp_1_7-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ];
+    };
+    multinomials = {
+      version = "1.1";
+      core-deps = with coqPackages; [ mathcomp_1_7-algebra ];
+      extra-deps = with coqPackages; [ mathcomp_1_7-finmap_1_0 mathcomp_1_7-bigenough ];
+    };
+  };
+};
+
+# generic package generator
+packageGen = {
+  # optional arguments
+  src ? "",
+  owner ? "math-comp",
+  core-deps ? [ coqPackages.mathcomp-ssreflect ],
+  extra-deps ? [],
+  coq-versions ? ["8.6" "8.7" "8.8" "8.9"],
+  mathcomp ? current-mathcomp,
+  license ? mathcomp.meta.license,
+  # mandatory
+  package, version, version-sha256, description
+  }:
+  if version == "" then {}
+  else { "${package}" =
+  let from = src; in
+
+  stdenv.mkDerivation rec {
+    inherit version;
+    name = "coq${coq.coq-version}-mathcomp-${mathcomp.version}-${package}-${version}";
+
+    src = if from == "" then fetchFromGitHub {
+      owner = owner;
+      repo = package;
+      rev = version;
+      sha256 = version-sha256."${version}";
+    } else from;
+
+    propagatedBuildInputs = [ coq mathcomp ] ++ extra-deps;
+
+    installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+    meta = {
+      inherit description;
+      inherit license;
+      inherit (src.meta) homepage;
+      inherit (mathcomp.meta) platforms;
+      maintainers = [ stdenv.lib.maintainers.vbgl ];
+    };
+
+    passthru = {
+      inherit version-sha256;
+      compatibleCoqVersions = v: builtins.elem v coq-versions;
+    };
+  };};
+
+current-versions = versions."${current-mathcomp.version}"
+  or (throw "no mathcomp extra packages found for mathcomp ${current-mathcomp.version}");
+
+select = x: mapAttrs (n: pkg: {package = n;} // pkg)
+              (recursiveUpdate (overrideExisting x param) x);
+
+all = (mapAttrs' (n: pkg:
+        {name = "mathcomp_1_7-${n}";
+         value = (packageGen ({mathcomp = coqPackages.mathcomp_1_7;} // pkg))."${n}";})
+        (select versions."1.7.0")) //
+      (mapAttrs' (n: pkg:
+        {name = "mathcomp_1_8-${n}";
+         value = (packageGen ({mathcomp = coqPackages.mathcomp_1_8;} // pkg))."${n}";})
+        (select versions."1.8.0")) //
+     (recurseIntoAttrs (mapDerivationAttrset dontDistribute (
+        mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg)."${n}";})
+              (select current-versions))));
+in
+{
+mathcompExtraGen = packageGen;
+mathcomp_1_7-finmap_1_0 =
+  (packageGen (select {finmap = {version = "1.0.0";
+                                 mathcomp = coqPackages.mathcomp_1_7;};
+                      }).finmap).finmap;
+multinomials = all.mathcomp-multinomials;
+} // all
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
deleted file mode 100644
index aa22c96256f..00000000000
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ /dev/null
@@ -1,28 +0,0 @@
-{ stdenv, fetchFromGitHub, coq, mathcomp }:
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-multinomials-${version}";
-  version = "1.0";
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "multinomials";
-    rev = version;
-    sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
-  };
-
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = {
-    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-    inherit (src.meta) homepage;
-    license = stdenv.lib.licenses.cecill-b;
-    inherit (coq.meta) platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
-  };
-}