public/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

several fixes in coq and coqPackages.mathcomp (and extras)

Browse Source
This commit is contained in:
Cyril Cohen 2019-05-20 11:38:26 +02:00 committed by Vincent Laporte
parent 3efd90e3c9
commit d16a78b512
3 changed files with 13 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
pkgs/applications/science/logic/coq/default.nix
View File

@ -29,10 +29,7 @@ let
"8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
"8.10+beta1" = "19wf39i0ap2vakglgdlqxpjd3l1h5w7dp460w8y7nc1y06b2153h"; "8.10+beta1" = "19wf39i0ap2vakglgdlqxpjd3l1h5w7dp460w8y7nc1y06b2153h";
}."${version}"; }."${version}";
coq-version = coq-version = stdenv.lib.versions.majorMinor version;
let inherit (builtins) concatStringsSep head map; in
let inherit (stdenv.lib) take splitString; in
concatStringsSep "." (take 2 (map head (map (splitString "pl") (splitString "." version))));
versionAtLeast = stdenv.lib.versionAtLeast coq-version; versionAtLeast = stdenv.lib.versionAtLeast coq-version;
ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10") ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10")
"-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt"; "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";

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

@ -16,9 +16,10 @@ let
"1.6.1" = flip elem ["8.5"]; "1.6.1" = flip elem ["8.5"];
}; };
# computes the default version of mathcomp given a version of Coq # computes the default version of mathcomp given a version of Coq
min-mathcomp-version = head (naturalSort (attrNames mathcomp-coq-versions)); max-mathcomp-version = last (naturalSort (attrNames mathcomp-coq-versions));
default-mathcomp-version = last (naturalSort ([min-mathcomp-version] default-mathcomp-version = let v = last (naturalSort (["0.0.0"]
++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions)))); ++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions))));
in if v == "0.0.0" then max-mathcomp-version else v;
# list of core mathcomp packages sorted by dependency order # list of core mathcomp packages sorted by dependency order
mathcomp-packages = mathcomp-packages =

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

@ -75,11 +75,9 @@ packageGen = {
mathcomp ? current-mathcomp, mathcomp ? current-mathcomp,
license ? mathcomp.meta.license, license ? mathcomp.meta.license,
# mandatory # mandatory
package, version, version-sha256, description package, version ? "broken", version-sha256, description
}: }:
if version == "" then {} { "${package}" = let from = src; in
else { "${package}" =
let from = src; in
stdenv.mkDerivation rec { stdenv.mkDerivation rec {
inherit version; inherit version;
@ -102,19 +100,20 @@ packageGen = {
inherit (src.meta) homepage; inherit (src.meta) homepage;
inherit (mathcomp.meta) platforms; inherit (mathcomp.meta) platforms;
maintainers = [ stdenv.lib.maintainers.vbgl ]; maintainers = [ stdenv.lib.maintainers.vbgl ];
broken = (version == "broken");
}; };
passthru = { passthru = {
inherit version-sha256; inherit version-sha256;
compatibleCoqVersions = v: builtins.elem v coq-versions; compatibleCoqVersions = if meta.broken then _: false else
v: builtins.elem v coq-versions;
};
};
}; };
};};
current-versions = versions."${current-mathcomp.version}" current-versions = versions."${current-mathcomp.version}" or {};
or (throw "no mathcomp extra packages found for mathcomp ${current-mathcomp.version}");
select = x: mapAttrs (n: pkg: {package = n;} // pkg) select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate param x);
(recursiveUpdate (overrideExisting x param) x);
all = (mapAttrs' (n: pkg: all = (mapAttrs' (n: pkg:
{name = "mathcomp_1_7-${n}"; {name = "mathcomp_1_7-${n}";