coqPackages.metacoq: create package (#162639)

2 files changed, 77 insertions, 0 deletions

diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix
new file mode 100644
index 000000000000..583d8b7adb91
--- /dev/null
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@@ -0,0 +1,76 @@
+{ lib, which, fetchzip,
+  mkCoqDerivation, recurseIntoAttrs,  single ? false,
+  coqPackages, coq, equations, version ? null }@args:
+with builtins // lib;
+let
+  repo  = "metacoq";
+  owner = "MetaCoq";
+  defaultVersion = with versions; switch coq.coq-version [
+      { case = "8.11"; out = "1.0-beta2-8.11"; }
+      { case = "8.12"; out = "1.0-beta2-8.12"; }
+      # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
+      # { case = "8.13"; out = "1.0-beta2-8.13"; }
+    ] null;
+  release = {
+    "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
+    "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
+    "1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
+  };
+  releaseRev = v: "v${v}";
+
+  # list of core metacoq packages sorted by dependency order
+  packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
+
+  template-coq = metacoq_ "template-coq";
+
+  metacoq_ = package: let
+      metacoq-deps = if package == "single" then []
+        else map metacoq_ (head (splitList (pred.equal package) packages));
+      pkgpath = if package == "single" then "./" else "./${package}";
+      pname = if package == "all" then "metacoq" else "metacoq-${package}";
+      pkgallMake = ''
+          mkdir all
+          echo "all:" > all/Makefile
+          echo "install:" >> all/Makefile
+        '' ;
+      derivation = mkCoqDerivation ({
+        inherit version pname defaultVersion release releaseRev repo owner;
+
+        extraNativeBuildInputs = [ which ];
+        mlPlugin = true;
+        extraBuildInputs = [ coq.ocamlPackages.zarith ];
+        propagatedBuildInputs = [ equations ] ++ metacoq-deps;
+
+        patchPhase =  ''
+          patchShebangs ./configure.sh
+          patchShebangs ./template-coq/update_plugin.sh
+          patchShebangs ./template-coq/gen-src/to-lower.sh
+          patchShebangs ./pcuic/clean_extraction.sh
+          patchShebangs ./safechecker/clean_extraction.sh
+          patchShebangs ./erasure/clean_extraction.sh
+          echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
+          sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
+        '' ;
+
+        configurePhase = optionalString (package == "all") pkgallMake + ''
+          touch ${pkgpath}/metacoq-config
+        '' + optionalString (elem package ["safechecker" "erasure"]) ''
+          echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
+        '' + optionalString (package == "single") ''
+          ./configure.sh local
+        '';
+
+        preBuild = ''
+          cd ${pkgpath}
+        '' ;
+
+        meta = {
+          homepage    = "https://metacoq.github.io/";
+          license     = licenses.mit;
+          maintainers = with maintainers; [ cohencyril ];
+        };
+      } // optionalAttrs (package != "single")
+        { passthru = genAttrs packages metacoq_; });
+    in 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 c71ec2acf944..6af05d761c43 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -77,6 +77,7 @@ let
       mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {};
       mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
       mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
+      metacoq = callPackage ../development/coq-modules/metacoq { };
       metalib = callPackage ../development/coq-modules/metalib { };
       multinomials = callPackage ../development/coq-modules/multinomials {};
       odd-order = callPackage ../development/coq-modules/odd-order { };