Merge PR #9394: [nix-ci] Maintenance

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: maximedenes

1 files changed, 26 insertions, 4 deletions

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 4acfae48e4..277e9ee08f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -2,7 +2,8 @@
 , branch
 , wd
 , project ? "xyz"
-, bn ? "release"
+, withCoq ? true
+, bn ? "master"
 }:
 
 with pkgs;
@@ -16,6 +17,11 @@ 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 ssreflect = coqPackages.ssreflect.overrideAttrs (o: {
+  inherit (mathcomp) src;
+  }); in
+let coq-ext-lib = coqPackages.coq-ext-lib; in
+let simple-io = coqPackages.simple-io; 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
@@ -28,9 +34,17 @@ let math-classes =
     src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
   }); in
 
-let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
+  }); in
+
+let unicoq = callPackage ./unicoq { inherit coq; }; in
 
-let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
+let callPackage = newScope { inherit coq
+  bignums coq-ext-lib coqprime corn math-classes
+  mathcomp simple-io ssreflect unicoq;
+}; in
 
 # Environments for building CI libraries with this Coq
 let projects = {
@@ -45,12 +59,14 @@ let projects = {
   fiat_crypto = callPackage ./fiat_crypto.nix {};
   fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
   flocq = callPackage ./flocq.nix {};
+  formal-topology = callPackage ./formal-topology.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
   math_classes = callPackage ./math_classes.nix {};
   mathcomp = {};
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
+  quickchick = callPackage ./quickchick.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
@@ -60,10 +76,16 @@ else
 
 let prj = projects."${project}"; in
 
+let inherit (stdenv.lib) optional optionals; in
+
 stdenv.mkDerivation {
   name = "shell-for-${project}-in-${branch}";
 
-  buildInputs = [ coq ] ++ (prj.buildInputs or []);
+  buildInputs =
+    optional withCoq coq
+  ++ (prj.buildInputs or [])
+  ++ optionals withCoq (prj.coqBuildInputs or [])
+  ;
 
   configure = prj.configure or "true";
   make = prj.make or "make";