From b71c308591e1bfc3708c31dc1a94fcae636b5557 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 9 Apr 2019 19:21:57 +0200 Subject: coqPackages: refactor mathcomp packages Closes #61456 --- .../coq-modules/mathcomp-analysis/default.nix | 30 ---- .../coq-modules/mathcomp-bigenough/default.nix | 29 --- .../coq-modules/mathcomp-finmap/default.nix | 40 ----- pkgs/development/coq-modules/mathcomp/default.nix | 194 ++++++++++++++------- pkgs/development/coq-modules/mathcomp/extra.nix | 138 +++++++++++++++ .../coq-modules/multinomials/default.nix | 28 --- 6 files changed, 273 insertions(+), 186 deletions(-) delete mode 100644 pkgs/development/coq-modules/mathcomp-analysis/default.nix delete mode 100644 pkgs/development/coq-modules/mathcomp-bigenough/default.nix delete mode 100644 pkgs/development/coq-modules/mathcomp-finmap/default.nix create mode 100644 pkgs/development/coq-modules/mathcomp/extra.nix delete mode 100644 pkgs/development/coq-modules/multinomials/default.nix (limited to 'pkgs/development/coq-modules') diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix deleted file mode 100644 index 8c315371229..00000000000 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ /dev/null @@ -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" ]; - }; -} diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix deleted file mode 100644 index e1f58edc9cb..00000000000 --- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix +++ /dev/null @@ -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" ]; - }; -} diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix deleted file mode 100644 index c36b72711ff..00000000000 --- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix +++ /dev/null @@ -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" ]; - }; -} diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 85678a4c6a9..aa6da1a1e28 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -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} = } 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 = ;} 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 = ; ... character = ; all = ;}. +# 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) diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix new file mode 100644 index 00000000000..ef387985e06 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp/extra.nix @@ -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 diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix deleted file mode 100644 index aa22c96256f..00000000000 --- a/pkgs/development/coq-modules/multinomials/default.nix +++ /dev/null @@ -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" ]; - }; -} -- cgit 1.4.1