diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix index c79261aa174f..bc87c7111352 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -39,9 +39,7 @@ let releaseRev = v: "v${v}"; # list of core metacoq packages sorted by dependency order - packages = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" - then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ] - else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ]; + packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]; template-coq = metacoq_ "template-coq"; @@ -105,6 +103,14 @@ let { propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; }); - in derivation; + # utils, common, template-pcuic, quotation, safechecker-plugin, and erasure-plugin + # packages didn't exist before 1.2, so bulding nothing in that case + patched-derivation = derivation.overrideAttrs (o: + lib.optionalAttrs (o.pname != null && + lib.elem package [ "utils" "common" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" ] && + o.version != null && o.version != "dev" && lib.versions.isLt "1.2" o.version) + { patchPhase = ""; configurePhase = ""; preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } + ); + in patched-derivation; in metacoq_ (if single then "single" else "all") diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index cfc8bcd289da..a4e75a9bf95a 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -115,10 +115,16 @@ let mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {}; MenhirLib = callPackage ../development/coq-modules/MenhirLib {}; metacoq = callPackage ../development/coq-modules/metacoq { }; - metacoq-template-coq = self.metacoq.template-coq; - metacoq-pcuic = self.metacoq.pcuic; - metacoq-safechecker = self.metacoq.safechecker; - metacoq-erasure = self.metacoq.erasure; + metacoq-utils = self.metacoq.utils; + metacoq-common = self.metacoq.common; + metacoq-template-coq = self.metacoq.template-coq; + metacoq-pcuic = self.metacoq.pcuic; + metacoq-safechecker = self.metacoq.safechecker; + metacoq-template-pcuic = self.metacoq.template-pcuic; + metacoq-erasure = self.metacoq.erasure; + metacoq-quotation = self.metacoq.quotation; + metacoq-safechecker-plugin = self.metacoq.safechecker-plugin; + metacoq-erasure-plugin = self.metacoq.erasure-plugin; metalib = callPackage ../development/coq-modules/metalib { }; mtac2 = callPackage ../development/coq-modules/mtac2 {}; multinomials = callPackage ../development/coq-modules/multinomials {};