Helpers for debugging external projects from CI

1 files changed, 72 insertions, 0 deletions

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
new file mode 100644
index 0000000000..4acfae48e4
--- /dev/null
+++ b/dev/ci/nix/default.nix
@@ -0,0 +1,72 @@
+{ pkgs ? import <nixpkgs> {}
+, branch
+, wd
+, project ? "xyz"
+, bn ? "release"
+}:
+
+with pkgs;
+
+# Coq from this directory
+let coq = callPackage ./coq.nix { inherit branch wd; }; in
+
+# Third-party libraries, built with this Coq
+let coqPackages = mkCoqPackages coq; in
+let mathcomp = coqPackages.mathcomp.overrideAttrs (o: {
+    name = "coq-git-mathcomp-git";
+    src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz;
+  }); in
+let bignums = coqPackages.bignums.overrideAttrs (o:
+    if bn == "release" then {} else
+    if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else
+    { src = fetchTarball bn; }
+  ); in
+let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in
+let math-classes =
+  (coqPackages.math-classes.override { inherit coq bignums; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
+  }); in
+
+let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+
+let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
+
+# Environments for building CI libraries with this Coq
+let projects = {
+  bedrock2 = callPackage ./bedrock2.nix {};
+  bignums = callPackage ./bignums.nix {};
+  CoLoR = callPackage ./CoLoR.nix {};
+  CompCert = callPackage ./CompCert.nix {};
+  coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+  Corn = callPackage ./Corn.nix {};
+  cross_crypto = callPackage ./cross_crypto.nix {};
+  Elpi = callPackage ./Elpi.nix {};
+  fiat_crypto = callPackage ./fiat_crypto.nix {};
+  fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
+  flocq = callPackage ./flocq.nix {};
+  GeoCoq = callPackage ./GeoCoq.nix {};
+  HoTT = callPackage ./HoTT.nix {};
+  math_classes = callPackage ./math_classes.nix {};
+  mathcomp = {};
+  mtac2 = callPackage ./mtac2.nix {};
+  oddorder = callPackage ./oddorder.nix {};
+  VST = callPackage ./VST.nix {};
+}; in
+
+if !builtins.hasAttr project projects
+then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}."
+else
+
+let prj = projects."${project}"; in
+
+stdenv.mkDerivation {
+  name = "shell-for-${project}-in-${branch}";
+
+  buildInputs = [ coq ] ++ (prj.buildInputs or []);
+
+  configure = prj.configure or "true";
+  make = prj.make or "make";
+  clean = prj.clean or "make clean";
+
+}