Commit ff20028f authored by 4ever2's avatar 4ever2 Committed by Vincent Laporte
Browse files

MetaCoq sub-packages dependencies

parent 51d1fd39
Loading
Loading
Loading
Loading
+20 −5
Original line number Diff line number Diff line
@@ -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")) ;