aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/nix/CompCert.nix
diff options
context:
space:
mode:
authorVincent Laporte2018-09-14 14:27:39 +0000
committerVincent Laporte2018-11-12 16:10:20 +0000
commit7e014333c57bdede663e490743bc84f696764381 (patch)
treecb6a82dbb7e5014ac71f976cc05999099cd2820c /dev/ci/nix/CompCert.nix
parent040fdec17f7e70fdbef7d400be2dc0e1607a10fa (diff)
Helpers for debugging external projects from CI
Diffstat (limited to 'dev/ci/nix/CompCert.nix')
-rw-r--r--dev/ci/nix/CompCert.nix7
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix
new file mode 100644
index 0000000000..db1721e5f5
--- /dev/null
+++ b/dev/ci/nix/CompCert.nix
@@ -0,0 +1,7 @@
+{ ocamlPackages }:
+
+{
+ buildInputs = with ocamlPackages; [ ocaml findlib menhir ];
+ configure = "./configure -ignore-coq-version x86_64-linux";
+ make = "make all check-proof";
+}