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

   1 {
   2   lib,
   3   mkCoqDerivation,
   4   mathcomp,
   5   mathcomp-finmap,
   6   mathcomp-bigenough,
   7   hierarchy-builder,
   8   single ? false,
   9   coqPackages,
  10   coq,
  11   version ? null,
  12 }@args:
  13
  14 let
  15   repo = "analysis";
  16   owner = "math-comp";
  17
  18   release."1.7.0".sha256 = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ=";
  19   release."1.5.0".sha256 = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
  20   release."1.4.0".sha256 = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
  21   release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
  22   release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
  23   release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
  24   release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
  25   release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
  26   release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
  27   release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
  28   release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
  29   release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
  30   release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
  31   release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
  32   release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
  33   release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
  34   release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
  35   release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
  36   release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
  37   release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
  38   release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
  39   release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
  40   release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
  41
  42   defaultVersion =
  43     let
  44       inherit (lib.versions) range;
  45     in
  46     lib.switch
  47       [ coq.version mathcomp.version ]
  48       [
  49         {
  50           cases = [
  51             (range "8.19" "8.20")
  52             (range "2.1.0" "2.2.0")
  53           ];
  54           out = "1.7.0";
  55         }
  56         {
  57           cases = [
  58             (range "8.17" "8.20")
  59             (range "2.0.0" "2.2.0")
  60           ];
  61           out = "1.1.0";
  62         }
  63         {
  64           cases = [
  65             (range "8.17" "8.19")
  66             (range "1.17.0" "1.19.0")
  67           ];
  68           out = "0.7.0";
  69         }
  70         {
  71           cases = [
  72             (range "8.17" "8.18")
  73             (range "1.15.0" "1.18.0")
  74           ];
  75           out = "0.6.7";
  76         }
  77         {
  78           cases = [
  79             (range "8.17" "8.18")
  80             (range "1.15.0" "1.18.0")
  81           ];
  82           out = "0.6.6";
  83         }
  84         {
  85           cases = [
  86             (range "8.14" "8.18")
  87             (range "1.15.0" "1.17.0")
  88           ];
  89           out = "0.6.5";
  90         }
  91         {
  92           cases = [
  93             (range "8.14" "8.18")
  94             (range "1.13.0" "1.16.0")
  95           ];
  96           out = "0.6.1";
  97         }
  98         {
  99           cases = [
 100             (range "8.14" "8.18")
 101             (range "1.13" "1.15")
 102           ];
 103           out = "0.5.2";
 104         }
 105         {
 106           cases = [
 107             (range "8.13" "8.15")
 108             (range "1.13" "1.14")
 109           ];
 110           out = "0.5.1";
 111         }
 112         {
 113           cases = [
 114             (range "8.13" "8.15")
 115             (range "1.12" "1.14")
 116           ];
 117           out = "0.3.13";
 118         }
 119         {
 120           cases = [
 121             (range "8.11" "8.14")
 122             (range "1.12" "1.13")
 123           ];
 124           out = "0.3.10";
 125         }
 126         {
 127           cases = [
 128             (range "8.10" "8.12")
 129             "1.11.0"
 130           ];
 131           out = "0.3.3";
 132         }
 133         {
 134           cases = [
 135             (range "8.10" "8.11")
 136             "1.11.0"
 137           ];
 138           out = "0.3.1";
 139         }
 140         {
 141           cases = [
 142             (range "8.8" "8.11")
 143             (range "1.8" "1.10")
 144           ];
 145           out = "0.2.3";
 146         }
 147       ]
 148       null;
 149
 150   # list of analysis packages sorted by dependency order
 151   packages = {
 152     "classical" = [ ];
 153     "reals" = [ "classical" ];
 154     "experimental-reals" = [ "reals" ];
 155     "analysis" = [ "reals" ];
 156     "reals-stdlib" = [ "reals" ];
 157     "analysis-stdlib" = [
 158       "analysis"
 159       "reals-stdlib"
 160     ];
 161   };
 162
 163   mathcomp_ =
 164     package:
 165     let
 166       classical-deps = [
 167         mathcomp.algebra
 168         mathcomp-finmap
 169       ];
 170       experimental-reals-deps = [ mathcomp-bigenough ];
 171       analysis-deps = [
 172         mathcomp.field
 173         mathcomp-bigenough
 174       ];
 175       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
 176       pkgpath = lib.switch package [
 177         {
 178           case = "single";
 179           out = ".";
 180         }
 181         {
 182           case = "analysis";
 183           out = "theories";
 184         }
 185         {
 186           case = "experimental-reals";
 187           out = "experimental_reals";
 188         }
 189         {
 190           case = "reals-stdlib";
 191           out = "reals_stdlib";
 192         }
 193         {
 194           case = "analysis-stdlib";
 195           out = "analysis_stdlib";
 196         }
 197       ] package;
 198       pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
 199       derivation = mkCoqDerivation ({
 200         inherit
 201           version
 202           pname
 203           defaultVersion
 204           release
 205           repo
 206           owner
 207           ;
 208
 209         namePrefix = [
 210           "coq"
 211           "mathcomp"
 212         ];
 213
 214         propagatedBuildInputs =
 215           intra-deps
 216           ++ lib.optionals (lib.elem package [
 217             "classical"
 218             "single"
 219           ]) classical-deps
 220           ++ lib.optionals (lib.elem package [
 221             "experimental-reals"
 222             "single"
 223           ]) experimental-reals-deps
 224           ++ lib.optionals (lib.elem package [
 225             "analysis"
 226             "single"
 227           ]) analysis-deps;
 228
 229         preBuild = ''
 230           cd ${pkgpath}
 231         '';
 232
 233         meta = {
 234           description = "Analysis library compatible with Mathematical Components";
 235           maintainers = [ lib.maintainers.cohencyril ];
 236           license = lib.licenses.cecill-c;
 237         };
 238
 239         passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
 240       });
 241       # split packages didn't exist before 0.6, so bulding nothing in that case
 242       patched-derivation1 = derivation.overrideAttrs (
 243         o:
 244         lib.optionalAttrs
 245           (
 246             o.pname != null
 247             && o.pname != "mathcomp-analysis"
 248             && o.version != null
 249             && o.version != "dev"
 250             && lib.versions.isLt "0.6" o.version
 251           )
 252           {
 253             preBuild = "";
 254             buildPhase = "echo doing nothing";
 255             installPhase = "echo doing nothing";
 256           }
 257       );
 258       patched-derivation2 = patched-derivation1.overrideAttrs (
 259         o:
 260         lib.optionalAttrs (
 261           o.pname != null
 262           && o.pname == "mathcomp-analysis"
 263           && o.version != null
 264           && o.version != "dev"
 265           && lib.versions.isLt "0.6" o.version
 266         ) { preBuild = ""; }
 267       );
 268       # only packages classical and analysis existed before 1.7, so bulding nothing in that case
 269       patched-derivation3 = patched-derivation2.overrideAttrs (
 270         o:
 271         lib.optionalAttrs
 272           (
 273             o.pname != null
 274             && o.pname != "mathcomp-classical"
 275             && o.pname != "mathcomp-analysis"
 276             && o.version != null
 277             && o.version != "dev"
 278             && lib.versions.isLt "1.7" o.version
 279           )
 280           {
 281             preBuild = "";
 282             buildPhase = "echo doing nothing";
 283             installPhase = "echo doing nothing";
 284           }
 285       );
 286       patched-derivation = patched-derivation3.overrideAttrs (
 287         o:
 288         lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
 289           {
 290             propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
 291           }
 292       );
 293     in
 294     patched-derivation;
 295 in
 296 mathcomp_ (if single then "single" else "analysis")