Matita and its dependencies.

svn path=/nixpkgs/trunk/; revision=25328

3 files changed, 101 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/matita/Makefile.patch b/pkgs/applications/science/logic/matita/Makefile.patch
new file mode 100644
index 000000000000..64c9a13f2d07
--- /dev/null
+++ b/pkgs/applications/science/logic/matita/Makefile.patch
@@ -0,0 +1,11 @@
+--- matita-0.5.8/Makefile	2009-12-01 18:21:00.000000000 -0500
++++ matita-0.5.8/Makefile	2010-09-16 10:33:59.665461260 -0400
+@@ -38,7 +38,7 @@
+ uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d))
+ 
+ rec@%:
+-	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) DESTDIR=$(shell pwd)/$(DESTDIR)
++	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
+ 
+ # {{{ Distribution stuff
+ 
diff --git a/pkgs/applications/science/logic/matita/configure.patch b/pkgs/applications/science/logic/matita/configure.patch
new file mode 100644
index 000000000000..9a3bbbb13f52
--- /dev/null
+++ b/pkgs/applications/science/logic/matita/configure.patch
@@ -0,0 +1,36 @@
+--- zzz/matita-0.5.8/configure	2009-12-01 18:21:00.000000000 -0500
++++ matita-0.5.8/configure	2010-09-07 19:57:29.732139550 -0400
+@@ -1895,6 +1895,7 @@
+ # look for METAS dir
+ 
+ LIBSPATH="`pwd`/components"
++OLDCAMLPATH="$OCAMLPATH"
+ OCAMLPATH="$LIBSPATH/METAS"
+ 
+ # creating META.*
+@@ -1917,7 +1918,7 @@
+ gdome2 \
+ http \
+ lablgtk2 \
+-lablgtksourceview2.gtksourceview2 \
++lablgtk2.gtksourceview \
+ lablgtkmathview \
+ mysql \
+ netstring \
+@@ -1951,14 +1952,14 @@
+ $FINDLIB_CREQUIRES \
+ lablgtk2.glade \
+ lablgtkmathview \
+-lablgtksourceview2.gtksourceview2 \
++lablgtk2.gtksourceview \
+ helm-xmldiff \
+ "
+ for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
+ do
+   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5
+ $as_echo_n "checking for $r ocaml library... " >&6; }
+-  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
++  if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then
+     { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+ $as_echo "yes" >&6; }
+   else
diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix
new file mode 100644
index 000000000000..6ac672193e27
--- /dev/null
+++ b/pkgs/applications/science/logic/matita/default.nix
@@ -0,0 +1,54 @@
+{stdenv, fetchurl, ocaml, camlp5, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, lablgtkmathview, ocaml_mysql, ocaml_sqlite3, ocamlnet, ulex08, camlzip, ocaml_pcre }:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.5.8";
+  pname = "matita";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://matita.cs.unibo.it/FILES/${pname}-${version}.orig.tar.gz";
+    sha256 = "04sxklfak71khy1f07ks5c6163jbpxv6fmaw03fx8gwwlvpmzglh";
+  };
+
+  buildInputs = [ocaml camlp5 findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre ];
+
+  postPatch = ''
+    BASH=$(type -tp bash)
+    substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
+    substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
+    substituteInPlace configure --replace "ulex08" "ulex"
+    substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex"
+    substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex"
+    substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex"
+    substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex"
+    substituteInPlace configure --replace "zip" "camlzip"
+    substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip"
+    substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
+  '';
+
+  patches = [ ./configure.patch ./Makefile.patch ];
+
+  preConfigure = ''
+    # Setup for findlib.
+    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
+    RTDIR=$out/share/matita
+    export configureFlags="--with-runtime-dir=$RTDIR"
+  '';
+
+  postInstall = ''
+    ensureDir $out/bin
+    ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
+  '';
+
+  meta = {
+    homepage = http://matita.cs.unibo.it/;
+    description = "Matita is an experimental, interactive theorem prover";
+    license = "GPLv2+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}