From 0c51a4ac98ecb43bc729588d0eb3df21481a4e05 Mon Sep 17 00:00:00 2001
From: Austin Seipp <aseipp@pobox.com>
Date: Thu, 1 May 2014 19:09:37 -0500
Subject: [PATCH] nixpkgs: add CompCert

Signed-off-by: Austin Seipp <aseipp@pobox.com>
---
 .../compilers/compcert/default.nix            | 24 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 ++
 2 files changed, 26 insertions(+)
 create mode 100644 pkgs/development/compilers/compcert/default.nix

diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix
new file mode 100644
index 000000000000..c181e34217ad
--- /dev/null
+++ b/pkgs/development/compilers/compcert/default.nix
@@ -0,0 +1,24 @@
+{ stdenv, fetchurl, coq, ocaml, gcc }:
+
+stdenv.mkDerivation rec {
+  name    = "compcert-${version}";
+  version = "2.2";
+
+  src = fetchurl {
+    url    = "http://compcert.inria.fr/release/${name}.tgz";
+    sha256 = "0zhqx9mixlsycckl6wq6yrd795byj1jz7m4njcgfv29cx33j1nrk";
+  };
+
+  buildInputs = [ coq ocaml ];
+
+  enableParallelBuilding = true;
+  configurePhase = "./configure -prefix $out -toolprefix ${gcc}/bin/ ia32-linux";
+
+  meta = {
+    description = "Formally verified C compiler";
+    homepage    = "http://compcert.inria.fr";
+    license     = stdenv.lib.licenses.inria;
+    platforms   = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 0a6ff055ff02..e416cd416828 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -2470,6 +2470,8 @@ let
 
   cmucl_binary = callPackage ../development/compilers/cmucl/binary.nix { };
 
+  compcert = callPackage_i686 ../development/compilers/compcert {};
+
   cryptol1 = lowPrio (callPackage ../development/compilers/cryptol/1.8.x.nix {});
   cryptol2 = haskellPackages.cryptol;