Merge commit '98e3b90b6c8f400ae5438ef868eb992a64b75ce5'

5 files changed, 157 insertions, 56 deletions

diff --git a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
index 0d5a892e2e96..14a7f2dc4e24 100644
--- a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
@@ -1,25 +1,25 @@
 { stdenv, fetchFromGitHub, coq }:
 
-let params =
-  let v_8_8_0 = {
-      rev = "V8.8.0";
-      sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+let params = {
+      "8.6" = {
+        rev = "v8.6.0";
+        sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
+      };
+      "8.7" = {
+        rev = "V8.7.0";
+        sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
+      };
+      "8.8" = {
+        rev = "V8.8.0";
+        sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+      };
+      "8.9" = {
+        rev = "V8.9.0";
+        sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
+      };
     };
-  in
-  {
-    "8.6" = {
-      rev = "v8.6.0";
-      sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
-    };
-    "8.7" = {
-      rev = "V8.7.0";
-      sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
-    };
-    "8.8" = v_8_8_0;
-    "8.9" = v_8_8_0;
-  };
-  param = params."${coq.coq-version}"
-; in
+    param = params."${coq.coq-version}";
+in
 
 stdenv.mkDerivation rec {
 
diff --git a/nixpkgs/pkgs/development/coq-modules/equations/default.nix b/nixpkgs/pkgs/development/coq-modules/equations/default.nix
index 86e5687321b4..b31fcde1b80b 100644
--- a/nixpkgs/pkgs/development/coq-modules/equations/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/equations/default.nix
@@ -15,15 +15,15 @@ let
     };
 
     "8.8" = {
-      version = "1.0";
-      rev = "v1.0-8.8";
-      sha256 = "0dd7zd5j2sv5cw3mfwg33ss2vcj634q3qykakc41sv7f3rfgqfnn";
+      version = "1.2beta2";
+      rev = "v1.2-beta2-8.8";
+      sha256 = "1v9asdlhhks25ngnjn4dafx7nrcc5p0lhriqckh3y79nxbgpq4lx";
     };
 
     "8.9" = {
-      version = "1.2beta";
-      rev = "v1.2-beta-8.9";
-      sha256 = "1sj7vyarmvp1w5kvbhgpgap1yd0yrj4n1jrla0wv70k0jrq5hhpz";
+      version = "1.2beta2";
+      rev = "v1.2-beta2-8.9";
+      sha256 = "0y2zwv7jxs1crprj5qvg46h0v9wyfn99ln40yskq91y9h1lj5h3j";
     };
   };
   param = params."${coq.coq-version}";
diff --git a/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix b/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix
new file mode 100644
index 000000000000..30917fcb78f2
--- /dev/null
+++ b/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix
@@ -0,0 +1,49 @@
+{ stdenv, fetchFromGitHub, which, coq }:
+
+let params = {
+  "8.7" = {
+    version = "0.1";
+    rev = "v0.1-8.7";
+    sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
+  };
+  "8.8" = {
+    version = "0.1";
+    rev = "0.1";
+    sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7";
+  };
+  "8.9" = {
+    version = "0.1";
+    rev = "a69551a49543b22a7d4e6a2484356b56bd05068e";
+    sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73";
+  };
+};
+  param = params."${coq.coq-version}";
+in
+
+stdenv.mkDerivation rec {
+  inherit (param) version;
+  name = "coq${coq.coq-version}-ltac2-${version}";
+
+  src = fetchFromGitHub {
+    owner = "coq";
+    repo = "ltac2";
+    inherit (param) rev sha256;
+  };
+
+  nativeBuildInputs = [ which ];
+  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = {
+    description = "A robust and expressive tactic language for Coq";
+    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    license = stdenv.lib.licenses.lgpl21;
+    inherit (coq.meta) platforms;
+    inherit (src.meta) homepage;
+  };
+
+  passthru = {
+    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
+  };
+}
diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
index aa6da1a1e28c..c769ab5521e8 100644
--- a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
@@ -5,20 +5,23 @@ with builtins // stdenv.lib;
 let
   # sha256 of released mathcomp versions
   mathcomp-sha256 = {
+    "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.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"];
   };
   # 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]
+  max-mathcomp-version = last (naturalSort (attrNames mathcomp-coq-versions));
+  default-mathcomp-version = let v = last (naturalSort (["0.0.0"]
      ++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions))));
+     in if v == "0.0.0" then max-mathcomp-version else v;
 
   # list of core mathcomp packages sorted by dependency order
   mathcomp-packages =
