diff options
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/autosubst/default.nix | 1 | ||||
-rw-r--r-- | pkgs/development/coq-modules/contribs/default.nix | 2 | ||||
-rw-r--r-- | pkgs/development/coq-modules/fiat/HEAD.nix | 5 | ||||
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/default.nix | 80 | ||||
-rw-r--r-- | pkgs/development/coq-modules/mathcomp/generic.nix | 42 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/default.nix | 59 | ||||
-rw-r--r-- | pkgs/development/coq-modules/ssreflect/generic.nix | 49 |
7 files changed, 94 insertions, 144 deletions
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix index 9c24e77e0f78..bffa5172b0e4 100644 --- a/pkgs/development/coq-modules/autosubst/default.nix +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -11,6 +11,7 @@ stdenv.mkDerivation rec { sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341"; }; + buildInputs = [ coq ]; propagatedBuildInputs = [ mathcomp ]; patches = [./0001-changes-to-work-with-Coq-8.6.patch]; diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix index d12d3fefb944..a1ecdd610a3e 100644 --- a/pkgs/development/coq-modules/contribs/default.nix +++ b/pkgs/development/coq-modules/contribs/default.nix @@ -1018,7 +1018,7 @@ let mkContrib = repo: revs: param: sha256 = "0fp3vdl79c8d759qjhk42rjfpkd0ba4pcw572f5gxn28kfwz3rrj"; }; - zfc = mkContrib "zfc" [ "8.5" "8.6" "8.7" ] { + zfc = mkContrib "zfc" [ "8.5" "8.6" "8.7" "8.8" ] { version = "v8.5.0-5-gbba3259"; rev = "bba325933370fea64780b1afa2fad54c1b567819"; sha256 = "0iwkpmc22nwasrk4g7ki4s5y05zjs7kmqk3j98giwp2wiavhgapn"; diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index a064064fd919..4abaec6528a9 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -11,8 +11,9 @@ stdenv.mkDerivation rec { sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; }; - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 python27 ]; - propagatedBuildInputs = [ coq ]; + buildInputs = [ coq python27 ] ++ (with coq.ocamlPackages; [ ocaml camlp5 ]); + + prePatch = "patchShebangs etc/coq-scripts"; doCheck = false; diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 92c3c87774ab..1e5b6b7bf666 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -1,29 +1,65 @@ -{ callPackage, fetchurl, coq }: +{ stdenv, fetchFromGitHub, coq, ncurses, which +, graphviz, withDoc ? false +}: let param = - let param_1_7 = { - version = "1.7.0"; - sha256 = "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"; - }; in - + if stdenv.lib.versionAtLeast coq.coq-version "8.6" then + { + version = "1.7.0"; + sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; + } + else if stdenv.lib.versionAtLeast coq.coq-version "8.5" then { - "8.5" = { - version = "1.6.1"; - sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"; - }; - - "8.6" = param_1_7; - "8.7" = param_1_7; - "8.8" = param_1_7; - - }."${coq.coq-version}" -; in - -callPackage ./generic.nix { - name = "coq${coq.coq-version}-mathcomp-${param.version}"; - src = fetchurl { - url = "https://github.com/math-comp/math-comp/archive/mathcomp-${param.version}.tar.gz"; + version = "1.6.1"; + sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; + } + else throw "No version of math-comp is available for Coq ${coq.coq-version}"; + +in + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-mathcomp-${version}"; + + # used in ssreflect + inherit (param) version; + + src = fetchFromGitHub { + owner = "math-comp"; + repo = "math-comp"; + rev = "mathcomp-${param.version}"; 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"; + + COQBIN = "${coq}/bin/"; + + preBuild = '' + patchShebangs etc/utils/ssrcoqdep || true + cd mathcomp + ''; + + 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: stdenv.lib.versionAtLeast v "8.5"; + }; + } diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix deleted file mode 100644 index 2a602711965f..000000000000 --- a/pkgs/development/coq-modules/mathcomp/generic.nix +++ /dev/null @@ -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" ]; - }; - -} diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix index 9e9c3c7957aa..1fcb7e2da8ae 100644 --- a/pkgs/development/coq-modules/ssreflect/default.nix +++ b/pkgs/development/coq-modules/ssreflect/default.nix @@ -1,29 +1,32 @@ -{ callPackage, fetchurl, coq }: - -let param = - - let param_1_7 = { - version = "1.7.0"; - sha256 = "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"; - }; in - - { - "8.5" = { - version = "1.6.1"; - sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"; - }; - - "8.6" = param_1_7; - "8.7" = param_1_7; - "8.8" = param_1_7; - - }."${coq.coq-version}" -; in - -callPackage ./generic.nix { - name = "coq${coq.coq-version}-ssreflect-${param.version}"; - src = fetchurl { - url = "https://github.com/math-comp/math-comp/archive/mathcomp-${param.version}.tar.gz"; - inherit (param) sha256; - }; +{ stdenv, fetchFromGitHub, coq, ncurses, which +, graphviz, mathcomp, withDoc ? false +}: + +stdenv.mkDerivation rec { + name = "coq${coq.coq-version}-ssreflect-${version}"; + + inherit (mathcomp) src version meta; + + nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; + buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + + enableParallelBuilding = true; + + COQBIN = "${coq}/bin/"; + + preBuild = '' + patchShebangs etc/utils/ssrcoqdep || true + cd mathcomp/ssreflect + ''; + + installPhase = '' + make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + postInstall = stdenv.lib.optionalString withDoc '' + 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/ + ''; + + passthru.compatibleCoqVersions = mathcomp.compatibleCoqVersions; } diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix deleted file mode 100644 index 23e364cd960d..000000000000 --- a/pkgs/development/coq-modules/ssreflect/generic.nix +++ /dev/null @@ -1,49 +0,0 @@ -{ stdenv, coq, ncurses, which -, graphviz, withDoc ? false -, src, name, patches ? [] -}: - -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; - - inherit patches; - - preBuild = '' - patchShebangs etc/utils/ssrcoqdep || true - cd mathcomp/ssreflect - export COQBIN=${coq}/bin/ - ''; - - 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 - '' + stdenv.lib.optionalString withDoc '' - 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; { - homepage = http://ssr.msr-inria.inria.fr/; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" ]; - }; - -} |