coqPackages.mathcomp: refactor
This commit is contained in:
parent
14a9365952
commit
d2c38d1eef
@ -1,6 +1,8 @@
|
|||||||
{ callPackage, fetchurl, coq }:
|
{ stdenv, fetchurl, coq, ncurses, which
|
||||||
|
, graphviz, withDoc ? false
|
||||||
|
}:
|
||||||
|
|
||||||
let param =
|
let params =
|
||||||
|
|
||||||
let param_1_7 = {
|
let param_1_7 = {
|
||||||
version = "1.7.0";
|
version = "1.7.0";
|
||||||
@ -16,14 +18,48 @@ let param =
|
|||||||
"8.6" = param_1_7;
|
"8.6" = param_1_7;
|
||||||
"8.7" = param_1_7;
|
"8.7" = param_1_7;
|
||||||
"8.8" = param_1_7;
|
"8.8" = param_1_7;
|
||||||
|
"8.9" = param_1_7;
|
||||||
|
|
||||||
}."${coq.coq-version}"
|
};
|
||||||
; in
|
param = params."${coq.coq-version}";
|
||||||
|
in
|
||||||
|
|
||||||
callPackage ./generic.nix {
|
stdenv.mkDerivation {
|
||||||
name = "coq${coq.coq-version}-mathcomp-${param.version}";
|
name = "coq${coq.coq-version}-mathcomp-${param.version}";
|
||||||
|
|
||||||
src = fetchurl {
|
src = fetchurl {
|
||||||
url = "https://github.com/math-comp/math-comp/archive/mathcomp-${param.version}.tar.gz";
|
url = "https://github.com/math-comp/math-comp/archive/mathcomp-${param.version}.tar.gz";
|
||||||
inherit (param) sha256;
|
inherit (param) sha256;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
|
||||||
|
buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
|
||||||
|
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
buildFlags = stdenv.lib.optionalString withDoc "doc";
|
||||||
|
|
||||||
|
preBuild = ''
|
||||||
|
patchShebangs etc/utils/ssrcoqdep || true
|
||||||
|
cd mathcomp
|
||||||
|
export COQBIN=${coq}/bin/
|
||||||
|
'';
|
||||||
|
|
||||||
|
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}/
|
||||||
|
'';
|
||||||
|
|
||||||
|
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 = v: builtins.hasAttr v params;
|
||||||
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
@ -1,42 +0,0 @@
|
|||||||
{ stdenv, coq, ncurses, which
|
|
||||||
, graphviz, withDoc ? false
|
|
||||||
, src, name
|
|
||||||
}:
|
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
|
||||||
|
|
||||||
inherit name;
|
|
||||||
inherit src;
|
|
||||||
|
|
||||||
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
|
|
||||||
buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ncurses which ];
|
|
||||||
propagatedBuildInputs = [ coq ];
|
|
||||||
|
|
||||||
enableParallelBuilding = true;
|
|
||||||
|
|
||||||
buildFlags = stdenv.lib.optionalString withDoc "doc";
|
|
||||||
|
|
||||||
preBuild = ''
|
|
||||||
patchShebangs etc/utils/ssrcoqdep || true
|
|
||||||
cd mathcomp
|
|
||||||
export COQBIN=${coq}/bin/
|
|
||||||
'';
|
|
||||||
|
|
||||||
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}/
|
|
||||||
'';
|
|
||||||
|
|
||||||
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 = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" ];
|
|
||||||
};
|
|
||||||
|
|
||||||
}
|
|
Loading…
x
Reference in New Issue
Block a user