From bb1ad2a59f0c9c6b62a1c70023a9ee31866b9a01 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 29 Nov 2018 17:01:47 +0000
Subject: [Nix-ci] Add formal-topology

---
 dev/ci/nix/default.nix | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'dev/ci/nix/default.nix')

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 4acfae48e4..ac4894dfd3 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -2,7 +2,7 @@
 , branch
 , wd
 , project ? "xyz"
-, bn ? "release"
+, bn ? "master"
 }:
 
 with pkgs;
@@ -28,9 +28,14 @@ let math-classes =
     src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
   }); 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.nix { inherit coq; }; in
 
-let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
+let callPackage = newScope { inherit coq mathcomp bignums coqprime corn math-classes unicoq; }; in
 
 # Environments for building CI libraries with this Coq
 let projects = {
@@ -45,6 +50,7 @@ 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 {};
-- 
cgit v1.2.3


From 736a425208ef526412a961e97e157b44eea050c5 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 3 Dec 2018 13:18:50 +0000
Subject: [Nix-ci] Fix Unicoq

---
 dev/ci/nix/default.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci/nix/default.nix')

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index ac4894dfd3..35f44f8e84 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -33,7 +33,7 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
     src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
   }); in
 
-let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+let unicoq = callPackage ./unicoq { inherit coq; }; in
 
 let callPackage = newScope { inherit coq mathcomp bignums coqprime corn math-classes unicoq; }; in
 
-- 
cgit v1.2.3


From 43525f9ee12a40bf3ad2c2521832fd7fc3a658f8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 3 Dec 2018 15:31:52 +0000
Subject: [Nix-ci] Add QuickChick

---
 dev/ci/nix/default.nix | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'dev/ci/nix/default.nix')

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 35f44f8e84..2c6e5b37bc 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -16,6 +16,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
@@ -35,7 +40,10 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
 
 let unicoq = callPackage ./unicoq { inherit coq; }; in
 
-let callPackage = newScope { inherit coq mathcomp bignums coqprime corn 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 = {
@@ -57,6 +65,7 @@ let projects = {
   mathcomp = {};
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
+  quickchick = callPackage ./quickchick.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
-- 
cgit v1.2.3


From dec2994980e00eff72f474aed6da94b97c3d703a Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 24 Jan 2019 09:58:33 +0000
Subject: [nix-CI] Split the build inputs

Coq and the Coq libraries can now be excluded
(by setting the NOCOQ environment variable).
---
 dev/ci/nix/default.nix | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'dev/ci/nix/default.nix')

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";
-- 
cgit v1.2.3