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

coqPackages.mathcomp: 1.8.0 -> 1.9.0 and adding real-closed

Browse Source
This commit is contained in:
Cyril Cohen 2019-05-23 15:45:28 +02:00 committed by Vincent Laporte
parent ddaf94d804
commit 547466064e
No known key found for this signature in database
GPG Key ID: EBD582ADDDB1F81F
3 changed files with 104 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
pkgs/development/coq-modules/mathcomp/default.nix
View File

@ -5,12 +5,14 @@ with builtins // stdenv.lib;
let
# sha256 of released mathcomp versions
mathcomp-sha256 = {
"1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
"1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
"1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
"1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
};
# versions of coq compatible with released mathcomp versions
mathcomp-coq-versions = {
"1.9.0" = flip elem ["8.7" "8.8" "8.9" "8.10"];
"1.8.0" = flip elem ["8.7" "8.8" "8.9"];
"1.7.0" = flip elem ["8.6" "8.7" "8.8" "8.9"];
"1.6.1" = flip elem ["8.5"];
@ -56,20 +58,22 @@ let
echo "-I ." >> Make
echo "-R . mathcomp.all" >> Make
'';
is-released = builtins.isString mathcomp-version;
custom-version = if is-released then mathcomp-version else "custom";
# the base set of attributes for mathcomp
attrs = rec {
name = "coq${coq.coq-version}-${pkgname}-${mathcomp-version}";
name = "coq${coq.coq-version}-${pkgname}-${custom-version}";
# used in ssreflect
version = mathcomp-version;
version = custom-version;
src = fetchFromGitHub {
src = if is-released then fetchFromGitHub {
owner = "math-comp";
repo = "math-comp";
rev = "mathcomp-${mathcomp-version}";
sha256 = mathcomp-sha256.${mathcomp-version};
};
} else mathcomp-version;
nativeBuildInputs = optionals withDoc [ graphviz ];
buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
@ -117,6 +121,7 @@ getAttrOr = a: n: a."${n}" or (throw a.error);
mathcompCorePkgs_1_7 = mathcompGen "1.7.0";
mathcompCorePkgs_1_8 = mathcompGen "1.8.0";
mathcompCorePkgs_1_9 = mathcompGen "1.9.0";
mathcompCorePkgs = recurseIntoAttrs
(mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
@ -126,6 +131,7 @@ in rec {
inherit mathcompGenSingle;
mathcomp_1_7_single = getAttrOr (mathcompGenSingle "1.7.0") "single";
mathcomp_1_8_single = getAttrOr (mathcompGenSingle "1.8.0") "single";
mathcomp_1_9_single = getAttrOr (mathcompGenSingle "1.9.0") "single";
mathcomp_single = dontDistribute
(getAttrOr (mathcompGenSingle default-mathcomp-version) "single");
@ -133,15 +139,19 @@ mathcomp_single = dontDistribute
# generates an attribute set {ssreflect = <drv>; ... character = <drv>; all = <drv>;}.
# each of these have a special attribute overrideMathcomp which
# must be used instead of overrideAttrs in order to also fix the dependencies
inherit mathcompGen mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs;
inherit mathcompGen mathcompCorePkgs
mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs_1_9;
mathcomp = getAttrOr mathcompCorePkgs "all";
mathcomp_1_7 = getAttrOr mathcompCorePkgs_1_7 "all";
mathcomp_1_8 = getAttrOr mathcompCorePkgs_1_8 "all";
mathcomp = getAttrOr mathcompCorePkgs "all";
mathcomp_1_9 = getAttrOr mathcompCorePkgs_1_9 "all";
ssreflect = getAttrOr mathcompCorePkgs "ssreflect";
ssreflect = getAttrOr mathcompCorePkgs "ssreflect";
} //
(mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = pkg;}) mathcompCorePkgs) //
(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_7"; value = pkg;}) mathcompCorePkgs_1_7) //
(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_8"; value = pkg;}) mathcompCorePkgs_1_8)
(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_8"; value = pkg;}) mathcompCorePkgs_1_8) //
(mapAttrs' (n: pkg: {name = "mathcomp-${n}_1_9"; value = pkg;}) mathcompCorePkgs_1_9)

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

@ -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.8.0" = {
finmap.version = "1.2.0";
"1.9.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_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.1";
bigenough.version = "1.0.0";
analysis = {
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))));

43
pkgs/top-level/coq-packages.nix
View File

@ -36,21 +36,38 @@ let
ltac2 = callPackage ../development/coq-modules/ltac2 {};
math-classes = callPackage ../development/coq-modules/math-classes { };
inherit (callPackage ../development/coq-modules/mathcomp { })
mathcompGen mathcompGenSingle mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs
mathcomp mathcomp_1_7 mathcomp_1_8 ssreflect
mathcomp-ssreflect mathcomp-ssreflect_1_7 mathcomp-ssreflect_1_8
mathcomp-fingroup mathcomp-fingroup_1_7 mathcomp-fingroup_1_8
mathcomp-algebra mathcomp-algebra_1_7 mathcomp-algebra_1_8
mathcomp-solvable mathcomp-solvable_1_7 mathcomp-solvable_1_8
mathcomp-field mathcomp-field_1_7 mathcomp-field_1_8
mathcomp-character mathcomp-character_1_7 mathcomp-character_1_8;
mathcompGen mathcompGenSingle ssreflect
mathcompCorePkgs mathcomp
mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra
mathcomp-solvable mathcomp-field mathcomp-character
mathcompCorePkgs_1_7 mathcomp_1_7
mathcomp-ssreflect_1_7 mathcomp-fingroup_1_7 mathcomp-algebra_1_7
mathcomp-solvable_1_7 mathcomp-field_1_7 mathcomp-character_1_7
mathcompCorePkgs_1_8 mathcomp_1_8
mathcomp-ssreflect_1_8 mathcomp-fingroup_1_8 mathcomp-algebra_1_8
mathcomp-solvable_1_8 mathcomp-field_1_8 mathcomp-character_1_8
mathcompCorePkgs_1_9 mathcomp_1_9
mathcomp-ssreflect_1_9 mathcomp-fingroup_1_9 mathcomp-algebra_1_9
mathcomp-solvable_1_9 mathcomp-field_1_9 mathcomp-character_1_9;
inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
mathcompExtraGen
mathcomp-finmap mathcomp-bigenough mathcomp-analysis mathcomp-multinomials
mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis mathcomp_1_7-multinomials
mathcompExtraGen multinomials
mathcomp-finmap mathcomp-bigenough mathcomp-analysis
mathcomp-multinomials mathcomp-real-closed
mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis
mathcomp_1_7-multinomials mathcomp_1_7-real-closed
mathcomp_1_7-finmap_1_0
mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis mathcomp_1_8-multinomials
multinomials;
mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis
mathcomp_1_8-multinomials mathcomp_1_8-real-closed
mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
mathcomp_1_9-multinomials mathcomp_1_9-real-closed;
metalib = callPackage ../development/coq-modules/metalib { };
paco = callPackage ../development/coq-modules/paco {};
paramcoq = callPackage ../development/coq-modules/paramcoq {};