public/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

coqPackages.mathcomp-extra: refactor

Browse Source 
- removing broken packages
- taking into account fixpoint coqPackages in mathcomp-extra-config
This commit is contained in:
Cyril Cohen 2020-05-22 04:06:06 +02:00 committed by Vincent Laporte
parent 670237ec93
commit 147aded7df
1 changed files with 15 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
pkgs/development/coq-modules/mathcomp/extra.nix
View File

@ -80,7 +80,7 @@ let
############################ ############################
rec-mathcomp-extra-config = { rec-mathcomp-extra-config = {
initial = { initial = {
mathcomp-finmap = version: { mathcomp-finmap = {version, coqPackages}: {
meta = { meta = {
description = "A finset and finmap library"; description = "A finset and finmap library";
repo = "finmap"; repo = "finmap";
@ -89,7 +89,7 @@ let
passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ]; passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ];
}; };
mathcomp-bigenough = version: { mathcomp-bigenough = {version, coqPackages}: {
meta = { meta = {
description = "A small library to do epsilon - N reasonning"; description = "A small library to do epsilon - N reasonning";
repo = "bigenough"; repo = "bigenough";
@ -98,7 +98,7 @@ let
passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
}; };
multinomials = version: { multinomials = {version, coqPackages}: {
buildInputs = [ which ]; buildInputs = [ which ];
propagatedBuildInputs = with coqPackages; propagatedBuildInputs = with coqPackages;
[ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
@ -110,7 +110,7 @@ let
passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ]; passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
}; };
mathcomp-analysis = version: { mathcomp-analysis = {version, coqPackages}: {
propagatedBuildInputs = with coqPackages; propagatedBuildInputs = with coqPackages;
[ mathcomp.field mathcomp-finmap mathcomp-bigenough ]; [ mathcomp.field mathcomp-finmap mathcomp-bigenough ];
meta = { meta = {
@ -122,9 +122,9 @@ let
passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
}; };
mathcomp-real-closed = version: { mathcomp-real-closed = {version, coqPackages}: {
propagatedBuildInputs = with coqPackages; propagatedBuildInputs = with coqPackages;
[ coq mathcomp.field mathcomp-bigenough ]; [ mathcomp.field mathcomp-bigenough ];
meta = { meta = {
description = "Mathematical Components Library on real closed fields"; description = "Mathematical Components Library on real closed fields";
repo = "real-closed"; repo = "real-closed";
@ -133,7 +133,7 @@ let
passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
}; };
coqeal = version: { coqeal = {version, coqPackages}: {
buildInputs = [ which ]; buildInputs = [ which ];
propagatedBuildInputs = with coqPackages; propagatedBuildInputs = with coqPackages;
[ mathcomp-algebra bignums paramcoq multinomials ]; [ mathcomp-algebra bignums paramcoq multinomials ];
@ -240,7 +240,7 @@ let
"1.10.0" = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";}; "1.10.0" = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";};
}; };
"8.10" = { "8.10" = {
"1.11.0+beta1" = v5; "1.11.0+beta1" = removeAttrs v5 ["coqeal"];
"1.10.0" = v4; "1.10.0" = v4;
"1.9.0" = removeAttrs v3 ["coqeal"]; "1.9.0" = removeAttrs v3 ["coqeal"];
}; };
@ -260,8 +260,8 @@ let
"8.7" = { "8.7" = {
"1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"]; "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
"1.10.0" = removeAttrs v4 ["mathcomp-analysis"]; "1.10.0" = removeAttrs v4 ["mathcomp-analysis"];
"1.9.0" = removeAttrs v3 ["coqeal"]; "1.9.0" = removeAttrs v3 ["coqeal" "mathcomp-analysis"];
"1.8.0" = removeAttrs v2 ["coqeal"]; "1.8.0" = removeAttrs v2 ["coqeal" "mathcomp-analysis"];
"1.7.0" = removeAttrs v1 ["coqeal" "multinomials"]; "1.7.0" = removeAttrs v1 ["coqeal" "multinomials"];
}; };
}; };
@ -318,13 +318,14 @@ let
rec-mathcomp-extra-override = generic: old: let rec-mathcomp-extra-override = generic: old: let
version = getVersion generic; version = getVersion generic;
package = old.meta.package or "math-comp-nix"; package = old.meta.package or "math-comp-nix";
cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {})) version) old cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {}))
{ inherit version coqPackages; }) old
// { inherit version; }; // { inherit version; };
fix = attrs: fix-attrs (pkgUp cfg attrs); fix = attrs: fix-attrs (pkgUp cfg attrs);
in in
if isFunction generic then fix (generic cfg) if isFunction generic then fix (generic cfg)
else if generic == null || generic == "" then fix {} else if generic == null || generic == "" then fix {}
else if isDerivation generic then fix generic.drvAttrs else if isDerivation generic then generic.drvAttrs
else if isAttrs generic then fix generic else if isAttrs generic then fix generic
else if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; } else if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; }
else let fixedcfg = fix cfg; in fixedcfg // ( else let fixedcfg = fix cfg; in fixedcfg // (
@ -365,7 +366,7 @@ in
mathcomp-real-closed = current-mathcomp-extra "mathcomp-real-closed"; mathcomp-real-closed = current-mathcomp-extra "mathcomp-real-closed";
coqeal = current-mathcomp-extra "coqeal"; coqeal = current-mathcomp-extra "coqeal";
mathcomp-extra-fast = map (pkg: current-mathcomp-extra pkg) mathcomp-extra-fast = map current-mathcomp-extra
(attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this)); (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this));
mathcomp-extra-all = map (pkg: current-mathcomp-extra pkg) (attrNames for-this); mathcomp-extra-all = map current-mathcomp-extra (attrNames for-this);
} }