Merge PR #9465: [Nix-CI] Add iris and lambda-rust

Reviewed-by: maximedenes

5 files changed, 31 insertions, 6 deletions

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 277e9ee08f..94e0a666e2 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -39,11 +39,21 @@ 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 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
-  mathcomp simple-io ssreflect unicoq;
+  bignums coq-ext-lib coqprime corn iris math-classes
+  mathcomp simple-io ssreflect stdpp unicoq;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -62,6 +72,8 @@ let projects = {
   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 {};
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/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
   '';
 }