diff options
Diffstat (limited to 'pkgs/development/coq-modules/mathcomp/extra.nix')
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/extra.nix | 68 |
1 files changed, 55 insertions, 13 deletions
diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix index 3666d54a7869..c30ba19b75a3 100644 --- a/pkgs/development/coq-modules/mathcomp/extra.nix +++ b/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,12 +106,17 @@ 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 ? "broken", version-sha256, description }: + let + theCompatibleCoqVersions = if compatibleCoqVersions == null + then mathcomp.compatibleCoqVersions + else compatibleCoqVersions; + in { "${package}" = let from = src; in stdenv.mkDerivation rec { @@ -105,8 +145,8 @@ packageGen = { passthru = { inherit version-sha256; - compatibleCoqVersions = if meta.broken then _: false else - v: builtins.elem v coq-versions; + compatibleCoqVersions = if meta.broken then _: false + else theCompatibleCoqVersions; }; }; }; @@ -115,14 +155,16 @@ current-versions = versions."${current-mathcomp.version}" or {}; select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate 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")) // +for-version = v: suffix: (mapAttrs' (n: pkg: + {name = "mathcomp_${suffix}-${n}"; + value = (packageGen ({ + mathcomp = coqPackages."mathcomp_${suffix}"; + } // pkg))."${n}";}) + (select versions."${v}")); + +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)))); |