@@ -55,20 +58,22 @@ let
       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 = rec {
-        name = "coq${coq.coq-version}-${pkgname}-${mathcomp-version}";
+        name = "coq${coq.coq-version}-${pkgname}-${custom-version}";
 
         # used in ssreflect
-        version = mathcomp-version;
+        version = custom-version;
 
-        src = fetchFromGitHub {
+        src = if is-released then fetchFromGitHub {
           owner = "math-comp";
           repo = "math-comp";
           rev = "mathcomp-${mathcomp-version}";
           sha256 = mathcomp-sha256.${mathcomp-version};
-        };
+        } else mathcomp-version;
 
         nativeBuildInputs = optionals withDoc [ graphviz ];
         buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
@@ -116,6 +121,7 @@ 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     = recurseIntoAttrs
   (mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
 
@@ -125,6 +131,7 @@ in rec {
 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_single     = dontDistribute
  (getAttrOr (mathcompGenSingle default-mathcomp-version) "single");
 
@@ -132,15 +139,19 @@ mathcomp_single     = dontDistribute
 # 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;
+inherit mathcompGen mathcompCorePkgs
+        mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs_1_9;
+
 
+mathcomp     = getAttrOr mathcompCorePkgs     "all";
 mathcomp_1_7 = getAttrOr mathcompCorePkgs_1_7 "all";
 mathcomp_1_8 = getAttrOr mathcompCorePkgs_1_8 "all";
-mathcomp     = getAttrOr mathcompCorePkgs     "all";
+mathcomp_1_9 = getAttrOr mathcompCorePkgs_1_9 "all";
 
-ssreflect     = getAttrOr mathcompCorePkgs     "ssreflect";
+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_8"; value = pkg;}) mathcompCorePkgs_1_8) //
+(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_9"; value = pkg;}) mathcompCorePkgs_1_9)
diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
index ef387985e062..c30ba19b75a3 100644
--- a/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
+++ b/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
@@ -7,6 +7,7 @@ let
 param = {
   finmap = {
     version-sha256 = {
+      "1.2.1" = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
       "1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
       "1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
       "1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
@@ -27,18 +28,42 @@ param = {
   };
  analysis = {
     version-sha256 = {
+      "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk";
       "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
       "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
     };
     description = "Analysis library compatible with Mathematical Components";
   };
+  real-closed = {
+    version-sha256 = {
+      "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
+      "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl";
+      "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
+    };
+    description = "Mathematical Components Library on real closed fields";
+  };
 };
 versions = {
+  "1.9.0" = {
+    finmap.version = "1.2.1";
+    bigenough.version = "1.0.0";
+    analysis = {
+      version = "0.2.2";
+      core-deps = with coqPackages; [ mathcomp_1_9-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ];
+    };
+    multinomials = {};
+    real-closed = {
+      version = "1.0.3";
+      core-deps = with coqPackages; [ mathcomp_1_9-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_9-bigenough ];
+    };
+  }; 
   "1.8.0" = {
-    finmap.version = "1.2.0";
+    finmap.version = "1.2.1";
     bigenough.version = "1.0.0";
     analysis = {
-      version = "0.2.0";
+      version = "0.2.2";
       core-deps = with coqPackages; [ mathcomp_1_8-field ];
       extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
     };
@@ -47,6 +72,11 @@ versions = {
       core-deps = with coqPackages; [ mathcomp_1_8-algebra ];
       extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
     };
+    real-closed = {
+      version = "1.0.3";
+      core-deps = with coqPackages; [ mathcomp_1_8-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ];
+    };
   };
   "1.7.0" = {
     finmap.version = "1.1.0";
@@ -61,6 +91,11 @@ versions = {
       core-deps = with coqPackages; [ mathcomp_1_7-algebra ];
       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_1_8-field ];
+      extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ];
+    };
   };
 };
 
@@ -71,15 +106,18 @@ packageGen = {
   owner ? "math-comp",
   core-deps ? [ coqPackages.mathcomp-ssreflect ],
   extra-deps ? [],
-  coq-versions ? ["8.6" "8.7" "8.8" "8.9"],
   mathcomp ? current-mathcomp,
+  compatibleCoqVersions ? null,
   license ? mathcomp.meta.license,
   # mandatory
-  package, version, version-sha256, description
+  package, version ? "broken", version-sha256, description
   }:
-  if version == "" then {}
-  else { "${package}" =
-  let from = src; in
+  let
+    theCompatibleCoqVersions = if compatibleCoqVersions == null
+                               then mathcomp.compatibleCoqVersions
+                               else compatibleCoqVersions;
+  in
+  { "${package}" = let from = src; in
 
   stdenv.mkDerivation rec {
     inherit version;
@@ -102,28 +140,31 @@ packageGen = {
       inherit (src.meta) homepage;
       inherit (mathcomp.meta) platforms;
       maintainers = [ stdenv.lib.maintainers.vbgl ];
+      broken = (version == "broken");
     };
 
     passthru = {
       inherit version-sha256;
-      compatibleCoqVersions = v: builtins.elem v coq-versions;
+      compatibleCoqVersions = if meta.broken then _: false
+                              else theCompatibleCoqVersions;
     };
-  };};
+  };
+  };
+
+current-versions = versions."${current-mathcomp.version}" or {};
 
-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 param x);
 
-select = x: mapAttrs (n: pkg: {package = n;} // pkg)
-              (recursiveUpdate (overrideExisting x param) x);
+for-version = v: suffix: (mapAttrs' (n: pkg:
+        {name = "mathcomp_${suffix}-${n}";
+         value = (packageGen ({
+             mathcomp = coqPackages."mathcomp_${suffix}";
+           } // pkg))."${n}";})
+        (select versions."${v}"));
 
-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")) //
+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))));