coqPackages.mathcomp-boot: init at master (future 2.5.0)

pkgs/development/coq-modules/mathcomp-analysis/default.nix

@@ -167,6 +167,7 @@ let
     package:
     let
       classical-deps = [
+        mathcomp.ssreflect
         mathcomp.algebra
         mathcomp-finmap
       ];

pkgs/development/coq-modules/mathcomp/default.nix

@@ -131,22 +131,28 @@ let
   releaseRev = v: "mathcomp-${v}";
 
   # list of core mathcomp packages sorted by dependency order
-  packages = [
-    "ssreflect"
-    "fingroup"
-    "algebra"
-    "solvable"
-    "field"
-    "character"
-    "all"
-  ];
+  packages = {
+    "boot" = [ ];
+    "order" = [ "boot" ];
+    "fingroup" = [ "boot" ];
+    "ssreflect" = [
+      "boot"
+      "order"
+    ];
+    "algebra" = [
+      "order"
+      "fingroup"
+    ];
+    "solvable" = [ "algebra" ];
+    "field" = [ "solvable" ];
+    "character" = [ "field" ];
+    "all" = [ "character" ];
+  };
 
   mathcomp_ =
     package:
     let
-      mathcomp-deps = lib.optionals (package != "single") (
-        map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages))
-      );
+      mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath = if package == "single" then "." else package;
       pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
       pkgallMake = ''
@@ -188,7 +194,7 @@ let
             + ''
               # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
               test -d mathcomp && cd mathcomp
-              cd ${pkgpath}
+              cd ${pkgpath} || cd ssreflect  # before 2.5, boot didn't exist, make it behave as ssreflect
             ''
             + lib.optionalString (package == "all") pkgallMake;
 
@@ -202,7 +208,7 @@ let
             ];
           };
         }
-        // lib.optionalAttrs (package != "single") { passthru = lib.genAttrs packages mathcomp_; }
+        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
         // lib.optionalAttrs withDoc {
           htmldoc_template = fetchzip {
             url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
@@ -264,7 +270,28 @@ let
           propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
         }
       );
+      # boot and order packages didn't exist before 2.5,
+      # so make boot behave as ssreflect then (c.f., above)
+      # and building nothing in order and ssreflect
+      patched-derivation5 = patched-derivation4.overrideAttrs (
+        o:
+        lib.optionalAttrs
+          (
+            lib.elem package [
+              "order"
+              "ssreflect"
+            ]
+            && o.version != null
+            && o.version != "dev"
+            && lib.versions.isLt "2.5" o.version
+          )
+          {
+            preBuild = "";
+            buildPhase = "echo doing nothing";
+            installPhase = "echo doing nothing";
+          }
+      );
     in
-    patched-derivation4;
+    patched-derivation5;
 in
 mathcomp_ (if single then "single" else "all")

pkgs/top-level/coq-packages.nix

@@ -129,6 +129,8 @@ let
       math-classes = callPackage ../development/coq-modules/math-classes { };
       mathcomp = callPackage ../development/coq-modules/mathcomp { };
       ssreflect = self.mathcomp.ssreflect;
+      mathcomp-boot = self.mathcomp.boot;
+      mathcomp-order = self.mathcomp.order;
       mathcomp-ssreflect = self.mathcomp.ssreflect;
       mathcomp-fingroup = self.mathcomp.fingroup;
       mathcomp-algebra = self.mathcomp.algebra;