aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorVincent Laporte2019-11-04 16:09:30 +0000
committerVincent Laporte2020-01-15 10:01:17 +0100
commit0a5d20dc9dbe8bb0bbebf87d5f482dcd6ce12120 (patch)
treec0d23ce522c592461fb6771f694d4b0d39b36900
parenta7e788403cae2c82bcb2b39f8576318a175ee788 (diff)
[Nix/CI] Update fiat_crypto
-rw-r--r--dev/ci/nix/fiat_crypto.nix6
1 files changed, 3 insertions, 3 deletions
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";
}