diff options
author | John Wiegley <johnw@newartisans.com> | 2015-12-20 11:12:23 -0800 |
---|---|---|
committer | John Wiegley <johnw@newartisans.com> | 2015-12-20 11:12:23 -0800 |
commit | e582c41482615dc4d383a8d3f578e9ead9209743 (patch) | |
tree | ad65012720a092bdd2a95dff219e80a8534291b9 /pkgs/development | |
parent | 56f6be2583909cff986ec12c9f3a3c9af6e83936 (diff) | |
download | nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar.gz nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar.bz2 nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar.lz nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar.xz nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.tar.zst nixlib-e582c41482615dc4d383a8d3f578e9ead9209743.zip |
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.
Diffstat (limited to 'pkgs/development')
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/default.nix | 8 | ||||
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/generic.nix | 24 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/default.nix | 10 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/generic.nix | 31 |
4 files changed, 39 insertions, 34 deletions
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 7c34e186717c..189b12206400 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -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}"; diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix index 56838734b6d3..b4048aa80037 100644 --- a/pkgs/development/coq-modules/mathcomp/generic.nix +++ b/pkgs/development/coq-modules/mathcomp/generic.nix @@ -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}/ ''; diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix index a0b0d951c0df..8ba49d06bae9 100644 --- a/pkgs/development/coq-modules/ssreflect/default.nix +++ b/pkgs/development/coq-modules/ssreflect/default.nix @@ -5,8 +5,8 @@ if coq.coq-version == "8.4" then callPackage ./generic.nix { src = fetchurl { - url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz; - sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds"; + url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; + sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; }; } @@ -16,12 +16,10 @@ else if coq.coq-version == "8.5" then callPackage ./generic.nix { src = fetchurl { - url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz; - sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf"; + url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; + sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; }; - patches = [ ./threads.patch ]; - } else throw "No ssreflect package for Coq version ${coq.coq-version}" diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix index 3bfccab0be7d..d7303ad8852c 100644 --- a/pkgs/development/coq-modules/ssreflect/generic.nix +++ b/pkgs/development/coq-modules/ssreflect/generic.nix @@ -1,39 +1,38 @@ -{ stdenv, fetchurl, coq, ncurses -, graphviz, withDoc ? true +{ stdenv, fetchurl, coq, ncurses, which +, graphviz, withDoc ? false , src, patches ? [] }: stdenv.mkDerivation { - name = "coq-ssreflect-1.5-${coq.coq-version}"; + name = "coq-ssreflect-1.6-${coq.coq-version}"; inherit src; nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; - buildInputs = [ coq.ocaml coq.camlp5 ncurses ]; + buildInputs = [ coq.ocaml coq.camlp5 ncurses which ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; inherit patches; - postPatch = '' - # Permit building of the ssrcoq statically-bound executable - sed -i 's/^#-custom/-custom/' Make - sed -i 's/^#SSRCOQ/SSRCOQ/' Make + preBuild = '' + cd mathcomp/ssreflect + export COQBIN=${coq}/bin/ ''; - buildFlags = stdenv.lib.optionalString withDoc "doc"; - - installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; postInstall = '' - mkdir -p $out/bin - cp -p bin/ssrcoq $out/bin - cp -p bin/ssrcoq.byte $out/bin + # mkdir -p $out/bin + # cp -p bin/ssrcoq $out/bin + # cp -p bin/ssrcoq.byte $out/bin '' + stdenv.lib.optionalString withDoc '' - mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/ - cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/ + mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/ + cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/ ''; meta = with stdenv.lib; { |