12 files changed, 33 insertions, 12 deletions
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix
index 4c5cfd83da..3fcf177aec 100644
--- a/dev/ci/nix/CoLoR.nix
+++ b/dev/ci/nix/CoLoR.nix
@@ -1,5 +1,5 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
 }
diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix
index 18c7750279..0d22a6b91b 100644
--- a/dev/ci/nix/Corn.nix
+++ b/dev/ci/nix/Corn.nix
@@ -1,5 +1,5 @@
 { bignums, math-classes }:
 
 {
-  buildInputs = [ bignums math-classes ];
+  coqBuildInputs = [ bignums math-classes ];
 }
diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix
index a86fb2c44a..45d688285e 100644
--- a/dev/ci/nix/GeoCoq.nix
+++ b/dev/ci/nix/GeoCoq.nix
@@ -1,5 +1,5 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
index 1685b084e9..6f32abef95 100644
--- a/dev/ci/nix/README.md
+++ b/dev/ci/nix/README.md
@@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after
 changing the working directory to the root of the sources of that project, the
 contents of these variables can be evaluated to respectively set-up, build, and
 clean the project.
+
+## Variant: nocoq
+
+The dependencies of the third-party developments are split into `buildInputs`
+and `coqBuildInputs`. The second list gathers the Coq libraries. In case you
+only want the non-coq dependencies (because you want to use Coq from your `PATH`),
+set the environment variable `NOCOQ` to some non-empty value.
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 2c6e5b37bc..277e9ee08f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -2,6 +2,7 @@
 , branch
 , wd
 , project ? "xyz"
+, withCoq ? true
 , bn ? "master"
 }:
 
@@ -75,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";
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 7b37e6e8e4..0f0ee91387 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
 { coqprime }:
 {
-  buildInputs = [ coqprime ];
+  coqBuildInputs = [ coqprime ];
   configure = "git submodule update --init --recursive && ulimit -s 32768";
   make = "make new-pipeline c-files";
 }
diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix
index 70ba541577..53b9b1182b 100644
--- a/dev/ci/nix/formal-topology.nix
+++ b/dev/ci/nix/formal-topology.nix
@@ -1,4 +1,4 @@
 { corn }:
 {
-  buildInputs = [ corn ];
+  coqBuildInputs = [ corn ];
 }
diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix
index b0fa2fe795..8edc3c8358 100644
--- a/dev/ci/nix/math_classes.nix
+++ b/dev/ci/nix/math_classes.nix
@@ -1,6 +1,6 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix
index 9a2353c5cf..4acc326c02 100644
--- a/dev/ci/nix/mtac2.nix
+++ b/dev/ci/nix/mtac2.nix
@@ -1,5 +1,6 @@
 { coq, unicoq }:
 {
-  buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+  buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ];
+  coqBuildInputs = [ unicoq ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix
index 3b8fdbab51..2341bb3173 100644
--- a/dev/ci/nix/oddorder.nix
+++ b/dev/ci/nix/oddorder.nix
@@ -1,4 +1,4 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
 }
diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix
index b057160cb8..46bf02ae3c 100644
--- a/dev/ci/nix/quickchick.nix
+++ b/dev/ci/nix/quickchick.nix
@@ -1,5 +1,5 @@
 { ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
 {
-  buildInputs = [ ssreflect coq-ext-lib simple-io ]
-  ++ (with ocamlPackages; [ ocaml findlib ocamlbuild num ]);
+  buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ];
+  coqBuildInputs = [ ssreflect coq-ext-lib simple-io ];
 }
diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
index 2e4462ed40..a5f8ee8f54 100755
--- a/dev/ci/nix/shell
+++ b/dev/ci/nix/shell
@@ -17,4 +17,10 @@ else
   BN=""
 fi
 
-nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN
+if [ "$NOCOQ" ]; then
+    NOCOQ="--arg withCoq false"
+else
+    NOCOQ=""
+fi
+
+nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