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

coq-ssreflect: refactor

Browse Source
This commit is contained in:
Vincent Laporte 2015-05-28 16:09:05 +02:00
parent 0f6b981fba
commit 524b7fe178
3 changed files with 33 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
pkgs/development/coq-modules/ssreflect/default.nix
View File

@ -1,48 +1,27 @@
{ stdenv, fetchurl, coq { callPackage, fetchurl, coq }:
, graphviz, withDoc ? true
}:
assert coq.coq-version == "8.4"; if coq.coq-version == "8.4" then
stdenv.mkDerivation { callPackage ./generic.nix {
name = "coq-ssreflect-1.5";
src = fetchurl { src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz; url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz;
sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds"; sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
}; };
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; }
buildInputs = [ coq.ocaml coq.camlp5 ];
propagatedBuildInputs = [ coq ];
enableParallelBuilding = true; else if coq.coq-version == "8.5" then
patchPhase = '' callPackage ./generic.nix {
# Permit building of the ssrcoq statically-bound executable
sed -i 's/^#-custom/-custom/' Make
sed -i 's/^#SSRCOQ/SSRCOQ/' Make
'';
buildFlags = stdenv.lib.optionalString withDoc "doc"; src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz;
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf";
postInstall = ''
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/
'';
meta = with stdenv.lib; {
homepage = http://ssr.msr-inria.inria.fr/;
license = licenses.cecill-b;
maintainers = with maintainers; [ vbgl jwiegley ];
platforms = coq.meta.platforms;
}; };
patches = [ ./threads.patch ];
} }
else throw "No ssreflect package for Coq version ${coq.coq-version}"

22
pkgs/development/coq-modules/ssreflect/1.5.nix → pkgs/development/coq-modules/ssreflect/generic.nix
View File

@ -1,22 +1,21 @@
{stdenv, fetchurl, coq}: { stdenv, fetchurl, coq
, graphviz, withDoc ? true
assert coq.coq-version == "8.5"; , src, patches ? []
}:
stdenv.mkDerivation { stdenv.mkDerivation {
name = "coq-ssreflect-1.5-8.5b2"; name = "coq-${coq.coq-version}-ssreflect-1.5";
src = fetchurl { inherit src;
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz;
sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf";
};
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
buildInputs = [ coq.ocaml coq.camlp5 ]; buildInputs = [ coq.ocaml coq.camlp5 ];
propagatedBuildInputs = [ coq ]; propagatedBuildInputs = [ coq ];
enableParallelBuilding = true; enableParallelBuilding = true;
patches = [ ./threads.patch ]; inherit patches;
postPatch = '' postPatch = ''
# Permit building of the ssrcoq statically-bound executable # Permit building of the ssrcoq statically-bound executable
@ -24,12 +23,17 @@ stdenv.mkDerivation {
sed -i 's/^#SSRCOQ/SSRCOQ/' Make sed -i 's/^#SSRCOQ/SSRCOQ/' Make
''; '';
buildFlags = stdenv.lib.optionalString withDoc "doc";
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
postInstall = '' postInstall = ''
mkdir -p $out/bin mkdir -p $out/bin
cp -p bin/ssrcoq $out/bin cp -p bin/ssrcoq $out/bin
cp -p bin/ssrcoq.byte $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/
''; '';
meta = with stdenv.lib; { meta = with stdenv.lib; {

15
pkgs/top-level/all-packages.nix
View File

@ -14090,19 +14090,18 @@ let
mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec { mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec {
mathcomp = callPackage ../development/coq-modules/mathcomp/1.5.nix { inherit callPackage;
coq = coq_8_5;
ssreflect = ssreflect;
};
ssreflect = callPackage ../development/coq-modules/ssreflect/1.5.nix { coq = coq_8_5;
coq = coq_8_5;
}; mathcomp = callPackage ../development/coq-modules/mathcomp/1.5.nix { };
ssreflect = callPackage ../development/coq-modules/ssreflect { };
}; };
coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages); coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);
coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages); coqPackages_8_5 = recurseIntoAttrs (mkCoqPackages_8_5 coqPackages_8_5);
cvc3 = callPackage ../applications/science/logic/cvc3 {}; cvc3 = callPackage ../applications/science/logic/cvc3 {};
cvc4 = callPackage ../applications/science/logic/cvc4 {}; cvc4 = callPackage ../applications/science/logic/cvc4 {};