mirrors/nixpkgs
1
0
Fork 1
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-11-18 19:51:17 +00:00
Code Issues Wiki Activity

coqPackages.mathcomp: avoid top-level with ...;

Browse source
This commit is contained in:
Philip Taron 2024-03-14 14:51:49 -07:00
parent 9ab423efec
commit 94112e3ae5
No known key found for this signature in database
1 changed files with 21 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
pkgs/development/coq-modules/mathcomp/default.nix
View file

@ -11,14 +11,15 @@
############################################################################
{ lib, ncurses, graphviz, lua, fetchzip,
mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
mkCoqDerivation, withDoc ? false, single ? false,
coqPackages, coq, hierarchy-builder, version ? null }@args:
with builtins // lib;
let
repo = "math-comp";
owner = "math-comp";
withDoc = single && (args.withDoc or false);
defaultVersion = with versions; lib.switch coq.coq-version [
defaultVersion = let inherit (lib.versions) range; in
lib.switch coq.coq-version [
{ case = range "8.19" "8.19"; out = "1.19.0"; }
{ case = range "8.17" "8.18"; out = "1.18.0"; }
{ case = range "8.15" "8.18"; out = "1.17.0"; }
@ -63,7 +64,7 @@ let
packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
mathcomp_ = package: let
mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages)));
mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
pkgallMake = ''
@ -74,12 +75,12 @@ let
derivation = mkCoqDerivation ({
inherit version pname defaultVersion release releaseRev repo owner;
mlPlugin = versions.isLe "8.6" coq.coq-version;
nativeBuildInputs = optionals withDoc [ graphviz lua ];
mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
buildInputs = [ ncurses ];
propagatedBuildInputs = mathcomp-deps;
buildFlags = optional withDoc "doc";
buildFlags = lib.optional withDoc "doc";
preBuild = ''
if [[ -f etc/utils/ssrcoqdep ]]
@ -90,16 +91,16 @@ let
fi
'' + ''
cd ${pkgpath}
'' + optionalString (package == "all") pkgallMake;
'' + lib.optionalString (package == "all") pkgallMake;
meta = {
homepage = "https://math-comp.github.io/";
license = licenses.cecill-b;
maintainers = with maintainers; [ vbgl jwiegley cohencyril ];
license = lib.licenses.cecill-b;
maintainers = with lib.maintainers; [ vbgl jwiegley cohencyril ];
};
} // optionalAttrs (package != "single")
{ passthru = genAttrs packages mathcomp_; }
// optionalAttrs withDoc {
} // lib.optionalAttrs (package != "single")
{ passthru = lib.genAttrs packages mathcomp_; }
// lib.optionalAttrs withDoc {
htmldoc_template =
fetchzip {
url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
@ -111,7 +112,7 @@ let
'';
postInstall =
let tgt = "$out/share/coq/${coq.coq-version}/"; in
optionalString withDoc ''
lib.optionalString withDoc ''
mkdir -p ${tgt}
cp -r htmldoc ${tgt}
cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
@ -120,20 +121,20 @@ let
extraInstallFlags = [ "-f Makefile.coq" ];
});
patched-derivation1 = derivation.overrideAttrs (o:
optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
o.version != null && o.version != "dev" && versions.isLt "1.7" o.version)
lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version)
{ preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
);
patched-derivation2 = patched-derivation1.overrideAttrs (o:
optionalAttrs (versions.isLe "8.7" coq.coq-version ||
(o.version != "dev" && versions.isLe "1.7" o.version))
lib.optionalAttrs (lib.versions.isLe "8.7" coq.coq-version ||
(o.version != "dev" && lib.versions.isLe "1.7" o.version))
{
installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
}
);
patched-derivation = patched-derivation2.overrideAttrs (o:
optionalAttrs (o.version != null
&& (o.version == "dev" || versions.isGe "2.0.0" o.version))
lib.optionalAttrs (o.version != null
&& (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
{
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
}