diff options
| author | Vincent Laporte | 2019-11-04 16:09:30 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2020-01-15 10:01:17 +0100 |
| commit | 0a5d20dc9dbe8bb0bbebf87d5f482dcd6ce12120 (patch) | |
| tree | c0d23ce522c592461fb6771f694d4b0d39b36900 /dev | |
| parent | a7e788403cae2c82bcb2b39f8576318a175ee788 (diff) | |
[Nix/CI] Update fiat_crypto
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/nix/fiat_crypto.nix | 6 |
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"; } |