From ff20028fd4567b09819fc8ce6cd676c2a390bd35 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Tue, 29 Oct 2024 17:05:14 +0100
Subject: [PATCH] MetaCoq sub-packages dependencies

---
 .../coq-modules/metacoq/default.nix           | 25 +++++++++++++++----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix
index adda89d523da..9452ac977b6f 100644
--- a/pkgs/development/coq-modules/metacoq/default.nix
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@@ -38,13 +38,28 @@ let
   };
   releaseRev = v: "v${v}";
 
-  # list of core metacoq packages sorted by dependency order
-  packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "translations" "all" ];
+  # list of core metacoq packages and their dependencies
+  packages = {
+    "utils"              = [];
+    "common"             = [ "utils" ];
+    "template-coq"       = [ "common" ];
+    "pcuic"              = if (lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev")
+                           then [ "common" ]
+                           else [ "template-coq" ];
+    "safechecker"        = [ "pcuic" ];
+    "template-pcuic"     = [ "template-coq" "pcuic" ];
+    "erasure"            = [ "safechecker" "template-pcuic" ];
+    "quotation"          = [ "template-coq" "pcuic" "template-pcuic" ];
+    "safechecker-plugin" = [ "template-pcuic" "safechecker" ];
+    "erasure-plugin"     = [ "template-pcuic" "erasure" ];
+    "translations"       = [ "template-coq" ];
+    "all"                = [ "safechecker-plugin" "erasure-plugin" "translations" "quotation" ];
+  };
 
   template-coq = metacoq_ "template-coq";
 
   metacoq_ = package: let
-      metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
+      metacoq-deps = lib.optionals (package != "single") (map metacoq_ packages.${package});
       pkgpath = if package == "single" then "./" else "./${package}";
       pname = if package == "all" then "metacoq" else "metacoq-${package}";
       pkgallMake = ''
@@ -79,7 +94,7 @@ let
 
         configurePhase = lib.optionalString (package == "all") pkgallMake + ''
           touch ${pkgpath}/metacoq-config
-        '' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" "translations"]) ''
+        '' + lib.optionalString (lib.elem package ["erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" "translations"]) ''
           echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
         '' + lib.optionalString (package == "single") ''
           ./configure.sh local
@@ -95,7 +110,7 @@ let
           maintainers = with lib.maintainers; [ cohencyril ];
         };
       } // lib.optionalAttrs (package != "single")
-        { passthru = lib.genAttrs packages metacoq_; })
+        { passthru = lib.mapAttrs (package: deps: metacoq_ package) packages; })
       ).overrideAttrs (o:
         let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" ||
                                        (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;