diff options
| -rw-r--r-- | pkgs/development/coq-modules/mathcomp/default.nix | 15 | ||||
| -rw-r--r-- | pkgs/development/coq-modules/mathcomp/extra.nix | 69 | ||||
| -rw-r--r-- | pkgs/top-level/coq-packages.nix | 6 |
3 files changed, 62 insertions, 28 deletions
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index c769ab5521e8..d573eca809a2 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -3,6 +3,9 @@ }: with builtins // stdenv.lib; let + #################################### + # CONFIGURATION (please edit this) # + #################################### # sha256 of released mathcomp versions mathcomp-sha256 = { "1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; @@ -19,8 +22,16 @@ let }; # computes the default version of mathcomp given a version of Coq max-mathcomp-version = last (naturalSort (attrNames mathcomp-coq-versions)); - default-mathcomp-version = let v = last (naturalSort (["0.0.0"] - ++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions)))); + # mathcomp prefered version by decreasing order + # (the first version in the list will be tried first) + mathcomp-version-preference = [ "1.8.0" "1.9.0" "1.7.0" "1.6.1" ]; + + ############################################################## + # COMPUTED using the configuration above (edit with caution) # + ############################################################## + default-mathcomp-version = let v = head ( + filter (mc: mathcomp-coq-versions."${mc}" coq.coq-version) + mathcomp-version-preference ++ ["0.0.0"]); in if v == "0.0.0" then max-mathcomp-version else v; # list of core mathcomp packages sorted by dependency order diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix index c30ba19b75a3..0d9557623c36 100644 --- a/pkgs/development/coq-modules/mathcomp/extra.nix +++ b/pkgs/development/coq-modules/mathcomp/extra.nix @@ -1,7 +1,7 @@ -{ stdenv, fetchFromGitHub, coq, mathcomp, coqPackages, +{ stdenv, fetchFromGitHub, coq, ssreflect, coqPackages, recurseIntoAttrs }: with builtins // stdenv.lib; -let current-mathcomp = mathcomp; in +let current-ssreflect = ssreflect; in let # configuring packages param = { @@ -20,6 +20,7 @@ param = { }; multinomials = { version-sha256 = { + "1.3" = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; @@ -32,7 +33,9 @@ param = { "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd"; "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al"; }; + compatibleCoqVersions = flip elem ["8.8" "8.9"]; description = "Analysis library compatible with Mathematical Components"; + license = stdenv.lib.licenses.cecill-c; }; real-closed = { version-sha256 = { @@ -42,6 +45,15 @@ param = { }; description = "Mathematical Components Library on real closed fields"; }; + coqeal = { + version-sha256 = { + "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii"; + }; + description = "CoqEAL - The Coq Effective Algebra Library"; + owner = "CoqEAL"; + compatibleCoqVersions = flip elem ["8.7" "8.8" "8.9"]; + license = stdenv.lib.licenses.mit; + }; }; versions = { "1.9.0" = { @@ -49,13 +61,17 @@ versions = { bigenough.version = "1.0.0"; analysis = { version = "0.2.2"; - core-deps = with coqPackages; [ mathcomp_1_9-field ]; + core-deps = with coqPackages; [ mathcomp-field_1_9 ]; + extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ]; + }; + multinomials = { + version = "1.3"; + core-deps = with coqPackages; [ mathcomp-algebra_1_9 ]; 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 ]; + core-deps = with coqPackages; [ mathcomp-field_1_9 ]; extra-deps = with coqPackages; [ mathcomp_1_9-bigenough ]; }; }; @@ -64,37 +80,42 @@ versions = { bigenough.version = "1.0.0"; analysis = { version = "0.2.2"; - core-deps = with coqPackages; [ mathcomp_1_8-field ]; + core-deps = with coqPackages; [ mathcomp-field_1_8 ]; extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ]; }; multinomials = { - version = "1.2"; - core-deps = with coqPackages; [ mathcomp_1_8-algebra ]; + version = "1.3"; + core-deps = with coqPackages; [ mathcomp-algebra_1_8 ]; 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 ]; + core-deps = with coqPackages; [ mathcomp-field_1_8 ]; extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ]; }; + coqeal = { + version = "1.0.0"; + core-deps = with coqPackages; [ mathcomp-algebra_1_8 ]; + extra-deps = with coqPackages; [ bignums paramcoq mathcomp_1_8-multinomials ]; + }; }; "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 ]; + core-deps = with coqPackages; [ mathcomp-field_1_7 ]; extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ]; }; multinomials = { version = "1.1"; - core-deps = with coqPackages; [ mathcomp_1_7-algebra ]; + core-deps = with coqPackages; [ mathcomp-algebra_1_7 ]; 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 ]; + core-deps = with coqPackages; [ mathcomp-field_1_7 ]; + extra-deps = with coqPackages; [ mathcomp_1_7-bigenough ]; }; }; }; @@ -104,24 +125,25 @@ packageGen = { # optional arguments src ? "", owner ? "math-comp", - core-deps ? [ coqPackages.mathcomp-ssreflect ], extra-deps ? [], - mathcomp ? current-mathcomp, + ssreflect ? current-ssreflect, + core-deps ? null, compatibleCoqVersions ? null, - license ? mathcomp.meta.license, + license ? ssreflect.meta.license, # mandatory package, version ? "broken", version-sha256, description }: let theCompatibleCoqVersions = if compatibleCoqVersions == null - then mathcomp.compatibleCoqVersions + then ssreflect.compatibleCoqVersions else compatibleCoqVersions; + mc-core-deps = if builtins.isNull core-deps then [ssreflect] else core-deps; in { "${package}" = let from = src; in stdenv.mkDerivation rec { inherit version; - name = "coq${coq.coq-version}-mathcomp-${mathcomp.version}-${package}-${version}"; + name = "coq${coq.coq-version}-mathcomp${ssreflect.version}-${package}-${version}"; src = if from == "" then fetchFromGitHub { owner = owner; @@ -130,7 +152,7 @@ packageGen = { sha256 = version-sha256."${version}"; } else from; - propagatedBuildInputs = [ coq mathcomp ] ++ extra-deps; + propagatedBuildInputs = [ coq ] ++ mc-core-deps ++ extra-deps; installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/"; @@ -138,7 +160,7 @@ packageGen = { inherit description; inherit license; inherit (src.meta) homepage; - inherit (mathcomp.meta) platforms; + inherit (ssreflect.meta) platforms; maintainers = [ stdenv.lib.maintainers.vbgl ]; broken = (version == "broken"); }; @@ -151,14 +173,14 @@ packageGen = { }; }; -current-versions = versions."${current-mathcomp.version}" or {}; +current-versions = versions."${current-ssreflect.version}" or {}; select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate param x); for-version = v: suffix: (mapAttrs' (n: pkg: {name = "mathcomp_${suffix}-${n}"; value = (packageGen ({ - mathcomp = coqPackages."mathcomp_${suffix}"; + ssreflect = coqPackages."mathcomp-ssreflect_${suffix}"; } // pkg))."${n}";}) (select versions."${v}")); @@ -173,7 +195,8 @@ in mathcompExtraGen = packageGen; mathcomp_1_7-finmap_1_0 = (packageGen (select {finmap = {version = "1.0.0"; - mathcomp = coqPackages.mathcomp_1_7;}; + ssreflect = coqPackages.mathcomp-ssreflect_1_7;}; }).finmap).finmap; multinomials = all.mathcomp-multinomials; +coqeal = all.mathcomp-coqeal; } // all diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 524f3bf43994..8a987c6cf143 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -54,17 +54,17 @@ let 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 multinomials + mathcompExtraGen multinomials coqeal mathcomp-finmap mathcomp-bigenough mathcomp-analysis - mathcomp-multinomials mathcomp-real-closed + mathcomp-multinomials mathcomp-real-closed mathcomp-coqeal 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 mathcomp_1_8-real-closed + mathcomp_1_8-multinomials mathcomp_1_8-real-closed mathcomp_1_8-coqeal mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis mathcomp_1_9-multinomials mathcomp_1_9-real-closed; |