coqPackages.mathcomp: 1.12.0 -> 1.13.0

3 years ago · c5c34f6be1
parent 71d0e49b24
commit c5c34f6be1
14 changed files with 52 additions and 20 deletions
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@ -4,10 +4,10 @@
 with lib; mkCoqDerivation {

  pname = "CoqEAL";
-  owner = "CoqEAL";
+
  inherit version;
  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10") "1.12.0" ]; out = "1.0.6"; }
+      { cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.0.6"; }
      { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
      { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; }
      { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@ -9,9 +9,9 @@ with lib;
  owner = "arthuraa";

  inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
-    { case = range "8.11" "8.14"; out = "0.3.0"; }
-    { case = range "8.10" "8.12"; out = "0.2.2"; }
+  defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [
+    { cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; }
+    { cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; }
  ] null;

  releaseRev = v: "v${v}";
--- a/pkgs/development/coq-modules/gaia-hydras/default.nix
+++ b/pkgs/development/coq-modules/gaia-hydras/default.nix
@ -1,4 +1,5 @@
-{ lib, mkCoqDerivation, coq, hydra-battles, gaia, mathcomp-zify, version ? null }:
+{ lib, mkCoqDerivation, coq, hydra-battles, gaia,
+  mathcomp-zify, mathcomp, version ? null }:

 with lib; mkCoqDerivation rec {
  pname = "gaia-hydras";
@ -8,8 +9,8 @@ with lib; mkCoqDerivation rec {
  releaseRev = (v: "v${v}");

  inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
-    { case = range "8.13" "8.14"; out = "0.5"; }
+  defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [
+    { cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
  ] null;

  propagatedBuildInputs = [
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@ -5,11 +5,12 @@ with lib; mkCoqDerivation {

  release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
  release."1.12".sha256 = "sha256:0c6cim4x6f9944g8v0cp0lxs244lrhb04ms4y2s6y1wh321zj5mi";
+  release."1.13".sha256 = "sha256:0i8ix2rbw10v34bi0yrx0z89ng96ydqbxm8rv2rnfgy4d1b27x6q";
  releaseRev = (v: "v${v}");

  inherit version;
  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
-    { cases = [ (range "8.10" "8.14") "1.12.0" ]; out = "1.12"; }
+    { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.13"; }
    { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
  ] null;

--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@ -6,13 +6,17 @@ mkCoqDerivation {
  pname = "abel";
  owner = "math-comp";

-  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
-
  inherit version;
  defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.10" "8.13") (range "1.11.0" "1.12.0") ]; out = "1.0.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.12.0" "1.13.0") ]; out = "1.2.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
    ] null;

+  release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
+  release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
+  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
+
+
  propagatedBuildInputs = [ mathcomp.field mathcomp-real-closed ];

  meta = with lib; {
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@ -18,7 +18,7 @@ let mca = mkCoqDerivation {

  inherit version;
  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.11" "8.13") "1.12.0" ];             out = "0.3.10"; }
+      { cases = [ (range "8.11" "8.14") (isGe "1.12.0") ];      out = "0.3.10"; }
      { cases = [ (range "8.11" "8.13") "1.11.0" ];             out = "0.3.4"; }
      { cases = [ (range "8.10" "8.12") "1.11.0" ];             out = "0.3.3"; }
      { cases = [ (range "8.10" "8.11") "1.11.0" ];             out = "0.3.1"; }
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@ -7,7 +7,7 @@ with lib; mkCoqDerivation {
  owner = "math-comp";
  inherit version;
  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10")          (range "1.11" "1.12") ]; out = "1.5.1"; }
+      { cases = [ (isGe "8.10")          (range "1.11" "1.13") ]; out = "1.5.1"; }
      { cases = [ (range "8.7" "8.11")   "1.11.0" ];              out = "1.5.0"; }
      { cases = [ (isEq "8.11")          (range "1.8" "1.10") ];  out = "1.4.0+coq-8.11"; }
      { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.4.0"; }
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@ -17,7 +17,7 @@ with lib; mkCoqDerivation {
  };

  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10")  "1.12.0" ]; out = "1.1.2"; }
+      { cases = [ (isGe "8.10")  (isGe "1.12.0") ]; out = "1.1.2"; }
      { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
      { cases = [ (isGe "8.7")   (range "1.9.0" "1.10.0") ]; out = "1.0.4"; }
      { cases = [ (isGe "8.7")   "1.8.0"  ]; out = "1.0.3"; }
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@ -0,0 +1,22 @@
+{ coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
+  lib, version ? null }@args:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "tarjan";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with versions;
+    switch [ coq.version mathcomp-ssreflect.version ] [{
+      cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.0.0";
+  }] null;
+  release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
+
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-fingroup ];
+
+  meta = {
+    description = "Proofs of Tarjan and Kosaraju connected components algorithms";
+    license = licenses.cecill-b;
+  };
+}
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@ -1,14 +1,15 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:

 with lib; mkCoqDerivation rec {
-  pname = "mathcomp-zify";
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "zify";
  repo = "mczify";
  owner = "math-comp";
  inherit version;

  defaultVersion = with versions;
     switch [ coq.coq-version mathcomp-algebra.version ] [
-       { cases = [ (range "8.13" "8.14") (isEq "1.12") ]; out = "1.1.0+1.12+8.13"; }
+       { cases = [ (range "8.13" "8.14") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
     ] null;

  release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@ -19,7 +19,8 @@ let
  owner = "math-comp";
  withDoc = single && (args.withDoc or false);
  defaultVersion = with versions; switch coq.coq-version [
-      { case = isGe  "8.10";        out = "1.12.0"; }
+      { case = isGe  "8.14";        out = "1.13.0"; }
+      { case = range "8.10" "8.13"; out = "1.12.0"; }
      { case = range "8.7"  "8.12"; out = "1.11.0"; }
      { case = range "8.7" "8.11";  out = "1.10.0"; }
      { case = range "8.7" "8.11";  out = "1.9.0";  }
@ -28,6 +29,7 @@ let
      { case = range "8.5" "8.7";   out = "1.6.4";  }
    ] null;
  release = {
+    "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
    "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
    "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
    "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@ -9,7 +9,7 @@ with lib; mkCoqDerivation {

  inherit version;
  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
-      { cases = [ (range "8.10" "8.14") "1.12.0" ];             out = "1.5.4"; }
+      { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ];      out = "1.5.4"; }
      { cases = [ (range "8.10" "8.12") "1.12.0" ];             out = "1.5.3"; }
      { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
      { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@ -10,7 +10,7 @@ mkCoqDerivation {

  inherit version;
  defaultVersion = with versions; switch mathcomp.character.version [
-    { case = pred.union (isGe "1.10.0") (isEq "dev"); out = "1.12.0"; }
+    { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
  ] null;

  propagatedBuildInputs = [ mathcomp.character ];
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@ -74,6 +74,7 @@ let
      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
      mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
+      mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
      metalib = callPackage ../development/coq-modules/metalib { };
      multinomials = callPackage ../development/coq-modules/multinomials {};
      odd-order = callPackage ../development/coq-modules/odd-order { };