diff options
author | Pierre Roux <pierre.roux@onera.fr> | 2022-09-27 11:37:48 +0200 |
---|---|---|
committer | Vincent Laporte <vbgl@users.noreply.github.com> | 2022-10-11 11:46:46 +0200 |
commit | c8aa29813493163ffd7e878f2816fcf2df276483 (patch) | |
tree | 00a46f2d7c70ee49173332228370b8f2d7e1daae /pkgs/development/coq-modules | |
parent | 010f1b2138083df969a1f0e4eafe3cd1dd0d71e9 (diff) |
Adding mathcomp-analysis single
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/mathcomp-analysis/default.nix | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 99c760fce0cec..a42b551d18450 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -1,7 +1,8 @@ { lib, mkCoqDerivation, recurseIntoAttrs, - mathcomp, mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed, + mathcomp, mathcomp-finmap, mathcomp-bigenough, hierarchy-builder, + single ? false, coqPackages, coq, version ? null }@args: with builtins // lib; let @@ -36,20 +37,23 @@ let packages = [ "classical" "analysis" ]; mathcomp_ = package: let - analysis-deps = map mathcomp_ (head (splitList (pred.equal package) packages)); - pkgpath = if package == "analysis" then "theories" else "${package}"; - pname = "mathcomp-${package}"; + classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ]; + analysis-deps = [ mathcomp.field mathcomp-bigenough ]; + intra-deps = if package == "single" then [] + else map mathcomp_ (head (splitList (pred.equal package) packages)); + pkgpath = if package == "single" then "." + else if package == "analysis" then "theories" else "${package}"; + pname = if package == "single" then "mathcomp-analysis-single" + else "mathcomp-${package}"; derivation = mkCoqDerivation ({ inherit version pname defaultVersion release repo owner; namePrefix = [ "coq" "mathcomp" ]; propagatedBuildInputs = - (if package == "classical" then - [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap ] - else - [ mathcomp.field mathcomp-bigenough mathcomp-real-closed ]) - ++ [ analysis-deps ]; + intra-deps + ++ optionals (elem package [ "classical" "single" ]) classical-deps + ++ optionals (elem package [ "analysis" "single" ]) analysis-deps; preBuild = '' cd ${pkgpath} @@ -83,4 +87,4 @@ let ); in patched-derivation; in -mathcomp_ "analysis" +mathcomp_ (if single then "single" else "analysis") |