Something went wrong. Try again.
What happens if I push all of nixpkgs
Something went wrong. Try again.
8.0 kB · 231 lines
Nix
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232{ lib, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, hierarchy-builder, stdlib, single ? false, coqPackages, coq, version ? null,}@args:
let repo = "analysis"; owner = "math-comp";
release."1.12.0".sha256 = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo="; release."1.11.0".sha256 = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc="; release."1.9.0".sha256 = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g="; release."1.8.0".sha256 = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc="; release."1.7.0".sha256 = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ="; release."1.5.0".sha256 = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88="; release."1.4.0".sha256 = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg="; release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo="; release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o="; release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4="; release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60="; release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA="; release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y="; release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E="; release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0="; release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg="; release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k="; release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw"; release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68"; release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
defaultVersion = let case = coq: mc: out: { cases = [ coq mc ]; inherit out; }; in with lib.versions; lib.switch [ coq.coq-version mathcomp.version ] [ (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0") (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0") (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0") (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0") (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7") (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6") (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5") (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1") (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2") (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1") (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13") (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10") (case (range "8.10" "8.12") "1.11.0" "0.3.3") (case (range "8.10" "8.11") "1.11.0" "0.3.1") (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3") ] null;
# list of analysis packages sorted by dependency order packages = { "classical" = [ ]; "reals" = [ "classical" ]; "experimental-reals" = [ "reals" ]; "analysis" = [ "reals" ]; "reals-stdlib" = [ "reals" ]; "analysis-stdlib" = [ "analysis" "reals-stdlib" ]; };
mathcomp_ = package: let classical-deps = [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap ]; experimental-reals-deps = [ mathcomp-bigenough ]; analysis-deps = [ mathcomp.field mathcomp-bigenough ]; intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package}); pkgpath = lib.switch package [ { case = "single"; out = "."; } { case = "analysis"; out = "theories"; } { case = "experimental-reals"; out = "experimental_reals"; } { case = "reals-stdlib"; out = "reals_stdlib"; } { case = "analysis-stdlib"; out = "analysis_stdlib"; } ] package; pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}"; derivation = mkCoqDerivation ({ inherit version pname defaultVersion release repo owner ;
namePrefix = [ "coq" "mathcomp" ];
propagatedBuildInputs = intra-deps ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps ++ lib.optionals (lib.elem package [ "experimental-reals" "single" ]) experimental-reals-deps ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps ++ lib.optional (lib.elem package [ "reals-stdlib" "analysis-stdlib" "single" ]) stdlib;
preBuild = '' cd ${pkgpath} '';
meta = { description = "Analysis library compatible with Mathematical Components"; maintainers = [ lib.maintainers.cohencyril ]; license = lib.licenses.cecill-c; };
passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages; }); # split packages didn't exist before 0.6, so building nothing in that case patched-derivation1 = derivation.overrideAttrs ( o: lib.optionalAttrs ( o.pname != null && o.pname != "mathcomp-analysis" && o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version ) { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } ); patched-derivation2 = patched-derivation1.overrideAttrs ( o: lib.optionalAttrs ( o.pname != null && o.pname == "mathcomp-analysis" && o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version ) { preBuild = ""; } ); # only packages classical and analysis existed before 1.7, so building nothing in that case patched-derivation3 = patched-derivation2.overrideAttrs ( o: lib.optionalAttrs ( o.pname != null && o.pname != "mathcomp-classical" && o.pname != "mathcomp-analysis" && o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version ) { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } ); patched-derivation = patched-derivation3.overrideAttrs ( o: lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) { propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; } ); in patched-derivation;inmathcomp_ (if single then "single" else "analysis")