kookie
/
nomicon
1
0
Fork 0
Code Issues Projects Releases 1 Activity

coqPackages: fix + add multinomials 1.3 + coqeal 1.0.0

Browse Source
wip/yesman
Cyril Cohen 5 years ago committed by Vincent Laporte
parent 1556781737
commit d80148928b
3 changed files with 62 additions and 28 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 15
      pkgs/development/coq-modules/mathcomp/default.nix
  2. 69
      pkgs/development/coq-modules/mathcomp/extra.nix
  3. 6
      pkgs/top-level/coq-packages.nix

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

@ -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

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

@ -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

6
pkgs/top-level/coq-packages.nix
Unescape View File

@ -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;

Write Preview
Loading…
Cancel
Save