From c713b0ed679d35cdb999c19aadb5b4914f7c1e0f Mon Sep 17 00:00:00 2001
From: Marco Maggesi <maggesi@math.unifi.it>
Date: Thu, 5 Nov 2009 15:08:12 +0000
Subject: [PATCH] Preliminary version of package ssreflect

Add expression for ssreflect, an extension to the Coq Proof Assistant.
Still has some clitches (see TODO in default.nix) but is usable anyway.


svn path=/nixpkgs/trunk/; revision=18145
---
 .../science/logic/ssreflect/default.nix       | 55 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  5 ++
 2 files changed, 60 insertions(+)
 create mode 100644 pkgs/applications/science/logic/ssreflect/default.nix

diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
new file mode 100644
index 000000000000..61901d545d7a
--- /dev/null
+++ b/pkgs/applications/science/logic/ssreflect/default.nix
@@ -0,0 +1,55 @@
+# TODO:
+# - ssrcoqide does not build successfully (missing coqide libraries in the coq installation).
+# - ssrcoq needs to be invoked with the explicit path to the ssreflect theory
+#   e.g.. ssrcoq -I /nix/store/rp09dlb2y2hpddb0xa7fyrgjlzb284ar-ssreflect-1.2/lib/coq/user-contrib/theories/
+
+{stdenv, fetchurl, ocaml, camlp5, coq}:
+
+let
+  pname = "ssreflect";
+  version = "1.2";
+  name = "${pname}-${version}";
+  webpage = http://www.msr-inria.inria.fr/Projects/math-components;
+in
+
+stdenv.mkDerivation {
+  inherit name;
+
+  src = fetchurl {
+    url = "${webpage}/${name}.tgz";
+    sha256 = "0800b085e6a0caec5093c6c02aacdd8dfd9cc282177e8586f14f9a9e15f64d0b";
+  };
+
+  buildInputs = [ ocaml camlp5 coq ];
+
+  preBuild = ''
+    coq_makefile -f Make -o Makefile
+    substituteInPlace Makefile \
+      --replace 'install -D $$i $(COQLIB)' 'install -D $$i '$out'/lib/coq'
+  '';
+
+  # this fails
+  /*
+  postBuild = ''
+    cd src
+    coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
+  '';
+  */
+
+  postInstall = ''
+    ensureDir $out/bin
+    #cp -a bin/ssrcoq bin/ssrcoqide $out/bin
+    cp -a bin/ssrcoq $out/bin
+  '';
+
+  meta = {
+    description = "Small Scale Reflection extension for Coq";
+    longDescription = ''
+      Small Scale Reflection (ssreflect) is an extension of the Coq Theorem
+      Prover which enable a formal proof methodology based on the pervasive
+      use of computation with symbolic representation
+    '';
+    homepage = webpage;
+    license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index faafef4861de..596efb6946d8 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -8257,6 +8257,11 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  ssreflect = import ../applications/science/logic/ssreflect {
+    inherit stdenv fetchurl ocaml coq;
+    camlp5 = camlp5_transitional;
+  };
+
   ### SCIENCE / ELECTRONICS
 
   ngspice = import ../applications/science/electronics/ngspice {