From fa1247675544430e97aa0499ad5073b98cb31817 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Wed, 17 Oct 2018 13:26:43 +0200 Subject: [PATCH 1/3] coq: add ocamlPackages in passthru We might need OCaml packages that are not the one Coq is depending on but they still need to come from the same package set (same OCaml version). --- pkgs/applications/science/logic/coq/default.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 23f1ff85edf0..040d722f9410 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -37,6 +37,8 @@ self = stdenv.mkDerivation { passthru = { inherit coq-version; + inherit ocamlPackages; + # For compatibility inherit (ocamlPackages) ocaml camlp5 findlib num; emacsBufferSetup = pkgs: '' ; Propagate coq paths to children From 8c399bd6c1cfc8308b0cc7b3f82cb250e0ffc9a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 19 Oct 2018 10:25:09 +0200 Subject: [PATCH 2/3] coqPackages: use coq.ocamlPackages instead of coq.ocaml, coq.camlp5, etc. --- pkgs/development/coq-modules/QuickChick/default.nix | 2 +- pkgs/development/coq-modules/bignums/default.nix | 2 +- pkgs/development/coq-modules/category-theory/default.nix | 2 +- pkgs/development/coq-modules/contribs/default.nix | 2 +- pkgs/development/coq-modules/coq-ext-lib/default.nix | 2 +- pkgs/development/coq-modules/coq-haskell/default.nix | 2 +- pkgs/development/coq-modules/dpdgraph/default.nix | 6 +++--- pkgs/development/coq-modules/equations/default.nix | 2 +- pkgs/development/coq-modules/fiat/HEAD.nix | 2 +- pkgs/development/coq-modules/flocq/default.nix | 2 +- pkgs/development/coq-modules/heq/default.nix | 2 +- pkgs/development/coq-modules/mathcomp/generic.nix | 2 +- pkgs/development/coq-modules/metalib/default.nix | 2 +- pkgs/development/coq-modules/paco/default.nix | 2 +- pkgs/development/coq-modules/ssreflect/generic.nix | 2 +- 15 files changed, 17 insertions(+), 17 deletions(-) diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix index fc88a1c33eed..d532020d663c 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -33,7 +33,7 @@ stdenv.mkDerivation rec { inherit (param) rev sha256; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ]; propagatedBuildInputs = [ coq ssreflect ]; enableParallelBuilding = false; diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index 474ce05c1d47..e645a3424c0d 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -28,7 +28,7 @@ stdenv.mkDerivation rec { inherit (param) rev sha256; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index c707fcdbd6be..4587e08be483 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -26,7 +26,7 @@ stdenv.mkDerivation rec { inherit (param) rev sha256; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ]; propagatedBuildInputs = [ coq ssreflect ]; enableParallelBuilding = false; diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix index 1b310d74b82a..d12d3fefb944 100644 --- a/pkgs/development/coq-modules/contribs/default.nix +++ b/pkgs/development/coq-modules/contribs/default.nix @@ -12,7 +12,7 @@ let mkContrib = repo: revs: param: sha256 = "${param.sha256}"; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 5e6ee7fac6f1..0e9c0b93ceda 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -22,7 +22,7 @@ stdenv.mkDerivation rec { inherit (param) sha256; }; - buildInputs = [ coq.ocaml coq.camlp5 ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix index cbfd79fdd272..57f31e1847c1 100644 --- a/pkgs/development/coq-modules/coq-haskell/default.nix +++ b/pkgs/development/coq-modules/coq-haskell/default.nix @@ -38,7 +38,7 @@ stdenv.mkDerivation rec { inherit (param) rev sha256; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ]; propagatedBuildInputs = [ coq ssreflect ]; enableParallelBuilding = false; diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index 5b9437e7c279..e403f7d4fb5c 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, autoreconfHook, coq, ocamlPackages }: +{ stdenv, fetchFromGitHub, autoreconfHook, coq }: let params = { "8.8" = { @@ -34,8 +34,8 @@ stdenv.mkDerivation { }; nativeBuildInputs = [ autoreconfHook ]; - buildInputs = [ coq coq.camlp5 ] - ++ (with ocamlPackages; [ ocaml findlib ocamlgraph ]); + buildInputs = [ coq ] + ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ocamlgraph ]); preInstall = '' mkdir -p $out/bin diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index fa17d37b4bd3..3f049eed34be 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -35,7 +35,7 @@ stdenv.mkDerivation rec { sha256 = "${param.sha256}"; }; - buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; preBuild = "coq_makefile -f _CoqProject -o Makefile"; diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index b970747c7726..a064064fd919 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; }; - buildInputs = [ coq.ocaml coq.camlp5 python27 ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 python27 ]; propagatedBuildInputs = [ coq ]; doCheck = false; diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index 092337125a4d..ff7385a9222e 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -10,7 +10,7 @@ stdenv.mkDerivation rec { sha256 = "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3"; }; - buildInputs = [ coq.ocaml coq.camlp5 bash which autoconf automake ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 bash which autoconf automake ]; propagatedBuildInputs = [ coq ]; buildPhase = '' diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix index bf441562b14e..03149bab58b1 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -10,7 +10,7 @@ stdenv.mkDerivation rec { sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p"; }; - buildInputs = [ coq.ocaml coq.camlp5 unzip ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; propagatedBuildInputs = [ coq ]; preBuild = "cd src"; diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix index 22721ca98bc2..2a602711965f 100644 --- a/pkgs/development/coq-modules/mathcomp/generic.nix +++ b/pkgs/development/coq-modules/mathcomp/generic.nix @@ -9,7 +9,7 @@ stdenv.mkDerivation { inherit src; nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; - buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ]; + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ncurses which ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix index f6316f77a1fa..46a6cafb6ab8 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -29,7 +29,7 @@ stdenv.mkDerivation rec { license = stdenv.lib.licenses.mit; }; - buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott coq.findlib ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 which coq lngen ott findlib ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix index 94a24eb70858..86a1301d3c76 100644 --- a/pkgs/development/coq-modules/paco/default.nix +++ b/pkgs/development/coq-modules/paco/default.nix @@ -10,7 +10,7 @@ stdenv.mkDerivation rec { sha256 = "1lcmdr0y2d7gzyvr8dal3pi7fibbd60bpi1l32fw89xiyrgqhsqy"; }; - buildInputs = [ coq.ocaml coq.camlp5 unzip ]; + buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; propagatedBuildInputs = [ coq ]; preBuild = "cd src"; diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix index d09e47a7f845..23e364cd960d 100644 --- a/pkgs/development/coq-modules/ssreflect/generic.nix +++ b/pkgs/development/coq-modules/ssreflect/generic.nix @@ -9,7 +9,7 @@ stdenv.mkDerivation { inherit src; nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; - buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ]; + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ncurses which ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; From 668c19a9ac0c4f7ee1d17ea0d397045345b34b3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 19 Oct 2018 10:29:49 +0200 Subject: [PATCH 3/3] coqPackages: update documentation to mention coq.ocamlPackages attribute --- doc/languages-frameworks/coq.xml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/languages-frameworks/coq.xml b/doc/languages-frameworks/coq.xml index d5f2574039f2..640b04c7da9d 100644 --- a/doc/languages-frameworks/coq.xml +++ b/doc/languages-frameworks/coq.xml @@ -11,10 +11,9 @@ - Some libraries require OCaml and sometimes also Camlp5 or findlib. The exact - versions that were used to build Coq are saved in the - coq.ocaml and coq.camlp5 and - coq.findlib attributes. + Some extensions (plugins) might require OCaml and sometimes other OCaml + packages. The coq.ocamlPackages attribute can be used + to depend on the same package set Coq was built against.