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

coqPackages: refactor mathcomp packages

Browse Source 
Closes #61456
wip/yesman
Cyril Cohen 5 years ago committed by Vincent Laporte
parent 4ec7a6eda9
commit b71c308591
No known key found for this signature in database
GPG Key ID: EBD582ADDDB1F81F
7 changed files with 289 additions and 192 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. 30
      pkgs/development/coq-modules/mathcomp-analysis/default.nix
  2. 29
      pkgs/development/coq-modules/mathcomp-bigenough/default.nix
  3. 40
      pkgs/development/coq-modules/mathcomp-finmap/default.nix
  4. 194
      pkgs/development/coq-modules/mathcomp/default.nix
  5. 138
      pkgs/development/coq-modules/mathcomp/extra.nix
  6. 28
      pkgs/development/coq-modules/multinomials/default.nix
  7. 22
      pkgs/top-level/coq-packages.nix

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

@ -1,30 +0,0 @@
{ stdenv, fetchFromGitHub, coq, mathcomp-bigenough, mathcomp-finmap }:
stdenv.mkDerivation rec {
version = "0.2.0";
name = "coq${coq.coq-version}-mathcomp-analysis-${version}";
src = fetchFromGitHub {
owner = "math-comp";
repo = "analysis";
rev = version;
sha256 = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
};
buildInputs = [ coq ];
propagatedBuildInputs = [ mathcomp-bigenough mathcomp-finmap ];
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = {
description = "Analysis library compatible with Mathematical Components";
inherit (src.meta) homepage;
inherit (coq.meta) platforms;
license = stdenv.lib.licenses.cecill-c;
maintainers = [ stdenv.lib.maintainers.vbgl ];
};
passthru = {
compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" ];
};
}

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

@ -1,29 +0,0 @@
{ stdenv, fetchFromGitHub, coq, mathcomp }:
stdenv.mkDerivation rec {
version = "1.0.0";
name = "coq${coq.coq-version}-mathcomp-bigenough-${version}";
src = fetchFromGitHub {
owner = "math-comp";
repo = "bigenough";
rev = version;
sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
};
buildInputs = [ coq ];
propagatedBuildInputs = [ mathcomp ];
installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = {
description = "A small library to do epsilon - N reasonning";
inherit (src.meta) homepage;
inherit (mathcomp.meta) platforms license;
maintainers = [ stdenv.lib.maintainers.vbgl ];
};
passthru = {
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
};
}

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

@ -1,40 +0,0 @@
{ stdenv, fetchFromGitHub, coq, mathcomp }:
let param =
if stdenv.lib.versionAtLeast mathcomp.version "1.8.0"
then {
version = "1.2.0";
sha256 = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
} else {
version = "1.1.0";
sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
}
; in
stdenv.mkDerivation rec {
inherit (param) version;
name = "coq${coq.coq-version}-mathcomp-finmap-${version}";
src = fetchFromGitHub {
owner = "math-comp";
repo = "finmap";
rev = version;
inherit (param) sha256;
};
buildInputs = [ coq ];
propagatedBuildInputs = [ mathcomp ];
installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = {
description = "A finset and finmap library";
inherit (src.meta) homepage;
inherit (mathcomp.meta) platforms license;
maintainers = [ stdenv.lib.maintainers.vbgl ];
};
passthru = {
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
};
}

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

