diff options
author | Cyril Cohen <cohen@crans.org> | 2019-04-09 19:21:57 +0200 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2019-05-15 14:11:21 +0000 |
commit | b71c308591e1bfc3708c31dc1a94fcae636b5557 (patch) | |
tree | 64383399a44c1ffb465a91c6d46c9407cbfaa422 /pkgs/development/coq-modules/mathcomp/extra.nix | |
parent | 4ec7a6eda993986a2e0e00c999e92e290e9dccac (diff) | |
download | nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar.gz nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar.bz2 nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar.lz nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar.xz nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.tar.zst nixpkgs-b71c308591e1bfc3708c31dc1a94fcae636b5557.zip |
coqPackages: refactor mathcomp packages
Closes #61456
Diffstat (limited to 'pkgs/development/coq-modules/mathcomp/extra.nix')
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/extra.nix | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix new file mode 100644 index 00000000000..ef387985e06 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp/extra.nix @@ -0,0 +1,138 @@ +{ stdenv, fetchFromGitHub, coq, mathcomp, coqPackages, + recurseIntoAttrs }: +with builtins // stdenv.lib; +let current-mathcomp = mathcomp; in +let +# configuring packages +param = { + finmap = { + version-sha256 = { + "1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4"; + "1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a"; + "1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; + }; + description = "A finset and finmap library"; + }; + bigenough = { + version-sha256 = {"1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";}; + description = "A small library to do epsilon - N reasonning"; + }; + multinomials = { + version-sha256 = { + "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; + }; + description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + }; + analysis = { + version-sha256 = { + "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd"; + "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al"; + }; + description = "Analysis library compatible with Mathematical Components"; + }; +}; +versions = { + "1.8.0" = { + finmap.version = "1.2.0"; + bigenough.version = "1.0.0"; + analysis = { + version = "0.2.0"; + core-deps = with coqPackages; [ mathcomp_1_8-field ]; + extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ]; + }; + multinomials = { + version = "1.2"; + core-deps = with coqPackages; [ mathcomp_1_8-algebra ]; + extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ]; + }; + }; + "1.7.0" = { + finmap.version = "1.1.0"; + bigenough.version = "1.0.0"; + analysis = { + version = "0.1.0"; + core-deps = with coqPackages; [ mathcomp_1_7-field ]; + extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ]; + }; + multinomials = { + version = "1.1"; + core-deps = with coqPackages; [ mathcomp_1_7-algebra ]; + extra-deps = with coqPackages; [ mathcomp_1_7-finmap_1_0 mathcomp_1_7-bigenough ]; + }; + }; +}; + +# generic package generator +packageGen = { + # optional arguments + src ? "", + owner ? "math-comp", + core-deps ? [ coqPackages.mathcomp-ssreflect ], + extra-deps ? [], + coq-versions ? ["8.6" "8.7" "8.8" "8.9"], + mathcomp ? current-mathcomp, + license ? mathcomp.meta.license, + # mandatory + package, version, version-sha256, description + }: + if version == "" then {} + else { "${package}" = + let from = src; in + + stdenv.mkDerivation rec { + inherit version; + name = "coq${coq.coq-version}-mathcomp-${mathcomp.version}-${package}-${version}"; + + src = if from == "" then fetchFromGitHub { + owner = owner; + repo = package; + rev = version; + sha256 = version-sha256."${version}"; + } else from; + + propagatedBuildInputs = [ coq mathcomp ] ++ extra-deps; + + installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + meta = { + inherit description; + inherit license; + inherit (src.meta) homepage; + inherit (mathcomp.meta) platforms; + maintainers = [ stdenv.lib.maintainers.vbgl ]; + }; + + passthru = { + inherit version-sha256; + compatibleCoqVersions = v: builtins.elem v coq-versions; + }; + };}; + +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 (overrideExisting x param) x); + +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")) // + (recurseIntoAttrs (mapDerivationAttrset dontDistribute ( + mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg)."${n}";}) + (select current-versions)))); +in +{ +mathcompExtraGen = packageGen; +mathcomp_1_7-finmap_1_0 = + (packageGen (select {finmap = {version = "1.0.0"; + mathcomp = coqPackages.mathcomp_1_7;}; + }).finmap).finmap; +multinomials = all.mathcomp-multinomials; +} // all |