Nix CI reverse dependency compatibility testing

.nix/config.nix

@@ -31,59 +31,28 @@
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "coq-dev";
+  default-bundle = "coq-8.19";
 
   # MetaCoq is expected to be compatible with a single coq version
   # The name of the bundle should finish with the coq version to use
   # cachedMake.sh
-  bundles."coq-dev" = {
+  bundles."coq-8.19" = {
+    coqPackages.coq.override.version = "8.19";
+    coqPackages.equations.override.version = "1.3+8.19";
 
-    ## You can override Coq and other Coq coqPackages
-    ## through the following attribute
-    coqPackages.coq.override.version = "master";
-    coqPackages.equations.override.version = "main";
+    # coqPackages.metacoq.main-job = true;
+    coqPackages.metacoq-utils.main-job = true;
 
-    ## In some cases, light overrides are not available/enough
-    ## in which case you can use either
-    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
-    # coqPackages.equations.overrideAttrs = o: <overrides>;
-    ## or a "long" overlay to put in `.nix/coq-overlays
-    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
-    ## to automatically retrieve the one from nixpkgs
-    ## if it exists and is correctly named/located
-
-    ## You can override Coq and other coqPackages
-    ## through the following attribute
-    ## If <ocaml-pkg> does not support light overrides,
-    ## you may use `overrideAttrs` or long overlays
-    ## located in `.nix/ocaml-overlays`
-    ## (there is no automation for this one)
-    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
-
-    ## You can also override packages from the nixpkgs toplevel
-    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
-    ## Or put an overlay in `.nix/overlays`
-
-    ## you may mark a package as a main CI job (one to take deps and
-    ## rev deps from) as follows
-    # coqPackages.<main-pkg>.main-job = true;
-    ## by default the current package and its shell attributes are main jobs
-
-    ## you may mark a package as a CI job as follows
-    #  coqPackages.<another-pkg>.job = "test";
-    ## It can then built through
-    ## nix-build --argstr bundle "default" --arg job "test";
-    ## in the absence of such a directive, the job "another-pkg" will
-    ## is still available, but will be automatically included in the CI
-    ## via the command genNixActions only if it is a dependency or a
-    ## reverse dependency of a job flagged as "main-job" (see above).
+    push-branches = ["coq-8.19"];
 
+    # Reverse dependencies
+    coqPackages.ElmExtraction.override.version = "coq-8.19";
+    coqPackages.RustExtraction.override.version = "coq-8.19";
   };
 
   ## Cachix caches to use in CI
   ## Below we list some standard ones
   cachix.coq = {};
-  # cachix.math-comp = {};
   cachix.coq-community = {};
 
   ## If you have write access to one of these caches you can

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"39243d0edb4cb0b872d299c4b128fe232f0d8101"
+"95ab8ac1ca273c4db485937e55b03ba48fb2accc"

.nix/coq-overlays/equations/default.nix

@@ -1,11 +1,15 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; (mkCoqDerivation {
+(mkCoqDerivation {
   pname = "equations";
   owner = "mattam82";
   repo = "Coq-Equations";
   inherit version;
-  defaultVersion = switch coq.coq-version [
+  defaultVersion = lib.switch coq.coq-version [
+    { case = "8.20"; out = "1.3.1+8.20"; }
+    { case = "8.19"; out = "1.3+8.19"; }
+    { case = "8.18"; out = "1.3+8.18"; }
+    { case = "8.17"; out = "1.3+8.17"; }
     { case = "8.16"; out = "1.3+8.16"; }
     { case = "8.15"; out = "1.3+8.15"; }
     { case = "8.14"; out = "1.3+8.14"; }
@@ -54,14 +58,22 @@ with lib; (mkCoqDerivation {
     release."1.3+8.15".sha256         = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k";
     release."1.3+8.16".rev            = "v1.3-8.16";
     release."1.3+8.16".sha256         = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE=";
+    release."1.3+8.17".rev            = "v1.3-8.17";
+    release."1.3+8.17".sha256         = "sha256-yNotSIxFkhTg3reZIchGQ7cV9WmTJ7p7hPfKGBiByDw=";
+    release."1.3+8.18".rev            = "v1.3-8.18";
+    release."1.3+8.18".sha256         = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao=";
+    release."1.3+8.19".rev            = "v1.3-8.19";
+    release."1.3+8.19".sha256         = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk=";
+    release."1.3.1+8.20".rev          = "v1.3.1-8.20";
+    release."1.3.1+8.20".sha256       = "sha256-u8LB1KiACM5zVaoL7dSdHYvZgX7pf30VuqtjLLGuTzc=";
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     homepage = "https://mattam82.github.io/Coq-Equations/";
-    description = "A plugin for Coq to add dependent pattern-matching";
+    description = "Plugin for Coq to add dependent pattern-matching";
     maintainers = with maintainers; [ jwiegley ];
   };
 }).overrideAttrs (o: {
-  preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
+  preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
 })

.nix/coq-overlays/metacoq/default.nix

@@ -1,19 +1,22 @@
-{ lib, fetchzip,
-  mkCoqDerivation, recurseIntoAttrs,  single ? false,
-  coqPackages, coq, equations, version ? null }@args:
-with builtins // lib;
+{ lib,
+  mkCoqDerivation, single ? false,
+  coq, equations, version ? null }@args:
+
 let
   repo  = "metacoq";
   owner = "MetaCoq";
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = lib.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"; }
-      { case = "8.14"; out = "1.0-8.14"; }
-      { case = "8.15"; out = "1.0-8.15"; }
-      { case = "8.16"; out = "1.0-8.16"; }
-      { case = "dev"; out = "dev"; }
+      { 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.3.1-8.17"; }
+      { case = "8.18"; out = "1.3.1-8.18"; }
+      { case = "8.19"; out = "1.3.2-8.19"; }
+      { case = "8.20"; out = "1.3.2-8.20"; }
     ] null;
   release = {
     "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
@@ -22,66 +25,107 @@ let
     "1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0=";
     "1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k=";
     "1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o=";
+    "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=";
+    "1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc=";
+    "1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY=";
+    "1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64=";
+    "1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA=";
+    "1.3.2-8.20".sha256 = "sha256-4J7Ly4Fc2E/I6YqvzTLntVVls5t94OUOjVMKJyyJdw8=";
   };
   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" "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 = if package == "single" then []
-        else map metacoq_ (head (splitList (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 = ''
           mkdir all
           echo "all:" > all/Makefile
           echo "install:" >> all/Makefile
-        '' ;
+        '';
       derivation = (mkCoqDerivation ({
         inherit version pname defaultVersion release releaseRev repo owner;
 
         mlPlugin = true;
         propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
 
-        patchPhase =  ''
+        patchPhase = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" 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
+          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 + ''
+        configurePhase = lib.optionalString (package == "all") pkgallMake + ''
           touch ${pkgpath}/metacoq-config
-        '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
+        '' + 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
-        '' + optionalString (package == "single") ''
+        '' + lib.optionalString (package == "single") ''
           ./configure.sh local
         '';
 
         preBuild = ''
           cd ${pkgpath}
-        '' ;
+        '';
 
         meta = {
           homepage    = "https://metacoq.github.io/";
-          license     = licenses.mit;
-          maintainers = with maintainers; [ cohencyril ];
+          license     = lib.licenses.mit;
+          maintainers = with lib.maintainers; [ cohencyril ];
         };
-      } // optionalAttrs (package != "single")
-        { passthru = genAttrs packages metacoq_; })
-     ).overrideAttrs (o:
-       let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" ||
-                                      (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
-       in
-       {
-         propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
-       });
-    in derivation;
+      } // lib.optionalAttrs (package != "single")
+        { 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")) ;
+        in
+          {
+            propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
+          });
+      # 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")

default.nix

@@ -5,8 +5,7 @@
 }@args:
 let auto = fetchGit {
   url = "https://github.com/coq-community/coq-nix-toolbox.git";
-  allRefs = true ;
-  # ref = "master";
+  ref = "master";
   rev = import .nix/coq-nix-toolbox.nix;
 };
 in