Merge PR #9394: [nix-ci] Maintenance

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

15 files changed, 111 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 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";
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
new file mode 100644
index 0000000000..53b9b1182b
--- /dev/null
+++ b/dev/ci/nix/formal-topology.nix
@@ -0,0 +1,4 @@
+{ 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
new file mode 100644
index 0000000000..46bf02ae3c
--- /dev/null
+++ b/dev/ci/nix/quickchick.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
+{
+  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
diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
new file mode 100644
index 0000000000..30dd8b5559
--- /dev/null
+++ b/dev/ci/nix/unicoq/META
@@ -0,0 +1,2 @@
+archive(native) = "unicoq.cmxa"
+plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq/default.nix
index 093c262cde..36f40dbe33 100644
--- a/dev/ci/nix/unicoq.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -4,8 +4,16 @@ stdenv.mkDerivation {
   name = "coq${coq.coq-version}-unicoq-0.0-git";
   src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
 
+  patches = [ ./unicoq-num.patch ];
+
   buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
 
   configurePhase = "coq_makefile -f Make -o Makefile";
   installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+  postInstall = ''
+    install -d $OCAMLFIND_DESTDIR
+    ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
+    install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
+  '';
 }
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
new file mode 100644
index 0000000000..6d96d94dfc
--- /dev/null
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -0,0 +1,44 @@
+commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b
+Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
+Date:   Thu Nov 29 08:59:22 2018 +0000
+
+    Make explicit dependency to num
+
+diff --git a/Make b/Make
+index 550dc6a..8aa1309 100644
+--- a/Make
++++ b/Make
+@@ -9,7 +9,7 @@ src/logger.ml
+ src/munify.mli
+ src/munify.ml
+ src/unitactics.mlg
+-src/unicoq.mllib
++src/unicoq.mlpack
+ theories/Unicoq.v
+ test-suite/munifytest.v
+ test-suite/microtests.v
+diff --git a/Makefile.local b/Makefile.local
+new file mode 100644
+index 0000000..88be365
+--- /dev/null
++++ b/Makefile.local
+@@ -0,0 +1 @@
++CAMLPKGS += -package num
+diff --git a/src/unicoq.mllib b/src/unicoq.mllib
+deleted file mode 100644
+index 2b84e2d..0000000
+--- a/src/unicoq.mllib
++++ /dev/null
+@@ -1,3 +0,0 @@
+-Logger
+-Munify
+-Unitactics
+diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
+new file mode 100644
+index 0000000..2b84e2d
+--- /dev/null
++++ b/src/unicoq.mlpack
+@@ -0,0 +1,3 @@
++Logger
++Munify
++Unitactics