aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorThéo Zimmermann2020-01-15 10:54:03 +0100
committerThéo Zimmermann2020-01-15 10:54:03 +0100
commita8cb0bb1cbdf304da81dc292c9fddf361207142e (patch)
treecdbb6e7637137879f956c00cf9b9f382e0e76752 /dev/ci
parenta7e788403cae2c82bcb2b39f8576318a175ee788 (diff)
parentc8d2da3db29ada93ed46a68dd789ccf16f22401c (diff)
Merge PR #11401: [nix] Dune-2 and other improvements
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/nix/default.nix17
-rw-r--r--dev/ci/nix/fiat_crypto.nix6
-rw-r--r--dev/ci/nix/verdi-raft.nix5
3 files changed, 24 insertions, 4 deletions
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index a9cc91170f..f08a08531f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; })
let unicoq = callPackage ./unicoq { inherit coq; }; in
+let StructTact = coqPackages.StructTact.overrideAttrs (o: {
+ src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master";
+ }); in
+
+let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; })
+ .overrideAttrs (o: {
+ src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master";
+ }); in
+
+let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; })
+ .overrideAttrs (o: {
+ src = fetchTarball "https://github.com/uwplse/verdi/tarball/master";
+ }); in
+
let callPackage = newScope { inherit coq
bignums coq-ext-lib coqprime corn iris math-classes
- mathcomp simple-io ssreflect stdpp unicoq;
+ mathcomp simple-io ssreflect stdpp unicoq Verdi;
}; in
# Environments for building CI libraries with this Coq
@@ -89,6 +103,7 @@ let projects = {
mtac2 = callPackage ./mtac2.nix {};
oddorder = callPackage ./oddorder.nix {};
quickchick = callPackage ./quickchick.nix {};
+ verdi-raft = callPackage ./verdi-raft.nix {};
VST = callPackage ./VST.nix {};
}; in
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 0f0ee91387..1105fba7a6 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
-{ coqprime }:
+{ ocamlPackages }:
{
- coqBuildInputs = [ coqprime ];
+ buildInputs = with ocamlPackages; [ ocaml findlib ];
configure = "git submodule update --init --recursive && ulimit -s 32768";
- make = "make new-pipeline c-files";
+ make = "make c-files printlite lite && make -j 1 coq";
}
diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix
new file mode 100644
index 0000000000..6a98f4ef47
--- /dev/null
+++ b/dev/ci/nix/verdi-raft.nix
@@ -0,0 +1,5 @@
+{ Verdi }:
+{
+ coqBuildInputs = [ Verdi ];
+ configure = "./configure";
+}