Coq: refactoring of mathcomp packages (#86088)

- fixed bignum version
- fixed coq-bits version
- fixed coqprime version
- fixed mathcomp and mathcomp extra packages
  (reworked building scheme and removed unused ssreflect directory)
- giving the user access to function filterCoqPackages, because overrideScope' does not re-apply it.

6 files changed, 598 insertions, 372 deletions

diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index d61d5968ea0..0e8cead0b31 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -18,8 +18,8 @@ let params = {
         sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
       };
       "8.10" = {
-        rev = "V8.10+beta1";
-        sha256 = "1slw227idwjw9a21vj3s6kal22mrmvvlpg8r7xk590ml99bn6404";
+        rev = "V8.10.0";
+        sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
       };
       "8.11" = {
         rev = "V8.11.0";
diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix
index 97fd23208f2..05dcb7898e5 100644
--- a/pkgs/development/coq-modules/coq-bits/default.nix
+++ b/pkgs/development/coq-modules/coq-bits/default.nix
@@ -9,9 +9,9 @@ stdenv.mkDerivation {
 
   src = fetchFromGitHub {
     owner = "coq-community";
-    repo = "coq-bits";
-    rev = "f74498a6c67e97d9565e139d62be8eaae7111f06";
-    sha256 = "1ibg37qxgkmpbpvc78qcb179bcnzl149z1kzwdm8n98xk5ibavrf";
+    repo = "bits";
+    rev = "1.0.0";
+    sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
   };
 
   buildInputs = [ coq ];
diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix
index aaf867baf25..a049fa94d41 100644
--- a/pkgs/development/coq-modules/coqprime/default.nix
+++ b/pkgs/development/coq-modules/coqprime/default.nix
@@ -1,22 +1,26 @@
-{ stdenv, fetchFromGitHub, coq, bignums }:
-
-let params =
-  let v_8_8 = {
-      version = "8.8";
-      sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5";
-    };
-  in
-  {
-    "8.7" = {
-      version = "8.7.2";
-      sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
-    };
-    "8.8" = v_8_8;
-    "8.9" = v_8_8;
-    "8.10" = v_8_8;
-    };
-  param = params.${coq.coq-version}
-; in
+{ stdenv, which, fetchFromGitHub, coq, bignums }:
+
+let
+  params =
+    let v_8_8 = {
+          version = "8.8";
+          sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5";
+        };
+    in
+      {
+        "8.7" = {
+          version = "8.7.2";
+          sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
+        };
+        "8.8" = v_8_8;
+        "8.9" = v_8_8;
+        "8.10" = {
+          version = "8.10";
+          sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz";
+        };
+      };
+  param = params.${coq.coq-version};
+in
 
 stdenv.mkDerivation rec {
 
@@ -30,7 +34,7 @@ stdenv.mkDerivation rec {
     inherit (param) sha256;
   };
 
-  buildInputs = [ coq ];
+  buildInputs = [ which coq ];
 
   propagatedBuildInputs = [ bignums ];
 
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index aeb53a995e5..140bf8ab536 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -1,97 +1,151 @@
-{ stdenv, fetchFromGitHub, ncurses, which, graphviz, coq,
-  recurseIntoAttrs, withDoc ? false
+#############################
+# Main derivation: mathcomp #
+########################################################################
+# This file mainly provides the `mathcomp` derivation, which is        #
+# essentially a meta-package containing all core mathcomp libraries    #
+# (ssreflect fingroup algebra solvable field character). They can be   #
+# accessed individually through the paththrough attributes of mathcomp #
+# bearing the same names (mathcomp.ssreflect, etc).                    #
+#                                                                      #
+# Do not use overrideAttrs, but overrideMathcomp instead, which        #
+# regenerate a full mathcomp derivation with sub-derivations, and      #
+# behave the same as `mathcomp_`, described below.                     #
+########################################################################
+
+############################################################
+# Compiling a custom version of mathcomp using `mathcomp_` #
+##############################################################################
+# The prefered way to compile a custom version of mathcomp (other than a     #
+# released version which should be added to `mathcomp-config-initial`        #
+# and pushed to nixpkgs), is to apply the function `coqPackages.mathcomp_`   #
+# to either:                                                                 #
+# - a string without slash, which is interpreted as a github revision,       #
+#   i.e. either a tag, a branch or a commit hash                             #
+# - a string with slashes "owner/p_1/.../p_n", which is interpreted as       #
+#   github owner "owner" and revision "p_1/.../p_n".                         #
+# - a path which is interpreted as a local source for the repository,        #
+#   the name of the version is taken to be the basename of the path          #
+#   i.e. if the path is /home/you/git/package/branch/,                       #
+#        then "branch" is the name of the version                            #
+# - an attribute set which overrides some attributes (e.g. the src)          #
+#   if the version is updated, the name is automatically regenerated using   #
+#   the conventional schema "coq${coq.coq-version}-${pkgname}-${version}"    #
+# - a "standard" override function (old: new_attrs) to override the default  #
+#   attribute set, so that you can use old.${field} to patch the derivation. #
+##############################################################################
+
+#########################################################################
+# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix #
+#########################################################################
+
+#################################
+# Adding a new mathcomp version #
+#############################################################################
+# When adding a new version of mathcomp, add an attribute to `sha256` (use  #
+# ```sh                                                                     #
+# nix-prefetch-url --unpack                                                 #
+# https://github.com/math-comp/math-comp/archive/version.tar.gz             #
+# ```                                                                       #
+# to get the corresponding `sha256`) and to `coq-version` (read the release #
+# notes to check which versions of coq it is compatible with). Then add     #
+# it in `preference version`, if not all mathcomp-extra packages are        #
+# ready, you might want to give new release secondary priority.             #
+#############################################################################
+
+
+{ stdenv, fetchFromGitHub, ncurses, which, graphviz,
+  recurseIntoAttrs, withDoc ? false,
+  coqPackages,
+  mathcomp_, mathcomp, mathcomp-config,
 }:
 with builtins // stdenv.lib;
 let
-  ####################################
-  # CONFIGURATION (please edit this) #
-  ####################################
-  # sha256 of released mathcomp versions
-  mathcomp-sha256 = {
-    "1.10.0" = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
-    "1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
-    "1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
-    "1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
-    "1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
-  };
-  # versions of coq compatible with released mathcomp versions
-  mathcomp-coq-versions = {
-    "1.10.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
-    "1.9.0" = flip elem ["8.7" "8.8" "8.9" "8.10"];
-    "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"];
+  mathcomp-config-initial = rec {
+  #######################################################################
+  # CONFIGURATION (please edit this), it is exported as mathcomp-config #
+  #######################################################################
+    # sha256 of released mathcomp versions
+    sha256 = {
+      "1.11.0+beta1" = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm";
+      "1.10.0"       = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
+      "1.9.0"        = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
+      "1.8.0"        = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
+      "1.7.0"        = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
+      "1.6.1"        = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
+    };
+    # versions of coq compatible with released mathcomp versions
+    coq-versions     = {
+      "1.11.0+beta1" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
+      "1.10.0"       = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
+      "1.9.0"        = flip elem [ "8.7" "8.8" "8.9" "8.10" ];
+      "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"];
+    };
+
+    # sets the default version of mathcomp given a version of Coq
+    # this is currently computed using version-perference below
+    # but it can be set to a fixed version number
+    preferred-version = let v = head (
+      filter (mc: mathcomp-config.coq-versions.${mc} coq.coq-version)
+        mathcomp-config.version-preferences ++ ["0.0.0"]);
+     in if v == "0.0.0" then head mathcomp-config.version-preferences else v;
+
+    # mathcomp preferred versions by decreasing order
+    # (the first version in the list will be tried first)
+    version-preferences =
+      [ "1.10.0" "1.9.0" "1.11.0+beta1" "1.8.0" "1.7.0" "1.6.1" ];
+
+    # list of core mathcomp packages sorted by dependency order
+    packages = _version: # unused in current versions of mathcomp
+      # because the following list of packages is fixed for
+      # all versions of mathcomp up to 1.11.0
+      [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
+
+    # compute the dependencies of the core package pkg
+    # (assuming the total ordering above, change if necessary)
+    deps = version: pkg: if pkg == "single" then [] else
+      (pred-split-list (x: x == pkg) (mathcomp-config.packages version)).left;
   };
-  # computes the default version of mathcomp given a version of Coq
-  max-mathcomp-version = last (naturalSort (attrNames mathcomp-coq-versions));
-  # mathcomp prefered version by decreasing order
-  # (the first version in the list will be tried first)
-  mathcomp-version-preference = [ "1.8.0" "1.9.0" "1.10.0" "1.7.0" "1.6.1" ];
 
   ##############################################################
   # COMPUTED using the configuration above (edit with caution) #
   ##############################################################
-  default-mathcomp-version = let v = head (
-    filter (mc: mathcomp-coq-versions.${mc} coq.coq-version)
-            mathcomp-version-preference ++ ["0.0.0"]);
-     in if v == "0.0.0" then max-mathcomp-version else v;
-
-  # 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;
 
   # generic split function (TODO: move to lib?)
-  split = pred: l:
+  pred-split-list = 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;
 
-  # exported, documented at the end.
-  mathcompGen = mkMathcompGenFrom (_: {}) mathcomp-packages;
+  pkgUp = l: r: l // r // {
+    meta     = (l.meta or {}) // (r.meta or {});
+    passthru = (l.passthru or {}) // (r.passthru or {});
+  };
 
-  # exported, documented at the end.
-  mathcompGenSingle = mkMathcompGen (_: {}) "single";
+  coq = coqPackages.coq;
+  mathcomp-deps = mathcomp-config.deps mathcomp.config.preferred-version;
 
-  # 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:
+  # default set of attributes given a 'package' name.
+  # this attribute set will be extended using toOverrideFun
+  default-attrs = package:
     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}";
+      pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
+      pkgname = if package == "single" then "mathcomp" else "mathcomp-${package}";
       pkgallMake = ''
-      echo "all.v" > Make
-      echo "-I ." >> Make
-      echo "-R . mathcomp.all" >> Make
+        echo "all.v"  > Make
+        echo "-I ." >>   Make
+        echo "-R . mathcomp.all" >> Make
       '';
-      is-released = builtins.isString mathcomp-version;
-      custom-version = if is-released then mathcomp-version else "custom";
-
-      # the base set of attributes for mathcomp
-      attrs = {
-        name = "coq${coq.coq-version}-${pkgname}-${custom-version}";
-
-        # used in ssreflect
-        version = custom-version;
-
-        src = if is-released then fetchFromGitHub {
-          owner = "math-comp";
-          repo = "math-comp";
-          rev = "mathcomp-${mathcomp-version}";
-          sha256 = mathcomp-sha256.${mathcomp-version};
-        } else mathcomp-version;
+    in
+      rec {
+        version = "master";
+        name = "coq${coq.coq-version}-${pkgname}-${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);
+        propagatedBuildInputs = [ coq ];
         enableParallelBuilding = true;
 
         buildFlags = optional withDoc "doc";
@@ -101,7 +155,7 @@ let
         preBuild = ''
           patchShebangs etc/utils/ssrcoqdep || true
           cd ${pkgpath}
-        '' + optionalString (mathcomp-pkg == "all") pkgallMake;
+        '' + optionalString (package == "all") pkgallMake;
 
         installPhase = ''
           make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
@@ -110,67 +164,98 @@ let
         '';
 
         meta = with stdenv.lib; {
-          homepage = "https://math-comp.github.io/";
-          license = licenses.cecill-b;
-          maintainers = [ maintainers.vbgl maintainers.jwiegley ];
-          platforms = coq.meta.platforms;
+          homepage    = "https://math-comp.github.io/";
+          license     = licenses.cecill-b;
+          maintainers = [ maintainers.vbgl maintainers.jwiegley maintainers.cohencyril ];
+          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);
+          mathcompDeps = mathcomp-deps package;
+          inherit package mathcomp-config;
+          compatibleCoqVersions = _: true;
         };
       };
+
+  # converts a string, path or attribute set into an override function
+  toOverrideFun = overrides:
+    if isFunction overrides then overrides else old:
+      let
+          pkgname = if old.passthru.package == "single" then "mathcomp"
+                    else "mathcomp-${old.passthru.package}";
+
+          string-attrs = if hasAttr overrides mathcomp-config.sha256 then
+                let version = overrides;
+                in {
+                  inherit version;
+                  src = fetchFromGitHub {
+                    owner  = "math-comp";
+                    repo   = "math-comp";
+                    rev    = "mathcomp-${version}";
+                    sha256 = mathcomp-config.sha256.${version};
+                  };
+                  passthru = old.passthru // {
+                    compatibleCoqVersions = mathcomp-config.coq-versions.${version};
+                    mathcompDeps = mathcomp-config.deps version old.passthru.package;
+                  };
+                }
+              else
+                let splitted = filter isString (split "/" overrides);
+                    owner    = head splitted;
+                    ref      = concatStringsSep "/" (tail splitted);
+                    version  = head (reverseList splitted);
+                in if length splitted == 1 then {
+                  inherit version;
+                  src = fetchTarball "https://github.com/math-comp/math-comp/archive/${version}.tar.gz";
+                } else {
+                  inherit version;
+                  src = fetchTarball "https://github.com/${owner}/math-comp/archive/${ref}.tar.gz";
+                };
+
+          attrs =
+            if overrides == null || overrides == "" then _: {}
+            else  if isString overrides then string-attrs
+            else  if isPath overrides then { version = baseNameOf overrides; src = overrides; }
+            else  if isAttrs overrides then pkgUp old overrides
+            else  let overridesStr = toString overrides; in
+                  abort "${overridesStr} not a legitimate overrides";
+      in
+        attrs // (if attrs?version && ! (attrs?name)
+                  then { name = "coq${coq.coq-version}-${pkgname}-${attrs.version}"; } else {});
+
+  # generates {ssreflect = «derivation ...» ; ... ; character = «derivation ...», ...}
+  mkMathcompGenSet = pkgs: o:
+    fold (pkg: pkgs: pkgs // {${pkg} = mkMathcompGen pkg o;}) {} pkgs;
+  # generates the derivation of one mathcomp package.
+  mkMathcompGen = package: overrides:
+    let
+      up = x: o: x // (toOverrideFun o x);
+      fixdeps = attrs:
+        let version = attrs.version or "master";
+            mcdeps  = if package == "single" then {}
+                      else mkMathcompGenSet (filter isString attrs.passthru.mathcompDeps) overrides;
+            allmc   = mkMathcompGenSet (mathcomp-config.packages version ++ [ "single" ]) overrides;
+        in {
+          propagatedBuildInputs = [ coq ]
+                                  ++ filter isDerivation attrs.passthru.mathcompDeps
+                                  ++ attrValues mcdeps
+          ;
+          passthru = allmc //
+                     { overrideMathcomp = o: mathcomp_ (old: up (up old overrides) o); };
+        };
     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_1_9 = mathcompGen "1.9.0";
-mathcompCorePkgs_1_10 = mathcompGen "1.10.0";
-mathcompCorePkgs     = recurseIntoAttrs
-  (mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
-
-in {
-# 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_1_9_single = getAttrOr (mathcompGenSingle "1.9.0") "single";
-mathcomp_1_10_single = getAttrOr (mathcompGenSingle "1.10.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
-        mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs_1_9
-	mathcompCorePkgs_1_10
-	;
-
-
-mathcomp     = getAttrOr mathcompCorePkgs     "all";
-mathcomp_1_7 = getAttrOr mathcompCorePkgs_1_7 "all";
-mathcomp_1_8 = getAttrOr mathcompCorePkgs_1_8 "all";
-mathcomp_1_9 = getAttrOr mathcompCorePkgs_1_9 "all";
-mathcomp_1_10 = getAttrOr mathcompCorePkgs_1_10 "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) //
-(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_9"; value = pkg;}) mathcompCorePkgs_1_9) //
-(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_10"; value = pkg;}) mathcompCorePkgs_1_10)
+      stdenv.mkDerivation (up (up (default-attrs package) overrides) fixdeps);
+in
+{
+  mathcomp-config    = mathcomp-config-initial;
+  mathcomp_          = mkMathcompGen "all";
+  mathcomp           = mathcomp_ mathcomp-config.preferred-version;
+  # mathcomp-single    = mathcomp.single;
+  ssreflect          = mathcomp.ssreflect;
+  mathcomp-ssreflect = mathcomp.ssreflect;
+  mathcomp-fingroup  = mathcomp.fingroup;
+  mathcomp-algebra   = mathcomp.algebra;
+  mathcomp-solvable  = mathcomp.solvable;
+  mathcomp-field     = mathcomp.field;
+  mathcomp-character = mathcomp.character;
+}
diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix
index 2df9cbe58c7..d37608658b4 100644
--- a/pkgs/development/coq-modules/mathcomp/extra.nix
+++ b/pkgs/development/coq-modules/mathcomp/extra.nix
@@ -1,202 +1,371 @@
-{ stdenv, fetchFromGitHub, coq, ssreflect, coqPackages,
-  recurseIntoAttrs }:
+##########################################################
+# Main derivation:                                       #
+#   mathcomp-finmap mathcomp-analysis mathcomp-bigenough #
+#   mathcomp-multinomials mathcomp-real-closed coqeal    #
+# Additionally:                                          #
+#   mathcomp-extra-all  contains all the extra packages  #
+#   mathcomp-extra-fast contains the one not marked slow #
+########################################################################
+# This file mainly provides the above derivations, which are packages  #
+# extra mathcomp libraries based on mathcomp.                          #
+########################################################################
+
+#####################################################
+# Compiling customs versions using `mathcomp-extra` #
+##############################################################################
+# The prefered way to compile a custom version of mathcomp extra packages    #
+# (other than released versions which should be added to                     #
+# `rec-mathcomp-extra-config` and pushed to nixpkgs, see below),             #
+# is to use `coqPackages.mathcomp-extra name version` where                  #
+# 1. `name` is a string representing the name of a declared package          #
+#    OR undeclared package.                                                  #
+# 2. `version` is either:                                                    #
+# - a string without slash, which is interpreted as a github revision,       #
+#   i.e. either a tag, a branch or a commit hash                             #
+# - a string with slashes "owner/p_1/.../p_n", which is interpreted as       #
+#   github owner "owner" and revision "p_1/.../p_n".                         #
+# - a path which is interpreted as a local source for the repository,        #
+#   the name of the version is taken to be the basename of the path          #
+#   i.e. if the path is /home/you/git/package/branch/,                       #
+#        then "branch" is the name of the version                            #
+# - an attribute set which overrides some attributes (e.g. the src)          #
+#   if the version is updated, the name is automatically regenerated using   #
+#   the conventional schema "coq${coq.coq-version}-${pkgname}-${version}"    #
+# - a "standard" override function (old: new_attrs) to override the default  #
+#   attribute set, so that you can use old.${field} to patch the derivation. #
+#                                                                            #
+# Should you choose to use `pkg.overrideAttrs` instead, we provide the       #
+# function mathcomp-extra-override which takes a name and a version exactly  #
+# as above and returns an override function.                                 #
+##############################################################################
+
+#########################################################################
+# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix #
+#########################################################################
+
+###########################################
+# Adding a new package or package version #
+################################################################################
+# 1. Update or add a `package` entry to `initial`, it must be a function       #
+#    taking the version as argument and returning an attribute set. Everything #
+#    is optional and the default for the sources of the repository and the     #
+#    homepage will be https://github.com/math-comp/${package}.                 #
+#                                                                              #
+# 2. Update or add a `package` entry to `sha256` for each release.             #
+#    You may use                                                               #
+#    ```sh                                                                     #
+#    nix-prefetch-url --unpack                                                 #
+#    https://github.com/math-comp/math-comp/archive/version.tar.gz             #
+#    ```                                                                       #
+#                                                                              #
+# 3. Update or create a new consistent set of extra packages.                  #
+#    /!\ They must all be co-compatible. /!\                                   #
+#    Do not use versions that may disappear: it must either be                 #
+#    - a tag from the main repository (e.g. version or tag), or                #
+#    - a revision hash that has been *merged in master*                        #
+################################################################################
+
+{ stdenv, fetchFromGitHub, recurseIntoAttrs,
+  which, mathcomp, coqPackages,
+  mathcomp-extra-config, mathcomp-extra-override,
+  mathcomp-extra, current-mathcomp-extra,
+}:
 with builtins // stdenv.lib;
-let current-ssreflect = ssreflect; in
 let
-# configuring packages
-param = {
-  finmap = {
-    version-sha256 = {
-      "1.2.1" = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
-      "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.3" = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
-      "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
-      "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
-      "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
-    };
-    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-  };
- analysis = {
-    version-sha256 = {
-      "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk";
-      "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
-      "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
-    };
-    compatibleCoqVersions = flip elem ["8.8" "8.9"];
-    description = "Analysis library compatible with Mathematical Components";
-    license = stdenv.lib.licenses.cecill-c;
-  };
-  real-closed = {
-    version-sha256 = {
-      "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
-      "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl";
-      "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
-    };
-    description = "Mathematical Components Library on real closed fields";
-  };
-  coqeal = {
-    version-sha256 = {
-      "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii";
-    };
-    description = "CoqEAL - The Coq Effective Algebra Library";
-    owner = "CoqEAL";
-    compatibleCoqVersions = flip elem ["8.7" "8.8" "8.9"];
-    license = stdenv.lib.licenses.mit;
-  };
-};
-versions = {
-  "1.9.0" = {
-    finmap.version = "1.2.1";
-    bigenough.version = "1.0.0";
-    analysis = {
-      version = "0.2.2";
-      core-deps = with coqPackages; [ mathcomp-field_1_9 ];
-      extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ];
-    };
-    multinomials = {
-      version = "1.3";
-      core-deps = with coqPackages; [ mathcomp-algebra_1_9 ];
-      extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ];
-    };
-    real-closed = {
-      version = "1.0.3";
-      core-deps = with coqPackages; [ mathcomp-field_1_9 ];
-      extra-deps = with coqPackages; [ mathcomp_1_9-bigenough ];
-    };
-  };
-  "1.8.0" = {
-    finmap.version = "1.2.1";
-    bigenough.version = "1.0.0";
-    analysis = {
-      version = "0.2.2";
-      core-deps = with coqPackages; [ mathcomp-field_1_8 ];
-      extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
-    };
-    multinomials = {
-      version = "1.3";
-      core-deps = with coqPackages; [ mathcomp-algebra_1_8 ];
-      extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
-    };
-    real-closed = {
-      version = "1.0.3";
-      core-deps = with coqPackages; [ mathcomp-field_1_8 ];
-      extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ];
-    };
-    coqeal = {
-      version = "1.0.0";
-      core-deps = with coqPackages; [ mathcomp-algebra_1_8 ];
-      extra-deps = with coqPackages; [ bignums paramcoq mathcomp_1_8-multinomials ];
-    };
-  };
-  "1.7.0" = {
-    finmap.version = "1.1.0";
-    bigenough.version = "1.0.0";
-    analysis = {
-      version = "0.1.0";
-      core-deps = with coqPackages; [ mathcomp-field_1_7 ];
-      extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ];
-    };
-    multinomials = {
-      version = "1.1";
-      core-deps = with coqPackages; [ mathcomp-algebra_1_7 ];
-      extra-deps = with coqPackages; [ mathcomp_1_7-finmap_1_0 mathcomp_1_7-bigenough ];
-    };
-    real-closed = {
-      version = "1.0.1";
-      core-deps = with coqPackages; [ mathcomp-field_1_7 ];
-      extra-deps = with coqPackages; [ mathcomp_1_7-bigenough ];
-    };
-  };
-};
-
-# generic package generator
-packageGen = {
-  # optional arguments
-  src ? "",
-  owner ? "math-comp",
-  extra-deps ? [],
-  ssreflect ? current-ssreflect,
-  core-deps ? null,
-  compatibleCoqVersions ? null,
-  license ? ssreflect.meta.license,
-  # mandatory
-  package, version ? "broken", version-sha256, description
-  }:
-  let
-    theCompatibleCoqVersions = if compatibleCoqVersions == null
-                               then ssreflect.compatibleCoqVersions
-                               else compatibleCoqVersions;
-    mc-core-deps = if builtins.isNull core-deps then [ssreflect] else core-deps;
-  in
-  { ${package} = let from = src; in
+  ##############################
+  # CONFIGURATION, please edit #
+  ##############################
+  ############################
+  # Packages base delaration #
+  ############################
+  rec-mathcomp-extra-config = {
+    initial = {
+      mathcomp-finmap = version: {
+        meta = {
+          description = "A finset and finmap library";
+          repo = "finmap";
+          homepage = "https://github.com/math-comp/finmap";
+        };
+        passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ];
+      };
 
-  stdenv.mkDerivation rec {
-    inherit version;
-    name = "coq${coq.coq-version}-mathcomp${ssreflect.version}-${package}-${version}";
+      mathcomp-bigenough = version: {
+        meta = {
+          description = "A small library to do epsilon - N reasonning";
+          repo = "bigenough";
+          homepage = "https://github.com/math-comp/bigenough";
+        };
+        passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
+      };
 
-    src = if from == "" then fetchFromGitHub {
-      owner = owner;
-      repo = package;
-      rev = version;
-      sha256 = version-sha256.${version};
-    } else from;
+      multinomials = version: {
+        buildInputs = [ which ];
+        propagatedBuildInputs = with coqPackages;
+          [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
+        meta = {
+          description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+          repo = "multinomials";
+          homepage = "https://github.com/math-comp/multinomials";
+        };
+        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
+      };
 
-    propagatedBuildInputs = [ coq ] ++ mc-core-deps ++ extra-deps;
+      mathcomp-analysis = version: {
+        propagatedBuildInputs = with coqPackages;
+          [ mathcomp.field mathcomp-finmap mathcomp-bigenough ];
+        meta = {
+          description = "Analysis library compatible with Mathematical Components";
+          homepage = "https://github.com/math-comp/analysis";
+          repo = "analysis";
+          license = stdenv.lib.licenses.cecill-c;
+        };
+        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
+      };
 
-    installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+      mathcomp-real-closed = version: {
+        propagatedBuildInputs = with coqPackages;
+          [ coq mathcomp.field  mathcomp-bigenough ];
+        meta = {
+          description = "Mathematical Components Library on real closed fields";
+          repo = "real-closed";
+          homepage = "https://github.com/math-comp/real-closed";
+        };
+        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
+      };
 
-    meta = {
-      inherit description;
-      inherit license;
-      inherit (src.meta) homepage;
-      inherit (ssreflect.meta) platforms;
-      maintainers = [ stdenv.lib.maintainers.vbgl ];
-      broken = (version == "broken");
+      coqeal = version: {
+        buildInputs = [ which ];
+        propagatedBuildInputs = with coqPackages;
+          [ mathcomp-algebra bignums paramcoq multinomials ];
+        meta = {
+          description = "CoqEAL - The Coq Effective Algebra Library";
+          homepage = "https://github.com/coqeal/coqeal";
+          license = stdenv.lib.licenses.mit;
+          owner = "CoqEAL";
+        };
+        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
+      };
     };
 
-    passthru = {
-      inherit version-sha256;
-      compatibleCoqVersions = if meta.broken then _: false
-                              else theCompatibleCoqVersions;
+    ###############################
+    # sha256 of released versions #
+    ###############################
+    sha256 = {
+      mathcomp-finmap = {
+        "1.5.0"          = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
+        "1.4.1"          = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
+        "1.4.0+coq-8.11" = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
+        "1.4.0"          = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
+        "1.3.4"          = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
+        "1.3.3"          = "1n844zjhv354kp4g4pfbajix0plqh7yxv6471sgyb46885298am5";
+        "1.3.1"          = "14rvm0rm5hd3pd0srgak3jqmddzfv6n7gdpjwhady5xcgrc7gsx7";
+        "1.2.1"          = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
+        "1.2.0"          = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
+        "1.1.0"          = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+        "1.0.0"          = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+      };
+      mathcomp-bigenough = {
+        "1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
+      };
+      mathcomp-analysis = {
+        "0.2.3" = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
+        "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk";
+        "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
+        "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
+      };
+      multinomials = {
+        "1.5.1" = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
+        "1.5"   = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
+        "1.4"   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
+        "1.3"   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
+        "1.2"   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+        "1.1"   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+        "1.0"   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+      };
+      mathcomp-real-closed = {
+        "1.0.5" = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
+        "1.0.4" = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
+        "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
+        "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl";
+        "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
+      };
+      coqeal = {
+        "1.0.3" = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
+        "1.0.2" = "1brmf3gj03iky1bcl3g9vx8vknny7xfvs0y2rfr85am0296sxsfj";
+        "1.0.1" = "19jhdrv2yp9ww0h8q73ihb2w1z3glz4waf2d2n45klafxckxi7bm";
+        "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii";
+      };
     };
+
+    ################################
+    # CONSISTENT sets of packages. #
+    ################################
+    for-coq-and-mc = let
+      v5 = {
+        mathcomp-finmap       = "1.5.0";
+        mathcomp-bigenough    = "1.0.0";
+        mathcomp-analysis     = "678d3cc37f5f3c71b1bd550836eb44e3ba2a5459";
+        multinomials           = "1.5.1";
+        mathcomp-real-closed  = "1.0.5";
+        coqeal                = "CohenCyril/bdfc96771644b082e41268edc43d61dc5fda2358";
+      };
+      v4 = v3 // { coqeal = "1.0.3"; };
+      v3 = {
+        mathcomp-finmap       = "1.4.0";
+        mathcomp-bigenough    = "1.0.0";
+        mathcomp-analysis     = "0.2.3";
+        multinomials          = "1.5";
+        mathcomp-real-closed  = "1.0.4";
+        coqeal                = "1.0.0";
+      };
+      v2 = {
+        mathcomp-finmap       = "1.3.4";
+        mathcomp-bigenough    = "1.0.0";
+        mathcomp-analysis     = "0.2.3";
+        multinomials          = "1.4";
+        mathcomp-real-closed  = "1.0.3";
+        coqeal                = "1.0.0";
+      };
+      v1 = {
+        mathcomp-finmap       = "1.1.0";
+        mathcomp-bigenough    = "1.0.0";
+        multinomials          = "1.1";
+        mathcomp-real-closed  = "1.0.1";
+        coqeal                = "1.0.0";
+      };
+    in
+      {
+        "8.11" = {
+          "1.11.0+beta1" = v5;
+          "1.10.0"       = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";};
+        };
+        "8.10" = {
+          "1.11.0+beta1" = v5;
+          "1.10.0"       = v4;
+          "1.9.0"        = removeAttrs v3 ["coqeal"];
+        };
+        "8.9" = {
+          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
+          "1.10.0"       = v4;
+          "1.9.0"        = removeAttrs v3 ["coqeal"];
+          "1.8.0"        = removeAttrs v2 ["coqeal"];
+        };
+        "8.8" = {
+          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
+          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
+          "1.9.0"        = removeAttrs v3 ["coqeal"];
+          "1.8.0"        = removeAttrs v2 ["coqeal"];
+          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
+        };
+        "8.7" = {
+          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
+          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
+          "1.9.0"        = removeAttrs v3 ["coqeal"];
+          "1.8.0"        = removeAttrs v2 ["coqeal"];
+          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
+        };
+      };
   };
+
+  ##############################
+  # GENERATION, EDIT WITH CARE #
+  ##############################
+  coq = coqPackages.coq;
+
+  default-attrs = {
+    version = "master";
+    buildInputs = [];
+    propagatedBuildInputs = (with coqPackages; [ ssreflect ]);
+    installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+    meta = {
+      inherit (mathcomp.meta) platforms license;
+      owner = "math-comp";
+      maintainers = [ maintainers.vbgl maintainers.cohencyril ];
+    };
+    passthru.compatibleCoqVersions = (_: true);
   };
 
-current-versions = versions.${current-ssreflect.version} or {};
+  pkgUp = recursiveUpdateUntil (path: l: r: !(isAttrs l && isAttrs r) || path == ["src"]);
 
-select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate param x);
+  # Fixes a partial attribute set using the configuration
+  # in the style of the above mathcomp-extra-config.initial,
+  # and generates a name according to the conventional naming scheme below
+  fix-attrs = pkgcfg:
+    let attrs = pkgUp default-attrs pkgcfg; in
+    pkgUp attrs (rec {
+      name = "coq${coq.coq-version}mathcomp${mathcomp.version}-${attrs.meta.repo or attrs.meta.package or "anonymous"}-${attrs.version}";
+      src = attrs.src or (fetchTarball "${meta.homepage}/archive/${attrs.version}.tar.gz");
+      meta = rec {
+        homepage = attrs.meta.homepage or attrs.src.meta.homepage or "https://github.com/${owner}/${repo}";
+        owner    = attrs.meta.owner or "math-comp";
+        repo     = attrs.meta.repo or attrs.meta.package or "math-comp-nix";
+      };
+    });
 
-for-version = v: suffix: (mapAttrs' (n: pkg:
-        {name = "mathcomp_${suffix}-${n}";
-         value = (packageGen ({
-             ssreflect = coqPackages."mathcomp-ssreflect_${suffix}";
-           } // pkg)).${n};})
-        (select versions.${v}));
+  # Gets a version out of a string, path or attribute set.
+  getVersion = arg:
+    if isFunction arg then (arg {}).version
+    else  if arg == "" then "master"
+    else  if isDerivation arg then arg.drvAttrs.version or "master"
+    else  if isAttrs arg then arg.version or "master"
+    else  if isString arg then head (reverseList (split "/" arg))
+    else  if isPath arg   then (baseNameOf arg)
+    else "master";
 
-all = (for-version "1.7.0" "1_7") //
-      (for-version "1.8.0" "1_8") //
-      (for-version "1.9.0" "1_9") //
-     (recurseIntoAttrs (mapDerivationAttrset dontDistribute (
-        mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg).${n};})
-              (select current-versions))));
+  # Converts a string, path or attribute set into an override function
+  # It tries to fill the `old` argument of the override function using
+  # `mathcomp-extra-config.initial` first and finishes with `fix-attrs`
+  rec-mathcomp-extra-override = generic: old: let
+    version = getVersion generic;
+    package = old.meta.package or "math-comp-nix";
+    cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {})) version) old
+          // { inherit version; };
+    fix = attrs: fix-attrs (pkgUp cfg attrs);
+  in
+    if isFunction generic then fix (generic cfg)
+    else  if generic == null || generic == "" then fix {}
+    else  if isDerivation generic then fix generic.drvAttrs
+    else  if isAttrs generic then fix generic
+    else  if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; }
+    else  let fixedcfg = fix cfg; in fixedcfg // (
+      if isString generic then
+        if (mathcomp-extra-config.sha256.${package} or {})?${generic} then {
+          src = fetchFromGitHub {
+            inherit (fixedcfg.meta) owner repo;
+            rev = version;
+            sha256 = mathcomp-extra-config.sha256.${package}.${version};
+          };
+        }
+        else  let splitted = filter isString (split "/" generic); in {
+        src = fetchTarball
+          ("https://github.com/" +
+           (if length splitted == 1 then "${fixedcfg.meta.owner}/${fixedcfg.meta.repo}/archive/${version}.tar.gz"
+            else "${head splitted}/${fixedcfg.meta.repo}/archive/${concatStringsSep "/" (tail splitted)}.tar.gz"));
+        }
+      else  if isPath generic then { src = generic; }
+      else abort "${toString generic} not a legitimate generic version/override");
+
+  # applies mathcomp-extra-config.for-coq-and-mc to the current mathcomp version
+  for-this = mathcomp-extra-config.for-coq-and-mc.${coq.coq-version}.${mathcomp.version} or {};
+
+  # specializes mathcomp-extra to the current mathcomp version.
+  rec-current-mathcomp-extra = package: mathcomp-extra package (for-this.${package} or {});
 in
-{
-mathcompExtraGen = packageGen;
-mathcomp_1_7-finmap_1_0 =
-  (packageGen (select {finmap = {version = "1.0.0";
-                                 ssreflect = coqPackages.mathcomp-ssreflect_1_7;};
-                      }).finmap).finmap;
-multinomials = all.mathcomp-multinomials;
-coqeal = all.mathcomp-coqeal;
-} // all
+  {
+    mathcomp-extra-override = rec-mathcomp-extra-override;
+    mathcomp-extra-config   = rec-mathcomp-extra-config;
+    current-mathcomp-extra  = rec-current-mathcomp-extra;
+    mathcomp-extra          = package: version:
+      stdenv.mkDerivation (mathcomp-extra-override version {meta = {inherit package;};});
+
+    mathcomp-finmap       = current-mathcomp-extra "mathcomp-finmap";
+    mathcomp-analysis     = current-mathcomp-extra "mathcomp-analysis";
+    mathcomp-bigenough    = current-mathcomp-extra "mathcomp-bigenough";
+    multinomials          = current-mathcomp-extra "multinomials";
+    mathcomp-real-closed  = current-mathcomp-extra "mathcomp-real-closed";
+    coqeal                = current-mathcomp-extra "coqeal";
+
+    mathcomp-extra-fast    = map (pkg: current-mathcomp-extra pkg)
+      (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this));
+    mathcomp-extra-all    = map (pkg: current-mathcomp-extra pkg) (attrNames for-this);
+  }
diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix
deleted file mode 100644
index 01df38375ef..00000000000
--- a/pkgs/development/coq-modules/ssreflect/default.nix
+++ /dev/null
@@ -1,32 +0,0 @@
-{ stdenv, coq, ncurses, which
-, graphviz, mathcomp, withDoc ? false
-}:
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-ssreflect-${version}";
-
-  inherit (mathcomp) src version meta;
-
-  nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
-
-  enableParallelBuilding = true;
-
-  COQBIN = "${coq}/bin/";
-
-  preBuild = ''
-    patchShebangs etc/utils/ssrcoqdep || true
-    cd mathcomp/ssreflect
-  '';
-
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
-
-  postInstall = stdenv.lib.optionalString withDoc ''
-    mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/
-    cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/
-  '';
-
-  passthru.compatibleCoqVersions = mathcomp.compatibleCoqVersions;
-}