From d9f41a5bcee2f81c851bb060d287f6bc80986973 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 15 Dec 2017 19:52:16 +0000 Subject: [PATCH] coqPackages: move to a separate file and filter the package set --- .../development/coq-modules/CoLoR/default.nix | 12 +-- pkgs/development/coq-modules/HoTT/default.nix | 8 +- .../coq-modules/category-theory/default.nix | 4 + .../coq-modules/equations/default.nix | 4 + pkgs/development/coq-modules/fiat/HEAD.nix | 4 +- .../coq-modules/math-classes/default.nix | 13 ++-- .../coq-modules/metalib/default.nix | 9 ++- pkgs/top-level/all-packages.nix | 57 ++------------ pkgs/top-level/coq-packages.nix | 74 +++++++++++++++++++ 9 files changed, 115 insertions(+), 70 deletions(-) create mode 100644 pkgs/top-level/coq-packages.nix diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index ec190d5a1d6..3f5ec69235f 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -1,8 +1,4 @@ -{ stdenv, fetchurl, coq, coqPackages }: - -if !stdenv.lib.versionAtLeast coq.coq-version "8.6" -then throw "CoLoR is not available for Coq ${coq.coq-version}" -else +{ stdenv, fetchurl, coq, bignums }: stdenv.mkDerivation { name = "coq${coq.coq-version}-CoLoR-1.4.0"; @@ -12,7 +8,7 @@ stdenv.mkDerivation { sha256 = "1jsp9adsh7w59y41ihbwchryjhjpajgs9bhf8rnb4b3hzccqxgag"; }; - buildInputs = [ coq coqPackages.bignums ]; + buildInputs = [ coq bignums ]; enableParallelBuilding = false; installPhase = '' @@ -25,4 +21,8 @@ stdenv.mkDerivation { maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; }; + + passthru = { + compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; + }; } diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index cb77ac3deac..fb01da8d59c 100644 --- a/pkgs/development/coq-modules/HoTT/default.nix +++ b/pkgs/development/coq-modules/HoTT/default.nix @@ -1,8 +1,6 @@ { stdenv, fetchFromGitHub, autoconf, automake, coq }: -if !stdenv.lib.versionAtLeast coq.coq-version "8.6" -then throw "This version of HoTT requires Coq 8.6" -else stdenv.mkDerivation rec { +stdenv.mkDerivation rec { name = "coq${coq.coq-version}-HoTT-${version}"; version = "20170921"; @@ -56,4 +54,8 @@ else stdenv.mkDerivation rec { maintainers = with maintainers; [ siddharthist ]; platforms = coq.meta.platforms; }; + + passthru = { + compatibleCoqVersions = v: v == "8.6"; + }; } diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index 143e0344cf3..766a10c9579 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -42,4 +42,8 @@ stdenv.mkDerivation rec { platforms = coq.meta.platforms; }; + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ]; + }; + } diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index eb05a1be53e..34210ba01bb 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -42,4 +42,8 @@ stdenv.mkDerivation rec { platforms = coq.meta.platforms; }; + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ]; + }; + } diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index dc411763da5..b970747c772 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -30,7 +30,9 @@ stdenv.mkDerivation rec { description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; - broken = stdenv.lib.versionAtLeast coq.coq-version "8.6"; }; + passthru = { + compatibleCoqVersions = v: v == "8.5"; + }; } diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index d045ec4223b..1831cd0c571 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -1,8 +1,4 @@ -{ stdenv, fetchFromGitHub, coq, coqPackages }: - -if ! stdenv.lib.versionAtLeast coq.coq-version "8.6" then - throw "Math-Classes requires Coq 8.6 or later." -else +{ stdenv, fetchFromGitHub, coq, bignums }: stdenv.mkDerivation rec { @@ -16,7 +12,7 @@ stdenv.mkDerivation rec { sha256 = "0wgnczacvkb2pc3vjbni9bwjijfyd5jcdnyyjg8185hkf9zzabgi"; }; - buildInputs = [ coq coqPackages.bignums ]; + buildInputs = [ coq bignums ]; enableParallelBuilding = true; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; @@ -26,4 +22,9 @@ stdenv.mkDerivation rec { maintainers = with maintainers; [ siddharthist jwiegley ]; platforms = coq.meta.platforms; }; + + passthru = { + compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; + }; + } diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix index 0304cb48b3b..f6316f77a1f 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchgit, coq, ocamlPackages, haskellPackages, which, ott +{ stdenv, fetchgit, coq, haskellPackages, which, ott }: stdenv.mkDerivation rec { @@ -29,8 +29,7 @@ stdenv.mkDerivation rec { license = stdenv.lib.licenses.mit; }; - buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott ] - ++ (with ocamlPackages; [ findlib ]); + buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott coq.findlib ]; propagatedBuildInputs = [ coq ]; enableParallelBuilding = true; @@ -50,4 +49,8 @@ stdenv.mkDerivation rec { platforms = coq.meta.platforms; }; + passthru = { + compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; + }; + } diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 53f0234d604..dc5b26069f6 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -18825,57 +18825,12 @@ with pkgs; boogie = dotnetPackages.Boogie; - coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { - make = pkgs.gnumake3; - inherit (ocamlPackages_3_12_1) ocaml findlib; - camlp5 = ocamlPackages_3_12_1.camlp5_transitional; - lablgtk = ocamlPackages_3_12_1.lablgtk_2_14; - }; - coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix { - inherit (ocamlPackages_4_02) ocaml findlib lablgtk; - camlp5 = ocamlPackages_4_02.camlp5_transitional; - }; - coq_8_5 = callPackage ../applications/science/logic/coq { - version = "8.5pl3"; - }; - coq_8_6 = callPackage ../applications/science/logic/coq {}; - coq_8_7 = callPackage ../applications/science/logic/coq { - version = "8.7.1"; - }; - - mkCoqPackages = self: coq: let callPackage = newScope self; in rec { - inherit callPackage coq; - coqPackages = self; - - autosubst = callPackage ../development/coq-modules/autosubst {}; - bignums = if stdenv.lib.versionAtLeast coq.coq-version "8.6" - then callPackage ../development/coq-modules/bignums {} - else null; - coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; - coquelicot = callPackage ../development/coq-modules/coquelicot {}; - dpdgraph = callPackage ../development/coq-modules/dpdgraph {}; - flocq = callPackage ../development/coq-modules/flocq {}; - heq = callPackage ../development/coq-modules/heq {}; - HoTT = callPackage ../development/coq-modules/HoTT {}; - interval = callPackage ../development/coq-modules/interval {}; - mathcomp = callPackage ../development/coq-modules/mathcomp { }; - metalib = callPackage ../development/coq-modules/metalib { }; - paco = callPackage ../development/coq-modules/paco {}; - ssreflect = callPackage ../development/coq-modules/ssreflect { }; - QuickChick = callPackage ../development/coq-modules/QuickChick {}; - CoLoR = callPackage ../development/coq-modules/CoLoR {}; - math-classes = callPackage ../development/coq-modules/math-classes { }; - fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {}; - equations = callPackage ../development/coq-modules/equations { }; - coq-haskell = callPackage ../development/coq-modules/coq-haskell { }; - category-theory = callPackage ../development/coq-modules/category-theory { }; - }; - - coqPackages_8_5 = mkCoqPackages coqPackages_8_5 coq_8_5; - coqPackages_8_6 = mkCoqPackages coqPackages_8_6 coq_8_6; - coqPackages_8_7 = mkCoqPackages coqPackages_8_7 coq_8_7; - coqPackages = coqPackages_8_6; - coq = coqPackages.coq; + inherit (callPackage ./coq-packages.nix {}) + mkCoqPackages + coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7 + coqPackages_8_5 coqPackages_8_6 coqPackages_8_7 + coqPackages coq + ; coq2html = callPackage ../applications/science/logic/coq2html { make = pkgs.gnumake3; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix new file mode 100644 index 00000000000..34d9f09ff14 --- /dev/null +++ b/pkgs/top-level/coq-packages.nix @@ -0,0 +1,74 @@ +{ lib, callPackage, newScope +, gnumake3 +, ocamlPackages_3_12_1 +, ocamlPackages_4_02 +}: + +let + mkCoqPackages' = self: coq: + let callPackage = newScope self ; in rec { + inherit callPackage coq; + coqPackages = self; + + autosubst = callPackage ../development/coq-modules/autosubst {}; + bignums = if lib.versionAtLeast coq.coq-version "8.6" + then callPackage ../development/coq-modules/bignums {} + else null; + category-theory = callPackage ../development/coq-modules/category-theory { }; + CoLoR = callPackage ../development/coq-modules/CoLoR {}; + coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; + coq-haskell = callPackage ../development/coq-modules/coq-haskell { }; + coquelicot = callPackage ../development/coq-modules/coquelicot {}; + dpdgraph = callPackage ../development/coq-modules/dpdgraph {}; + equations = callPackage ../development/coq-modules/equations { }; + fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {}; + flocq = callPackage ../development/coq-modules/flocq {}; + heq = callPackage ../development/coq-modules/heq {}; + HoTT = callPackage ../development/coq-modules/HoTT {}; + interval = callPackage ../development/coq-modules/interval {}; + math-classes = callPackage ../development/coq-modules/math-classes { }; + mathcomp = callPackage ../development/coq-modules/mathcomp { }; + metalib = callPackage ../development/coq-modules/metalib { }; + paco = callPackage ../development/coq-modules/paco {}; + QuickChick = callPackage ../development/coq-modules/QuickChick {}; + ssreflect = callPackage ../development/coq-modules/ssreflect { }; + }; + + filterCoqPackages = coq: + lib.filterAttrs + (_: p: + let pred = p.compatibleCoqVersions or (_: true); + in pred coq.coq-version + ); + +in rec { + + mkCoqPackages = coq: + let self = mkCoqPackages' self coq; in + filterCoqPackages coq self; + + coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { + make = gnumake3; + inherit (ocamlPackages_3_12_1) ocaml findlib; + camlp5 = ocamlPackages_3_12_1.camlp5_transitional; + lablgtk = ocamlPackages_3_12_1.lablgtk_2_14; + }; + coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix { + inherit (ocamlPackages_4_02) ocaml findlib lablgtk; + camlp5 = ocamlPackages_4_02.camlp5_transitional; + }; + coq_8_5 = callPackage ../applications/science/logic/coq { + version = "8.5pl3"; + }; + coq_8_6 = callPackage ../applications/science/logic/coq {}; + coq_8_7 = callPackage ../applications/science/logic/coq { + version = "8.7.1"; + }; + + coqPackages_8_5 = mkCoqPackages coq_8_5; + coqPackages_8_6 = mkCoqPackages coq_8_6; + coqPackages_8_7 = mkCoqPackages coq_8_7; + coqPackages = coqPackages_8_6; + coq = coqPackages.coq; + +}