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

Add MetaCoq sub-packages to coq-packages

Browse Source
This commit is contained in:
4ever2
2024-10-31 11:09:26 +01:00
committed by Vincent Laporte
parent e24d868aba
commit 2d4ee5cab7
2 changed files with 20 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/metacoq/default.nix
+10 -4
View File
@@ -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")
pkgs/top-level/coq-packages.nix
+10 -4
View File
@@ -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 {};