aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/nix/default.nix7
-rw-r--r--dev/ci/nix/iris.nix4
2 files changed, 10 insertions, 1 deletions
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 ];
+}