From cb89f2f623e28ac6c23330cb1b37622f93780088 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Jan 2019 15:00:04 +0000
Subject: [Nix-CI] Fix Unicoq

---
 dev/ci/nix/unicoq/META        |  2 --
 dev/ci/nix/unicoq/default.nix | 11 +++++++++--
 2 files changed, 9 insertions(+), 4 deletions(-)
 delete mode 100644 dev/ci/nix/unicoq/META

(limited to 'dev')

diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
deleted file mode 100644
index 30dd8b5559..0000000000
--- a/dev/ci/nix/unicoq/META
+++ /dev/null
@@ -1,2 +0,0 @@
-archive(native) = "unicoq.cmxa"
-plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix
index 36f40dbe33..54c67ac0fd 100644
--- a/dev/ci/nix/unicoq/default.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -1,4 +1,10 @@
-{ stdenv, coq }:
+{ 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";
@@ -12,8 +18,9 @@ stdenv.mkDerivation {
   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
+    install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
   '';
 }
-- 
cgit v1.2.3


From 2d3b3412cc29c21e7e3d1d1824f317ed14313992 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 4 Feb 2019 14:10:34 +0000
Subject: [Nix-CI] Add Iris

---
 dev/ci/nix/default.nix | 7 ++++++-
 dev/ci/nix/iris.nix    | 4 ++++
 2 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 dev/ci/nix/iris.nix

(limited to 'dev')

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 277e9ee08f..fe606568aa 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -39,11 +39,15 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
     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 unicoq = callPackage ./unicoq { inherit coq; }; in
 
 let callPackage = newScope { inherit coq
   bignums coq-ext-lib coqprime corn math-classes
-  mathcomp simple-io ssreflect unicoq;
+  mathcomp simple-io ssreflect stdpp unicoq;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -62,6 +66,7 @@ let projects = {
   formal-topology = callPackage ./formal-topology.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
+  iris = callPackage ./iris.nix {};
   math_classes = callPackage ./math_classes.nix {};
   mathcomp = {};
   mtac2 = callPackage ./mtac2.nix {};
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 ];
+}
-- 
cgit v1.2.3


From 4869260a47ea9d28174ed61e05bec7907dbaa0bb Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 4 Feb 2019 15:14:25 +0000
Subject: [Nix-CI] Add lambda-rust

---
 dev/ci/nix/default.nix     | 9 ++++++++-
 dev/ci/nix/lambda-rust.nix | 4 ++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 dev/ci/nix/lambda-rust.nix

(limited to 'dev')

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index fe606568aa..94e0a666e2 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -43,10 +43,16 @@ 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 math-classes
+  bignums coq-ext-lib coqprime corn iris math-classes
   mathcomp simple-io ssreflect stdpp unicoq;
 }; in
 
@@ -67,6 +73,7 @@ let projects = {
   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 {};
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 ];
+}
-- 
cgit v1.2.3