coqPackages.mathcomp,ssreflect: 1.5 -> 1.6
See the INSTALL file in the mathcomp package for instructions on upgrading projects from 1.5 to 1.6. The 1.6 version works with both Coq 8.4 and 8.5.
This commit is contained in:
@@ -4,15 +4,15 @@ let src =
|
||||
if coq.coq-version == "8.4" then
|
||||
|
||||
fetchurl {
|
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
|
||||
sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
|
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
|
||||
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
|
||||
}
|
||||
|
||||
else if coq.coq-version == "8.5" then
|
||||
|
||||
fetchurl {
|
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;
|
||||
sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";
|
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
|
||||
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
|
||||
}
|
||||
|
||||
else throw "No mathcomp package for Coq version ${coq.coq-version}";
|
||||
|
||||
@@ -1,25 +1,33 @@
|
||||
{ stdenv, fetchurl, coq, ssreflect
|
||||
, graphviz, ocamlPackages, withDoc ? true
|
||||
{ stdenv, fetchurl, coq, ssreflect, ncurses, which
|
||||
, graphviz, ocamlPackages, withDoc ? false
|
||||
, src
|
||||
}:
|
||||
|
||||
stdenv.mkDerivation {
|
||||
|
||||
name = "coq-mathcomp-1.5-${coq.coq-version}";
|
||||
name = "coq-mathcomp-1.6-${coq.coq-version}";
|
||||
|
||||
inherit src;
|
||||
|
||||
nativeBuildInputs = stdenv.lib.optionals withDoc
|
||||
([ graphviz ] ++ (with ocamlPackages; [ ocaml camlp5_transitional ]));
|
||||
propagatedBuildInputs = [ ssreflect ];
|
||||
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ncurses which ];
|
||||
propagatedBuildInputs = [ coq ssreflect ];
|
||||
|
||||
enableParallelBuilding = true;
|
||||
|
||||
buildFlags = stdenv.lib.optionalString withDoc "doc";
|
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
||||
preBuild = ''
|
||||
cd mathcomp
|
||||
export COQBIN=${coq}/bin/
|
||||
'';
|
||||
|
||||
postInstall = stdenv.lib.optionalString withDoc ''
|
||||
installPhase = ''
|
||||
make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
|
||||
rm -fr $out/lib/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect*
|
||||
rm -fr $out/lib/coq/${coq.coq-version}/user-contrib/ssrmatching.cmi
|
||||
rm -fr $out/share/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect*
|
||||
'' + stdenv.lib.optionalString withDoc ''
|
||||
make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
|
||||
'';
|
||||
|
||||
|
||||
Reference in New Issue
Block a user