@ -1,70 +1,146 @@
{ stdenv, fetchFromGitHub, coq, ncurses, which
, graphviz, withDoc ? false
{ stdenv, fetchFromGitHub, ncurses, which, graphviz, coq,
recurseIntoAttrs, withDoc ? false
}:
let param =
if stdenv.lib.versionAtLeast coq.coq-version "8.7" then
{
version = "1.8.0";
sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
}
else if stdenv.lib.versionAtLeast coq.coq-version "8.6" then
{
version = "1.7.0";
sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
}
else if stdenv.lib.versionAtLeast coq.coq-version "8.5" then
{
version = "1.6.1";
sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
}
else throw "No version of math-comp is available for Coq ${coq.coq-version}";
in
stdenv.mkDerivation rec {
name = "coq${coq.coq-version}-mathcomp-${version}";
# used in ssreflect
inherit (param) version;
src = fetchFromGitHub {
owner = "math-comp";
repo = "math-comp";
rev = "mathcomp-${param.version}";
inherit (param) sha256;
with builtins // stdenv.lib;
let
# sha256 of released mathcomp versions
mathcomp-sha256 = {
"1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
"1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
"1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
};
# versions of coq compatible with released mathcomp versions
mathcomp-coq-versions = {
"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"];
};
# computes the default version of mathcomp given a version of Coq
min-mathcomp-version = head (naturalSort (attrNames mathcomp-coq-versions));
default-mathcomp-version = last (naturalSort ([min-mathcomp-version]
++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions))));
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
# list of core mathcomp packages sorted by dependency order
mathcomp-packages =
[ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
# compute the dependencies of the core package pkg
# (assuming the total ordering above, rewrite if necessary)
mathcomp-deps = pkg: if pkg == "single" then [] else
(split (x: x == pkg) mathcomp-packages).left;
enableParallelBuilding = true;
# generic split function (TODO: move to lib?)
split = pred: l:
let loop = v: l: if l == [] then {left = v; right = [];}
else let hd = builtins.head l; tl = builtins.tail l; in
if pred hd then {left = v; right = tl;} else loop (v ++ [hd]) tl;
in loop [] l;
buildFlags = stdenv.lib.optionalString withDoc "doc";
# exported, documented at the end.
mathcompGen = mkMathcompGenFrom (_: {}) mathcomp-packages;
COQBIN = "${coq}/bin/";
# exported, documented at the end.
mathcompGenSingle = mkMathcompGen (_: {}) "single";
preBuild = ''
patchShebangs etc/utils/ssrcoqdep || true
cd mathcomp
'';
# mkMathcompGen: internal mathcomp package generator
# returns {error = ...} if impossible to generate
# returns {${mathcomp-pkg} = <derivation>} otherwise
mkMathcompGenFrom = o: l: mcv: fold (pkg: pkgs: pkgs // mkMathcompGen o pkg mcv) {} l;
mkMathcompGen = overrides: mathcomp-pkg: mathcomp-version:
let
coq-version-check = mathcomp-coq-versions.${mathcomp-version} or (_: false);
pkgpath = {single = "mathcomp";}.${mathcomp-pkg} or "mathcomp/${mathcomp-pkg}";
pkgname = {single = "mathcomp";}.${mathcomp-pkg} or "mathcomp-${mathcomp-pkg}";
pkgallMake = ''
echo "all.v" > Make
echo "-I ." >> Make
echo "-R . mathcomp.all" >> Make
'';
installPhase = ''
make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
'' + stdenv.lib.optionalString withDoc ''
make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
'';
# the base set of attributes for mathcomp
attrs = rec {
name = "coq${coq.coq-version}-${pkgname}-${mathcomp-version}";
meta = with stdenv.lib; {
homepage = http://ssr.msr-inria.inria.fr/;
license = licenses.cecill-b;
maintainers = [ maintainers.vbgl maintainers.jwiegley ];
platforms = coq.meta.platforms;
};
# used in ssreflect
version = mathcomp-version;
passthru = {
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
};
src = fetchFromGitHub {
owner = "math-comp";
repo = "math-comp";
rev = "mathcomp-${mathcomp-version}";
sha256 = mathcomp-sha256.${mathcomp-version};
};
nativeBuildInputs = optionals withDoc [ graphviz ];
buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
propagatedBuildInputs = [ coq ] ++
attrValues (mkMathcompGenFrom overrides (mathcomp-deps mathcomp-pkg) mathcomp-version);
enableParallelBuilding = true;
buildFlags = optionalString withDoc "doc";
COQBIN = "${coq}/bin/";
preBuild = ''
patchShebangs etc/utils/ssrcoqdep || true
cd ${pkgpath}
'' + optionalString (mathcomp-pkg == "all") pkgallMake;
installPhase = ''
make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
'' + optionalString withDoc ''
make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
'';
meta = with stdenv.lib; {
homepage = http://ssr.msr-inria.inria.fr/;
license = licenses.cecill-b;
maintainers = [ maintainers.vbgl maintainers.jwiegley ];
platforms = coq.meta.platforms;
};
passthru = {
compatibleCoqVersions = coq-version-check;
currentOverrides = overrides;
overrideMathcomp = moreOverrides:
(mkMathcompGen (old: let new = overrides old; in new // moreOverrides new)
mathcomp-pkg mathcomp-version).${mathcomp-pkg};
mathcompGen = moreOverrides:
(mkMathcompGenFrom (old: let new = overrides old; in new // moreOverrides new)
mathcomp-packages mathcomp-version);
};
};
in
{"${mathcomp-pkg}" = stdenv.mkDerivation (attrs // overrides attrs);};
getAttrOr = a: n: a."${n}" or (throw a.error);
mathcompCorePkgs_1_7 = mathcompGen "1.7.0";
mathcompCorePkgs_1_8 = mathcompGen "1.8.0";
mathcompCorePkgs = recurseIntoAttrs
(mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
in rec {
# mathcompGenSingle: given a version of mathcomp
# generates an attribute set {single = <drv>;} with the single mathcomp derivation
inherit mathcompGenSingle;
mathcomp_1_7_single = getAttrOr (mathcompGenSingle "1.7.0") "single";
mathcomp_1_8_single = getAttrOr (mathcompGenSingle "1.8.0") "single";
mathcomp_single = dontDistribute
(getAttrOr (mathcompGenSingle default-mathcomp-version) "single");
# mathcompGen: given a version of mathcomp
# 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;
mathcomp_1_7 = getAttrOr mathcompCorePkgs_1_7 "all";
mathcomp_1_8 = getAttrOr mathcompCorePkgs_1_8 "all";
mathcomp = getAttrOr mathcompCorePkgs "all";
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)

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

@ -0,0 +1,138 @@
{ stdenv, fetchFromGitHub, coq, mathcomp, coqPackages,
recurseIntoAttrs }:
with builtins // stdenv.lib;
let current-mathcomp = mathcomp; in
let
# configuring packages
param = {
finmap = {
version-sha256 = {
"1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
"1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
"1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
};
description = "A finset and finmap library";
};
bigenough = {
version-sha256 = {"1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";};
description = "A small library to do epsilon - N reasonning";
};
multinomials = {
version-sha256 = {
"1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
"1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
"1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
};
description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
};
analysis = {
version-sha256 = {
"0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
"0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
};
description = "Analysis library compatible with Mathematical Components";
};
};
versions = {
"1.8.0" = {
finmap.version = "1.2.0";
bigenough.version = "1.0.0";
analysis = {
version = "0.2.0";
core-deps = with coqPackages; [ mathcomp_1_8-field ];
extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
};
multinomials = {
version = "1.2";
core-deps = with coqPackages; [ mathcomp_1_8-algebra ];
extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
};
};
"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 ];
extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ];
};
multinomials = {
version = "1.1";
core-deps = with coqPackages; [ mathcomp_1_7-algebra ];
extra-deps = with coqPackages; [ mathcomp_1_7-finmap_1_0 mathcomp_1_7-bigenough ];
};
};
};
# generic package generator
packageGen = {
# optional arguments
src ? "",
owner ? "math-comp",
core-deps ? [ coqPackages.mathcomp-ssreflect ],
extra-deps ? [],
coq-versions ? ["8.6" "8.7" "8.8" "8.9"],
mathcomp ? current-mathcomp,
license ? mathcomp.meta.license,
# mandatory
package, version, version-sha256, description
}:
if version == "" then {}
else { "${package}" =
let from = src; in
stdenv.mkDerivation rec {
inherit version;
name = "coq${coq.coq-version}-mathcomp-${mathcomp.version}-${package}-${version}";
src = if from == "" then fetchFromGitHub {
owner = owner;
repo = package;
rev = version;
sha256 = version-sha256."${version}";
} else from;
propagatedBuildInputs = [ coq mathcomp ] ++ extra-deps;
installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = {
inherit description;
inherit license;
inherit (src.meta) homepage;
inherit (mathcomp.meta) platforms;
maintainers = [ stdenv.lib.maintainers.vbgl ];
};
passthru = {
inherit version-sha256;
compatibleCoqVersions = v: builtins.elem v coq-versions;
};
};};
current-versions = versions."${current-mathcomp.version}"
or (throw "no mathcomp extra packages found for mathcomp ${current-mathcomp.version}");
select = x: mapAttrs (n: pkg: {package = n;} // pkg)
(recursiveUpdate (overrideExisting x 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")) //
(recurseIntoAttrs (mapDerivationAttrset dontDistribute (
mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg)."${n}";})
(select current-versions))));
in
{
mathcompExtraGen = packageGen;
mathcomp_1_7-finmap_1_0 =
(packageGen (select {finmap = {version = "1.0.0";
mathcomp = coqPackages.mathcomp_1_7;};
}).finmap).finmap;
multinomials = all.mathcomp-multinomials;
} // all

28
pkgs/development/coq-modules/multinomials/default.nix
Unescape View File

@ -1,28 +0,0 @@
{ stdenv, fetchFromGitHub, coq, mathcomp }:
stdenv.mkDerivation rec {
name = "coq${coq.coq-version}-multinomials-${version}";
version = "1.0";
src = fetchFromGitHub {
owner = "math-comp";
repo = "multinomials";
rev = version;
sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
};
buildInputs = [ coq ];
propagatedBuildInputs = [ mathcomp ];
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
meta = {
description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
inherit (src.meta) homepage;
license = stdenv.lib.licenses.cecill-b;
inherit (coq.meta) platforms;
};
passthru = {
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
};
}

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

@ -34,17 +34,27 @@ let
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
iris = callPackage ../development/coq-modules/iris {};
math-classes = callPackage ../development/coq-modules/math-classes { };
mathcomp = callPackage ../development/coq-modules/mathcomp { };
mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { };
mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };
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;
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
mathcomp_1_7-finmap_1_0
mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis mathcomp_1_8-multinomials
multinomials;
metalib = callPackage ../development/coq-modules/metalib { };
multinomials = callPackage ../development/coq-modules/multinomials {};
paco = callPackage ../development/coq-modules/paco {};
paramcoq = callPackage ../development/coq-modules/paramcoq {};
QuickChick = callPackage ../development/coq-modules/QuickChick {};
simple-io = callPackage ../development/coq-modules/simple-io { };
ssreflect = callPackage ../development/coq-modules/ssreflect { };
stdpp = callPackage ../development/coq-modules/stdpp { };
StructTact = callPackage ../development/coq-modules/StructTact {};
tlc = callPackage ../development/coq-modules/tlc {};

Write Preview
Loading…
Cancel
Save