27 files changed, 357 insertions, 0 deletions
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix
new file mode 100644
index 0000000000..3fcf177aec
--- /dev/null
+++ b/dev/ci/nix/CoLoR.nix
@@ -0,0 +1,5 @@
+{ bignums }:
+
+{
+  coqBuildInputs = [ bignums ];
+}
diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix
new file mode 100644
index 0000000000..db1721e5f5
--- /dev/null
+++ b/dev/ci/nix/CompCert.nix
@@ -0,0 +1,7 @@
+{ ocamlPackages }:
+
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib menhir ];
+  configure = "./configure -ignore-coq-version x86_64-linux";
+  make = "make all check-proof";
+}
diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix
new file mode 100644
index 0000000000..0d22a6b91b
--- /dev/null
+++ b/dev/ci/nix/Corn.nix
@@ -0,0 +1,5 @@
+{ bignums, math-classes }:
+
+{
+  coqBuildInputs = [ bignums math-classes ];
+}
diff --git a/dev/ci/nix/Elpi.nix b/dev/ci/nix/Elpi.nix
new file mode 100644
index 0000000000..0a6ed20295
--- /dev/null
+++ b/dev/ci/nix/Elpi.nix
@@ -0,0 +1,4 @@
+{ ocamlPackages }:
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib elpi ];
+}
diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix
new file mode 100644
index 0000000000..45d688285e
--- /dev/null
+++ b/dev/ci/nix/GeoCoq.nix
@@ -0,0 +1,5 @@
+{ mathcomp }:
+{
+  coqBuildInputs = [ mathcomp ];
+  configure = "./configure.sh";
+}
diff --git a/dev/ci/nix/HoTT.nix b/dev/ci/nix/HoTT.nix
new file mode 100644
index 0000000000..dea0aeeb55
--- /dev/null
+++ b/dev/ci/nix/HoTT.nix
@@ -0,0 +1,6 @@
+{ autoconf, automake }:
+{
+  buildInputs = [ autoconf automake ];
+  configure = "./autogen.sh && ./configure";
+  make = "make all validate";
+}
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
new file mode 100644
index 0000000000..6f32abef95
--- /dev/null
+++ b/dev/ci/nix/README.md
@@ -0,0 +1,26 @@
+# Working on third-party developments with *this* version of Coq
+
+Aim: getting an environment suitable for working on a third-party development
+using the current version of Coq (i.e., built from the current state of this
+repository).
+
+Dive into such an environment, for the project `example` by running, from the
+root of this repository:
+
+    ./dev/ci/nix/shell example
+
+This will build Coq and the other dependencies of the `example` project, then
+open a shell with all these dependencies available (e.g., `coqtop` is in path).
+
+Additionally, three environment variables are set, to abstract over the
+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/VST.nix b/dev/ci/nix/VST.nix
new file mode 100644
index 0000000000..3e2629a0b6
--- /dev/null
+++ b/dev/ci/nix/VST.nix
@@ -0,0 +1,6 @@
+{}:
+
+rec {
+  make = "make IGNORECOQVERSION=true";
+  clean = "${make} clean";
+}
diff --git a/dev/ci/nix/bedrock2.nix b/dev/ci/nix/bedrock2.nix
new file mode 100644
index 0000000000..552d9297e2
--- /dev/null
+++ b/dev/ci/nix/bedrock2.nix
@@ -0,0 +1,5 @@
+{}:
+{
+  configure = "git submodule update --init --recursive";
+  clean = "(cd deps/bbv && make clean); (cd deps/riscv-coq && make clean); (cd compiler && make clean); (cd bedrock2 && make clean)";
+}
diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
new file mode 100644
index 0000000000..1d931c858e
--- /dev/null
+++ b/dev/ci/nix/bignums.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages }:
+
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+}
diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix
new file mode 100644
index 0000000000..b610790f61
--- /dev/null
+++ b/dev/ci/nix/coq.nix
@@ -0,0 +1,8 @@
+{ stdenv, callPackage, branch, wd }:
+
+let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version = "8.9"; }; in
+
+coq.overrideAttrs (o: {
+  name = "coq-local-${branch}";
+  src = fetchGit "${wd}";
+})
diff --git a/dev/ci/nix/coq_dpdgraph.nix b/dev/ci/nix/coq_dpdgraph.nix
new file mode 100644
index 0000000000..611e2fcca5
--- /dev/null
+++ b/dev/ci/nix/coq_dpdgraph.nix
@@ -0,0 +1,7 @@
+{ autoconf, ocamlPackages }:
+
+{
+  buildInputs = [ autoconf ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ocamlgraph ]);
+  configure = "autoconf && ./configure";
+  make = "make all test-suite";
+}
diff --git a/dev/ci/nix/cross_crypto.nix b/dev/ci/nix/cross_crypto.nix
new file mode 100644
index 0000000000..98f74f9474
--- /dev/null
+++ b/dev/ci/nix/cross_crypto.nix
@@ -0,0 +1,5 @@
+{}:
+{
+  configure = "git submodule update --init --recursive";
+  clean = "make cleanall";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
new file mode 100644
index 0000000000..17070e66ee
--- /dev/null
+++ b/dev/ci/nix/default.nix
@@ -0,0 +1,115 @@
+{ pkgs ? import ../../nixpkgs.nix {}
+, branch
+, wd
+, project ? "xyz"
+, withCoq ? true
+, bn ? "master"
+}:
+
+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 ssreflect = coqPackages.ssreflect.overrideAttrs (o: {
+  inherit (mathcomp) src;
+  }); in
+
+let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master";
+  }); in
+
+let simple-io =
+  (coqPackages.simple-io.override { inherit coq-ext-lib; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/Lysxia/coq-simple-io/tarball/master";
+  }); 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 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 stdpp = coqPackages.stdpp.overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2";
+  }); in
+
+let iris = (coqPackages.iris.override { inherit coq stdpp; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2";
+    propagatedBuildInputs = [ stdpp ];
+  }); in
+
+let unicoq = callPackage ./unicoq { inherit coq; }; in
+
+let callPackage = newScope { inherit coq
+  bignums coq-ext-lib coqprime corn iris math-classes
+  mathcomp simple-io ssreflect stdpp 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 {};
+  formal-topology = callPackage ./formal-topology.nix {};
+  GeoCoq = callPackage ./GeoCoq.nix {};
+  HoTT = callPackage ./HoTT.nix {};
+  iris = callPackage ./iris.nix {};
+  lambda-rust = callPackage ./lambda-rust.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
+
+if !builtins.hasAttr project projects
+then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}."
+else
+
+let prj = projects."${project}"; in
+
+let inherit (stdenv.lib) optional optionals; in
+
+stdenv.mkDerivation {
+  name = "shell-for-${project}-in-${branch}";
+
+  buildInputs =
+    optional withCoq coq
+  ++ (prj.buildInputs or [])
+  ++ optionals withCoq (prj.coqBuildInputs or [])
+  ;
+
+  configure = prj.configure or "true";
+  make = prj.make or "make";
+  clean = prj.clean or "make clean";
+
+}
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
new file mode 100644
index 0000000000..0f0ee91387
--- /dev/null
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -0,0 +1,6 @@
+{ coqprime }:
+{
+  coqBuildInputs = [ coqprime ];
+  configure = "git submodule update --init --recursive && ulimit -s 32768";
+  make = "make new-pipeline c-files";
+}
diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix
new file mode 100644
index 0000000000..3248665579
--- /dev/null
+++ b/dev/ci/nix/fiat_crypto_legacy.nix
@@ -0,0 +1,6 @@
+{}:
+
+{
+  configure = "./etc/ci/remove_autogenerated.sh";
+  make = "make print-old-pipeline-lite old-pipeline-lite lite-display";
+}
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
new file mode 100644
index 0000000000..e153043557
--- /dev/null
+++ b/dev/ci/nix/flocq.nix
@@ -0,0 +1,7 @@
+{ autoconf, automake }:
+
+{
+  buildInputs = [ autoconf automake ];
+  configure = "./autogen.sh && ./configure";
+  make = "./remake";
+}
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/iris.nix b/dev/ci/nix/iris.nix
new file mode 100644
index 0000000000..b55cccc7c6
--- /dev/null
+++ b/dev/ci/nix/iris.nix
@@ -0,0 +1,4 @@
+{ stdpp }:
+{
+  coqBuildInputs = [ stdpp ];
+}
diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix
new file mode 100644
index 0000000000..0d07c3028a
--- /dev/null
+++ b/dev/ci/nix/lambda-rust.nix
@@ -0,0 +1,4 @@
+{ iris }:
+{
+  coqBuildInputs = [ iris ];
+}
diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix
new file mode 100644
index 0000000000..8edc3c8358
--- /dev/null
+++ b/dev/ci/nix/math_classes.nix
@@ -0,0 +1,6 @@
+{ bignums }:
+
+{
+  coqBuildInputs = [ bignums ];
+  configure = "./configure.sh";
+}
diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix
new file mode 100644
index 0000000000..4acc326c02
--- /dev/null
+++ b/dev/ci/nix/mtac2.nix
@@ -0,0 +1,6 @@
+{ coq, unicoq }:
+{
+  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
new file mode 100644
index 0000000000..2341bb3173
--- /dev/null
+++ b/dev/ci/nix/oddorder.nix
@@ -0,0 +1,4 @@
+{ mathcomp }:
+{
+  coqBuildInputs = [ mathcomp ];
+}
diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix
new file mode 100644
index 0000000000..b90f1e4f88
--- /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 simple-io ];
+}
diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
new file mode 100755
index 0000000000..a5f8ee8f54
--- /dev/null
+++ b/dev/ci/nix/shell
@@ -0,0 +1,26 @@
+#!/usr/bin/env sh
+
+## This file should be run from the root of the Coq source tree
+
+BRANCH=$(git rev-parse --abbrev-ref HEAD)
+echo "Branch: $BRANCH in $PWD"
+
+if [ "$#" -ne 1 ]; then
+  PROJECT=""
+else
+  PROJECT="--argstr project $1"
+fi
+
+if [ "$BN" ]; then
+  BN="--argstr bn ${BN}"
+else
+  BN=""
+fi
+
+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/default.nix b/dev/ci/nix/unicoq/default.nix
new file mode 100644
index 0000000000..54c67ac0fd
--- /dev/null
+++ b/dev/ci/nix/unicoq/default.nix
@@ -0,0 +1,26 @@
+{ stdenv, writeText, coq }:
+
+let META = writeText "META" ''
+  archive(native) = "unicoq.cmxa"
+  plugin(native) = "unicoq.cmxs"
+''; in
+
+
+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 = ''
+    cp ${META} META
+    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