upgrading default.nix

config.nix

@@ -0,0 +1,4 @@
+{
+  coq = "8.10";
+  mathcomp = "1.11.0+beta1";
+}

default.nix

@@ -1,14 +1,18 @@
 {
-  nixpkgs ? (fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-1.11.tar.gz),
-  config ? (pkgs: {}),
+  nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix
+             else fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-fix-rec.tar.gz),
+  config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}),
   withEmacs ? false,
   print-env ? false,
-  package ? "mathcomp-analysis"
+  package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"),
+  src ? (if builtins.pathExists ./package.nix then ./. else false)
 }:
 with builtins;
 let
   cfg-fun = if isFunction config then config else (pkgs: config);
-  pkgs = import nixpkgs {
+  pkg-src = if src == false then {}
+            else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; };
+  pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs {
     overlays = [ (pkgs: super-pkgs: with pkgs.lib;
       let coqPackages = with pkgs; {
         "8.7" = coqPackages_8_7;
@@ -18,25 +22,39 @@ let
         "8.11" = coqPackages_8_11;
         "default" = coqPackages_8_10;
       }.${(cfg-fun pkgs).coq or "default"}.overrideScope'
-        (self: super:
+        (coqPackages: super-coqPackages:
           let
-            all-pkgs = pkgs // { coqPackages = self; };
-            cfg = { ${package} = ./.; } // {
+            all-pkgs = pkgs // { inherit coqPackages; };
+            cfg = pkg-src // {
               mathcomp-fast = {
                 src = ./.;
-                propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-fast);
+                propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast);
               };
               mathcomp-full = {
                 src = ./.;
-                propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-all);
+                propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all);
               };
             } // (cfg-fun all-pkgs);
           in {
-            # mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config {
-            #   for-coq-and-mc.${self.coq.coq-version}.${self.mathcomp.version} =
-            #     removeAttrs cfg ["mathcomp" "coq"];
-            # };
-            mathcomp = if cfg?mathcomp then self.mathcomp_ cfg.mathcomp else super.mathcomp_ "1.11.0+beta1";
+            mathcomp-extra-config =
+              let mec = super-coqPackages.mathcomp-extra-config; in
+              lib.recursiveUpdate mec {
+                initial = {
+                  # fixing mathcomp analysis to depend on real-closed
+                  mathcomp-analysis = {version, coqPackages} @ args:
+                    let mca = mec.initial.mathcomp-analysis args; in
+                    mca // (
+                      if elem version [ "master" "cauchy_etoile" "holomorphy" ]
+                      then {
+                        propagatedBuildInputs = mca.propagatedBuildInputs ++
+                                                [coqPackages.mathcomp-real-closed];
+                      } else {});
+                };
+                for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} =
+                  (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) //
+                  (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]);
+              };
+            mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp;
           } // mapAttrs
             (package: version: coqPackages.mathcomp-extra package version)
             (removeAttrs cfg ["mathcomp" "coq"])
@@ -48,13 +66,11 @@ let
             src = cleanSourceWith {
               src = cleanSource src;
               filter = path: type: let baseName = baseNameOf (toString path); in ! (
-                # Filter out editor backup / swap files.
-                hasPrefix ".git" baseName ||
                 hasSuffix ".aux" baseName ||
                 hasSuffix ".d" baseName ||
                 hasSuffix ".vo" baseName ||
                 hasSuffix ".glob" baseName ||
-                elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap"]
+                elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"]
               );
             };
           };
@@ -72,10 +88,13 @@ let
       for x in $propagatedBuildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
       echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions"
     }
+    printEnv () {
+      for x in $buildInputs; do echo $x; done
+      for x in $propagatedBuildInputs; do echo $x; done
+    }
     cachixEnv () {
       echo "Pushing environement to cachix"
-      for x in $buildInputs; do printf "  "; echo $x | cachix push math-comp; done
-      for x in $propagatedBuildInputs; do printf "  "; echo $x | cachix push math-comp; done
+      printEnv | cachix push math-comp
     }
     nixDefault () {
       cat $mathcompnix/default.nix
@@ -86,7 +105,9 @@ let
   emacs = with pkgs; emacsWithPackages
     (epkgs: with epkgs.melpaStablePackages; [proof-general]);
 
-  pkg = with pkgs; coqPackages.${package} or (coqPackages.current-mathcomp-extra package);
+  pkg = with pkgs;
+        if package == "mathcomp.single" then coqPackages.mathcomp.single
+        else coqPackages.${package} or (coqPackages.current-mathcomp-extra package);
 in
 if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
   inherit shellHook mathcompnix;

package.nix

@@ -0,0 +1 @@
+"mathcomp-analysis"