coqPackages.metacoq: update for coq 8.17 and 8.18 (#273541)

Also update default.nix to match the default.nix in
MetaCoq/metacoq:.nix/coq-overlays/metacoq/default.nix

Because some files have changed names, some version-dependent
building is required to keep building older versions.

And Metacoq's default.nix had older version checksums.
We use the more recent versions from nixpkgs for coq 8.14-8.16

Co-authored-by: Lars Rasmusson <Lars.Rasmusson@rise>

pkgs/development/coq-modules/metacoq/default.nix

···
 let
   repo  = "metacoq";
   owner = "MetaCoq";
-  defaultVersion = with versions; lib.switch coq.coq-version [
+  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.14"; out = "1.1-8.14"; }
       { case = "8.15"; out = "1.1-8.15"; }
       { case = "8.16"; out = "1.1-8.16"; }
+      { case = "8.17"; out = "1.2.1-8.17"; }
+      { case = "8.18"; out = "1.2.1-8.18"; }
     ] null;
   release = {
     "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
···
     "1.1-8.14".sha256 = "sha256-6vViCNQl6BnGgOHX3P/OLfFXN4aUfv4RbDokfz2BgQI=";
     "1.1-8.15".sha256 = "sha256-qCD3wFW4E+8vSVk4XoZ0EU4PVya0al+JorzS9nzmR/0=";
     "1.1-8.16".sha256 = "sha256-cTK4ptxpPPlqxAhasZFX3RpSlsoTZwhTqs2A3BZy9sA=";
+    "1.2.1-8.17".sha256 = "sha256-FP4upuRsG8B5Q5FIr76t+ecRirrOUX0D1QiLq0/zMyE=";
+    "1.2.1-8.18".sha256 = "sha256-49g5db2Bv8HpltptJdxA7zrmgNFGC6arx5h2mKHhrko=";
   };
   releaseRev = v: "v${v}";
 
   # list of core metacoq packages sorted by dependency order
-  packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
+  packages = if versionAtLeast coq.coq-version "8.17"
+     then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]
+     else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
 
   template-coq = metacoq_ "template-coq";
 
···
         mlPlugin = true;
         propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
 
-        patchPhase =  ''
+        patchPhase =  if versionAtLeast coq.coq-version "8.17" then ''
+          patchShebangs ./configure.sh
+          patchShebangs ./template-coq/update_plugin.sh
+          patchShebangs ./template-coq/gen-src/to-lower.sh
+          patchShebangs ./safechecker-plugin/clean_extraction.sh
+          patchShebangs ./erasure-plugin/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 ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
+        '' else ''
+          patchShebangs ./configure.sh
           patchShebangs ./template-coq/update_plugin.sh
           patchShebangs ./template-coq/gen-src/to-lower.sh
           patchShebangs ./pcuic/clean_extraction.sh
···
 
         configurePhase = optionalString (package == "all") pkgallMake + ''
           touch ${pkgpath}/metacoq-config
-        '' + optionalString (elem package ["safechecker" "erasure"]) ''
+        '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
           echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
         '' + optionalString (package == "single") ''
           ./configure.sh local