Matita and its dependencies.

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

25 files changed, 780 insertions, 25 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 ];
+  };
+}
diff --git a/pkgs/development/libraries/gdome2/default.nix b/pkgs/development/libraries/gdome2/default.nix
new file mode 100644
index 000000000000..415a98029cc6
--- /dev/null
+++ b/pkgs/development/libraries/gdome2/default.nix
@@ -0,0 +1,25 @@
+{stdenv, fetchurl, pkgconfig, glib, libxml2, gtkdoc}:
+
+let
+  pname = "gdome2";
+  version = "0.8.1";
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://gdome2.cs.unibo.it/tarball/${pname}-${version}.tar.gz";
+    sha256 = "0hyms5s3hziajp3qbwdwqjc2xcyhb783damqg8wxjpwfxyi81fzl";
+  };
+
+  buildInputs = [pkgconfig glib libxml2 gtkdoc];
+  propagatedBuildInputs = [glib libxml2];
+
+  meta = {
+    homepage = http://gdome2.cs.unibo.it/;
+    description = "DOM C library developped for the Gnome project";
+    license = "LGPLv2.1+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/libraries/gtkmathview/default.nix b/pkgs/development/libraries/gtkmathview/default.nix
new file mode 100644
index 000000000000..eaccf2fb08bc
--- /dev/null
+++ b/pkgs/development/libraries/gtkmathview/default.nix
@@ -0,0 +1,27 @@
+{stdenv, fetchurl, pkgconfig, gtk, t1lib, glib, libxml2, popt, gmetadom ? null }:
+
+let
+  pname = "gtkmathview";
+  version = "0.8.0";
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://helm.cs.unibo.it/mml-widget/sources/${pname}-${version}.tar.gz";
+    sha256 = "0hwcamf5fi35frg7q6kgisc9v0prqbhsplb2gl55cg3av9sh3hqx";
+  };
+
+  buildInputs = [pkgconfig gtk t1lib glib gmetadom libxml2 popt];
+  propagatedBuildInputs = [gtk t1lib];
+
+  patches = [ ./gcc-4.3-build-fixes.patch ./gcc-4.4-build-fixes.patch ];
+
+  meta = {
+    homepage = http://helm.cs.unibo.it/mml-widget/;
+    description = "GtkMathView is a C++ rendering engine for MathML documents";
+    license = "LGPLv3+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/libraries/gtkmathview/gcc-4.3-build-fixes.patch b/pkgs/development/libraries/gtkmathview/gcc-4.3-build-fixes.patch
new file mode 100644
index 000000000000..14ad594b38b8
--- /dev/null
+++ b/pkgs/development/libraries/gtkmathview/gcc-4.3-build-fixes.patch
@@ -0,0 +1,74 @@
+From: Stefano Zacchiroli <zack@upsilon.cc>
+Date: Fri, 11 Dec 2009 12:58:56 +0100
+Subject: [PATCH] gcc 4.3 build fixes
+
+---
+ mathmlps/main.cc                    |    1 +
+ mathmlsvg/SMS.cc                    |    1 +
+ mathmlsvg/main.cc                   |    1 +
+ src/backend/ps/T1_FontDataBase.cc   |    2 +-
+ src/engine/mathml/mathVariantAux.cc |    1 +
+ 5 files changed, 5 insertions(+), 1 deletions(-)
+
+diff --git a/mathmlps/main.cc b/mathmlps/main.cc
+index cc6cd1c..48339af 100644
+--- a/mathmlps/main.cc
++++ b/mathmlps/main.cc
+@@ -19,6 +19,7 @@
+ #include <config.h>
+ 
+ #include <cassert>
++#include <cstring>
+ #include <fstream>
+ 
+ #include <popt.h>
+diff --git a/mathmlsvg/SMS.cc b/mathmlsvg/SMS.cc
+index a76266e..be7add8 100644
+--- a/mathmlsvg/SMS.cc
++++ b/mathmlsvg/SMS.cc
+@@ -18,6 +18,7 @@
+ 
+ #include <config.h>
+ 
++#include <cstring>
+ #include <sstream>
+ #include "defs.h"
+ #include "AbstractLogger.hh"
+diff --git a/mathmlsvg/main.cc b/mathmlsvg/main.cc
+index 259d67e..c49e8ac 100644
+--- a/mathmlsvg/main.cc
++++ b/mathmlsvg/main.cc
+@@ -19,6 +19,7 @@
+ #include <config.h>
+ 
+ #include <cassert>
++#include <cstring>
+ #include <fstream>
+ 
+ #include <popt.h>
+diff --git a/src/backend/ps/T1_FontDataBase.cc b/src/backend/ps/T1_FontDataBase.cc
+index b6490eb..3dd436c 100644
+--- a/src/backend/ps/T1_FontDataBase.cc
++++ b/src/backend/ps/T1_FontDataBase.cc
+@@ -19,7 +19,7 @@
+ #include <t1lib.h>
+ #include <config.h>
+ #include <map>
+-#include <string>
++#include <cstring>
+ #include <stdlib.h>
+ #include <iostream>
+ #include <list>
+diff --git a/src/engine/mathml/mathVariantAux.cc b/src/engine/mathml/mathVariantAux.cc
+index 736acc1..dcf1826 100644
+--- a/src/engine/mathml/mathVariantAux.cc
++++ b/src/engine/mathml/mathVariantAux.cc
+@@ -19,6 +19,7 @@
+ #include <config.h>
+ 
+ #include <cassert>
++#include <cstring>
+ 
+ #include "mathVariantAux.hh"
+ 
+-- 
diff --git a/pkgs/development/libraries/gtkmathview/gcc-4.4-build-fixes.patch b/pkgs/development/libraries/gtkmathview/gcc-4.4-build-fixes.patch
new file mode 100644
index 000000000000..0ebd31ef2a78
--- /dev/null
+++ b/pkgs/development/libraries/gtkmathview/gcc-4.4-build-fixes.patch
@@ -0,0 +1,21 @@
+From: Stefano Zacchiroli <zack@upsilon.cc>
+Date: Fri, 11 Dec 2009 13:26:26 +0100
+Subject: [PATCH] gcc 4.4 build fixes
+
+---
+ src/common/AbstractLogger.cc |    1 +
+ 1 files changed, 1 insertions(+), 0 deletions(-)
+
+diff --git a/src/common/AbstractLogger.cc b/src/common/AbstractLogger.cc
+index 6f638fb..c5b7e3d 100644
+--- a/src/common/AbstractLogger.cc
++++ b/src/common/AbstractLogger.cc
+@@ -19,6 +19,7 @@
+ #include <config.h>
+ 
+ #include <stdarg.h>
++#include <stdio.h>
+ 
+ #include "AbstractLogger.hh"
+ 
+-- 
diff --git a/pkgs/development/libraries/lablgtk/default.nix b/pkgs/development/libraries/lablgtk/default.nix
deleted file mode 100644
index 4b223ce05ef8..000000000000
--- a/pkgs/development/libraries/lablgtk/default.nix
+++ /dev/null
@@ -1,21 +0,0 @@
-{stdenv, fetchurl, ocaml, pkgconfig, gtk, libgnomecanvas}:
-
-stdenv.mkDerivation (rec {
-  version = "2.14.2";
-  name = "lablgtk-${version}";
-  src = fetchurl {
-    url = "http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/${name}.tar.gz";
-    sha256 = "1fnh0amm7lwgyjdhmlqgsp62gwlar1140425yc1j6inwmgnsp0a9";
-  };
-
-  buildInputs = [ocaml pkgconfig gtk libgnomecanvas];
-
-  configureFlags = "--with-libdir=$(out)/lib/ocaml";
-  buildFlags = "world";
-  meta = {
-    platforms = ocaml.meta.platforms;
-    maintainers = [
-      stdenv.lib.maintainers.z77z
-    ];
-  };
-})
diff --git a/pkgs/development/ocaml-modules/camlzip/META b/pkgs/development/ocaml-modules/camlzip/META
index 72f5a3b8bd02..44c5168ae518 100644
--- a/pkgs/development/ocaml-modules/camlzip/META
+++ b/pkgs/development/ocaml-modules/camlzip/META
@@ -1,6 +1,6 @@
 version="@VERSION@"
 description="reading and writing ZIP, JAR and GZIP files"
 requires="unix"
-archive(byte)="camlzip.cma"
-archive(native)="camlzip.cmxa"
+archive(byte)="zip.cma"
+archive(native)="zip.cmxa"
 linkopts = ""
diff --git a/pkgs/development/ocaml-modules/expat/default.nix b/pkgs/development/ocaml-modules/expat/default.nix
new file mode 100644
index 000000000000..b2702a5cade6
--- /dev/null
+++ b/pkgs/development/ocaml-modules/expat/default.nix
@@ -0,0 +1,51 @@
+{stdenv, fetchurl, ocaml, findlib, ounit, expat}:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.9.1";
+  pname = "ocaml-expat";
+  testcase = fetchurl {
+    url = "http://www.w3.org/TR/1998/REC-xml-19980210.xml";
+    sha256 = "00a3gsfvlkdhmcbziqhvpvy1zmcgbcihfqwcvl6ay03zf7gvw0k1";
+  };
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://www.xs4all.nl/~mmzeeman/ocaml/${pname}-${version}.tar.gz";
+    sha256 = "16n2j3y0jc9xgqyshw9plrwqnjiz30vnpbhahmgxlidbycw8rgjz";
+  };
+
+  buildInputs = [ocaml findlib ounit expat];
+
+  createFindlibDestdir = true;
+
+  patches = [ ./unittest.patch ];
+
+  postPatch = ''
+    substituteInPlace "unittest.ml" \
+      --replace "/home/maas/xml-samples/REC-xml-19980210.xml.txt" "${testcase}"
+    substituteInPlace Makefile --replace "EXPAT_LIBDIR=/usr/local/lib" "EXPAT_LIBDIR=${expat}/lib" \
+    substituteInPlace Makefile --replace "EXPAT_INCDIR=/usr/local/include" "EXPAT_INCDIR=${expat}/include" \
+  '';
+
+  configurePhase = "true";  	# Skip configure
+
+  buildPhase = ''
+    make all allopt
+  '';
+
+  doCheck = true;
+
+  checkTarget = "testall";
+
+  meta = {
+    homepage = http://www.xs4all.nl/~mmzeeman/ocaml/;
+    description = "An ocaml wrapper for the Expat XML parsing library";
+    license = "MIT/X11";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/expat/unittest.patch b/pkgs/development/ocaml-modules/expat/unittest.patch
new file mode 100644
index 000000000000..489b745c503a
--- /dev/null
+++ b/pkgs/development/ocaml-modules/expat/unittest.patch
@@ -0,0 +1,15 @@
+--- old/Makefile	2005-03-13 09:00:29.000000000 -0500
++++ new/Makefile	2010-08-26 14:20:34.515785557 -0400
+@@ -67,10 +67,10 @@
+ testall: test testopt
+ .PHONY: test
+ test: unittest 	
+-	./unittest
++	LD_LIBRARY_PATH=. ./unittest
+ .PHONY: testopt
+ testopt: unittest.opt
+-	./unittest.opt
++	LD_LIBRARY_PATH=. ./unittest.opt
+ unittest: all unittest.ml
+ 	$(OCAMLFIND) ocamlc -o unittest -package oUnit -ccopt -L. -linkpkg \
+ 	$(ARCHIVE) unittest.ml
diff --git a/pkgs/development/ocaml-modules/gmetadom/default.nix b/pkgs/development/ocaml-modules/gmetadom/default.nix
new file mode 100644
index 000000000000..4d46bda243f3
--- /dev/null
+++ b/pkgs/development/ocaml-modules/gmetadom/default.nix
@@ -0,0 +1,36 @@
+{stdenv, fetchurl, ocaml, findlib, gdome2, libxslt, pkgconfig}:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.2.6";
+  pname = "gmetadom";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "mirror://sourceforge/project/${pname}/${pname}/${version}/${pname}-${version}.tar.gz";
+    sha256 = "0skmlv0pnqvg99wzzzi1h4zhwzd82xg7xpkj1kwpfy7bzinjh7ig";
+  };
+
+  patches = [ ./gcc-4.3.dpatch ];
+
+  dontDisableStatic = true;
+
+  preConfigure=''
+    configureFlags="--with-ocaml-lib-prefix=$out/lib/ocaml/${ocaml_version}/site-lib"
+  '';
+
+
+  buildInputs = [ocaml findlib pkgconfig gdome2 libxslt];
+  propagatedBuildInputs = [gdome2];
+
+  meta = {
+    homepage = http://gmetadom.sourceforge.net/;
+    description = "GMetaDOM is a collection of librares, each library providing a DOM implementation";
+    license = "LGPLv2.1+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/gmetadom/gcc-4.3.dpatch b/pkgs/development/ocaml-modules/gmetadom/gcc-4.3.dpatch
new file mode 100644
index 000000000000..d8d1d4631632
--- /dev/null
+++ b/pkgs/development/ocaml-modules/gmetadom/gcc-4.3.dpatch
@@ -0,0 +1,18 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## gcc-4.3.dpatch by Stefano Zacchiroli <zack@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: ensure sources build with gcc-4.3
+
+@DPATCH@
+diff -urNad trunk~/src/shared/Traits.hh.in trunk/src/shared/Traits.hh.in
+--- trunk~/src/shared/Traits.hh.in	2003-01-14 12:41:55.000000000 +0100
++++ trunk/src/shared/Traits.hh.in	2008-05-01 15:45:39.000000000 +0200
+@@ -26,6 +26,7 @@
+  */
+ 
+ #include <string>
++#include <cstring>
+ 
+ #include "@DOM_NAMESPACE@Char.hh"
+ 
diff --git a/pkgs/development/ocaml-modules/http/default.nix b/pkgs/development/ocaml-modules/http/default.nix
new file mode 100644
index 000000000000..46398d26114b
--- /dev/null
+++ b/pkgs/development/ocaml-modules/http/default.nix
@@ -0,0 +1,39 @@
+{stdenv, fetchurl, ocaml_pcre, ocamlnet, ocaml, findlib}:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  pname = "ocaml-http";
+  version = "0.1.3";
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://upsilon.cc/~zack/hacking/software/${pname}/${pname}-${version}.tar.gz";
+    sha256 = "070xw033r4pk6f4l0wcknm75y9qm4mp622a4cgzmcfhm58v6kssn";
+  };
+
+  buildInputs = [ocaml_pcre ocamlnet ocaml findlib];
+
+  createFindlibDestdir = true;
+
+  prePatch = ''
+    BASH=$(type -tp bash)
+    echo $BASH
+    substituteInPlace Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
+  '';
+
+  configurePhase = "true";	# Skip configure phase
+
+  buildPhase = ''
+    make all opt
+  '';
+
+  meta = {
+    homepage = "http://upsilon.cc/~zack/hacking/software/ocaml-http/";
+    description = "do it yourself (OCaml) HTTP daemon";
+    license = "LGPLv2";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/lablgtk/META.patch b/pkgs/development/ocaml-modules/lablgtk/META.patch
new file mode 100644
index 000000000000..d2b7b500c69b
--- /dev/null
+++ b/pkgs/development/ocaml-modules/lablgtk/META.patch
@@ -0,0 +1,64 @@
+diff -ruN zzz/lablgtk-2.14.1/META lablgtk-2.14.1/META
+--- zzz/lablgtk-2.14.1/META	2009-02-12 21:39:14.000000000 -0500
++++ lablgtk-2.14.1/META	2010-09-07 19:48:06.454452726 -0400
+@@ -1,8 +1,52 @@
+-requires=""
+-version="2.12.0"
+-archive(byte)="lablgtk.cma"
+-archive(byte,init)="lablgtk.cma gtkInit.cmo"
+-archive(native)="lablgtk.cmxa"
+-archive(native,init)="lablgtk.cmxa gtkInit.cmx"
+-linkopts=""
+-directory="+lablgtk2"
++version="2.14.1"
++requires(mt) = "threads"
++requires(mt,mt_vm) = "threads.vm"
++requires(mt,mt_posix) = "threads.posix"
++archive(byte) = "lablgtk.cma"
++archive(native) = "lablgtk.cmxa"
++archive(byte,mt) += "gtkThread.cmo"
++archive(native,mt) += "gtkThread.cmx"
++
++package "init" (
++  requires = "lablgtk2"
++  archive(byte) = "gtkInit.cmo"
++  archive(native) = "gtkInit.cmx"
++)
++
++package "glade" (
++  requires = "lablgtk2"
++  archive(byte) = "lablglade.cma"
++  archive(native) = "lablglade.cmxa"
++)
++
++package "gtkspell" (
++  requires = "lablgtk2"
++  archive(byte) = "lablgtkspell.cma"
++  archive(native) = "lablgtkspell.cmxa"
++)
++
++package "gnomecanvas" (
++  archive(byte)	= "lablgnomecanvas.cma"
++  archive(native) = "lablgnomecanvas.cmxa"
++)
++
++package "gnomeui" (
++  archive(byte) = "lablgnomeui.cma"
++  archive(native) = "lablgnomeui.cmxa"
++)
++
++package "panel" (
++  archive(byte) = "lablpanel.cma"
++  archive(native) = "lablpanel.cmxa"
++)
++
++package "rsvg" (
++  archive(byte) = "lablrsvg.cma"
++  archive(native) = "lablrsvg.cmxa"
++)
++
++package "gtksourceview" (
++  requires = "lablgtk2"
++  archive(byte) = "lablgtksourceview2.cma"
++  archive(native) = "lablgtksourceview2.cmxa"
++)
diff --git a/pkgs/development/ocaml-modules/lablgtk/default.nix b/pkgs/development/ocaml-modules/lablgtk/default.nix
new file mode 100644
index 000000000000..8a51c216ab40
--- /dev/null
+++ b/pkgs/development/ocaml-modules/lablgtk/default.nix
@@ -0,0 +1,37 @@
+{stdenv, fetchurl, ocaml, findlib, pkgconfig, gtk, libgnomecanvas, libglade, gtksourceview}:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  pname = "lablgtk";
+  version = "2.14.2";
+in
+
+stdenv.mkDerivation (rec {
+  name = "${pname}-${version}";
+  src = fetchurl {
+    url = "http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/${name}.tar.gz";
+    sha256 = "1fnh0amm7lwgyjdhmlqgsp62gwlar1140425yc1j6inwmgnsp0a9";
+  };
+
+  buildInputs = [ocaml findlib pkgconfig gtk libgnomecanvas libglade gtksourceview];
+
+  patches = [ ./META.patch ];
+
+  configureFlags = "--with-libdir=$(out)/lib/ocaml/${ocaml_version}/site-lib";
+  buildFlags = "world";
+
+  postInstall = ''
+    ocamlfind install lablgtk2 META
+  '';
+
+  meta = {
+    platforms = ocaml.meta.platforms;
+    maintainers = [
+      stdenv.lib.maintainers.z77z
+      stdenv.lib.maintainers.roconnor
+    ];
+    homepage = http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html;
+    description = "LablGTK is is an Objective Caml interface to gtk+";
+    license = "LGPLv2.1+";
+  };
+})
diff --git a/pkgs/development/ocaml-modules/lablgtkmathview/configure.patch b/pkgs/development/ocaml-modules/lablgtkmathview/configure.patch
new file mode 100644
index 000000000000..b841e8f43822
--- /dev/null
+++ b/pkgs/development/ocaml-modules/lablgtkmathview/configure.patch
@@ -0,0 +1,14 @@
+--- configure	2010-09-02 10:58:16.128236964 -0400
++++ configure.old	2010-09-02 10:57:42.368111615 -0400
+@@ -1637,9 +1637,9 @@
+ echo "$as_me:$LINENO: result: $ac_cv_file__usr_include_caml_mlvalues_h" >&5
+ echo "${ECHO_T}$ac_cv_file__usr_include_caml_mlvalues_h" >&6
+ if test $ac_cv_file__usr_include_caml_mlvalues_h = yes; then
+-  OCAML_INCLUDE_DIR=/usr/include
++  OCAML_INCLUDE_DIR=/usr/include/caml
+ else
+-  OCAML_INCLUDE_DIR=$OCAML_LIB_DIR
++  OCAML_INCLUDE_DIR=$OCAML_LIB_DIR/caml
+ 
+ fi
+ 
diff --git a/pkgs/development/ocaml-modules/lablgtkmathview/default.nix b/pkgs/development/ocaml-modules/lablgtkmathview/default.nix
new file mode 100644
index 000000000000..13c25495cdc6
--- /dev/null
+++ b/pkgs/development/ocaml-modules/lablgtkmathview/default.nix
@@ -0,0 +1,40 @@
+{stdenv, fetchurl, pkgconfig, ocaml, findlib, gmetadom, gtkmathview, lablgtk }:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.7.2";
+  pname = "lablgtkmathview";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://helm.cs.unibo.it/mml-widget/sources/${pname}-${version}.tar.gz";
+    sha256 = "0rgrpgwrgphw106l1xawxir002b7rmzc23rcxhv8ib6rymp1divx";
+  };
+
+  buildInputs = [pkgconfig ocaml findlib gmetadom gtkmathview lablgtk];
+
+  createFindlibDestdir = true;
+
+  propagatedBuildInputs = [gtkmathview];
+
+  prePatch = ''
+    substituteInPlace Makefile.in --replace "PROPCC = @OCAML_LIB_DIR@" "PROPCC = ${lablgtk}/lib/ocaml/${ocaml_version}/site-lib"
+  '';
+
+  buildPhase = ''
+    ensureDir .test
+    make
+    make opt
+  '';
+
+  meta = {
+    homepage = http://helm.cs.unibo.it/mml-widget/;
+    description = "OCaml bindings for gtkmathview";
+    license = "LGPLv2+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/mysql/default.nix b/pkgs/development/ocaml-modules/mysql/default.nix
new file mode 100644
index 000000000000..32455fb4310c
--- /dev/null
+++ b/pkgs/development/ocaml-modules/mysql/default.nix
@@ -0,0 +1,42 @@
+{stdenv, fetchurl, ocaml, findlib, mysql}:
+
+# TODO: la versione stabile da' un errore di compilazione dovuto a
+# qualche cambiamento negli header .h
+# TODO: compilazione di moduli dipendenti da zip, ssl, tcl, gtk, gtk2
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  pname = "ocaml-mysql";
+  version = "1.0.4";
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://raevnos.pennmush.org/code/${pname}/${pname}-${version}.tar.gz";
+    sha256 = "17i5almar8qrhc9drq0cvlprxf9wi9szj5kh4gnz11l9al8i3lar";
+  };
+
+  buildInputs = [ocaml findlib mysql];
+
+  createFindlibDestdir = true;
+
+  propagatedbuildInputs = [mysql];
+
+  preConfigure = ''
+    export LDFLAGS="-L${mysql}/lib/mysql"
+  '';
+
+  buildPhase = ''
+    make
+    make opt
+  '';
+
+  meta = {
+    homepage = http://raevnos.pennmush.org/code/ocaml-mysql/;
+    description = "Bindings for interacting with MySQL databases from ocaml";
+    license = "LGPLv2.1+";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/ocamlnet/default.nix b/pkgs/development/ocaml-modules/ocamlnet/default.nix
index 07a781657b3f..e4dc43743f32 100644
--- a/pkgs/development/ocaml-modules/ocamlnet/default.nix
+++ b/pkgs/development/ocaml-modules/ocamlnet/default.nix
@@ -15,6 +15,8 @@ stdenv.mkDerivation {
 
   buildInputs = [ncurses ocaml findlib ocaml_pcre camlzip openssl ocaml_ssl];
 
+  createFindlibDestdir = true;
+
   dontAddPrefix = true;
 
   preConfigure = ''
diff --git a/pkgs/development/ocaml-modules/ulex/0.8/camlp5.patch b/pkgs/development/ocaml-modules/ulex/0.8/camlp5.patch
new file mode 100644
index 000000000000..2fa92527035e
--- /dev/null
+++ b/pkgs/development/ocaml-modules/ulex/0.8/camlp5.patch
@@ -0,0 +1,72 @@
+Author: Stefano Zacchiroli <zack@debian.org>
+Description: build (and install) using camlp5 instead of camlp4
+--- ulex0.8.orig/META
++++ ulex0.8/META
+@@ -1,5 +1,5 @@
+ version = "0.8"
+-requires = "camlp4"
++requires = "camlp5"
+ description = "Runtime support for ulex"
+ archive(byte) = "ulexing.cma"
+ archive(native) = "ulexing.cmxa"
+--- ulex0.8.orig/Makefile
++++ ulex0.8/Makefile
+@@ -20,7 +20,7 @@
+ 	ocamlopt -a -o ulexing.cmxa $(ULEXING)
+ 
+ pa_ulex.cma: $(ULEX)
+-	ocamlc -a -o pa_ulex.cma -pp 'camlp4o pa_extend.cmo q_MLast.cmo' -I +camlp4 $(ULEX)
++	ocamlc -a -o pa_ulex.cma -pp 'camlp5o pa_extend.cmo q_MLast.cmo' -I `camlp5 -where` $(ULEX)
+ 
+ pa_ulex.ml: pa_ulex.ml.src
+ 	ocaml mk_pa_ulex.ml
+@@ -29,14 +29,14 @@
+ 	rm -f *.cm* *~ test custom_ulexing *.o *.a *.html *.css pa_ulex.ml
+ 
+ view_test: pa_ulex.cma
+-	camlp4o ./pa_ulex.cma pr_o.cmo -sep "\n" test.ml
++	camlp5o ./pa_ulex.cma pr_o.cmo -sep "\n" test.ml
+ 
+ run_test: ulexing.cma pa_ulex.cma
+-	ocamlc -o test -pp 'camlp4o ./pa_ulex.cma' ulexing.cma test.ml
++	ocamlc -o test -pp 'camlp5o ./pa_ulex.cma' ulexing.cma test.ml
+ 	./test
+ 
+ custom_ulexing: ulexing.cma pa_ulex.cma
+-	ocamlc -o custom_ulexing -pp 'camlp4o ./pa_ulex.cma' ulexing.cma custom_ulexing.ml
++	ocamlc -o custom_ulexing -pp 'camlp5o ./pa_ulex.cma' ulexing.cma custom_ulexing.ml
+ 
+ 
+ doc:
+--- ulex0.8.orig/README
++++ ulex0.8/README
+@@ -142,7 +142,7 @@
+ 
+ Compilation of OCaml files with lexer specifications:
+ 
+-  ocamlfind ocamlc -c -package ulex -syntax camlp4o my_file.ml
++  ocamlfind ocamlc -c -package ulex -syntax camlp5o my_file.ml
+ 
+ When linking, you must also include the ulex package:
+   ocamlfind ocamlc -o my_prog -linkpkg -package ulex my_file.cmo
+--- ulex0.8.orig/mk_pa_ulex.ml
++++ ulex0.8/mk_pa_ulex.ml
+@@ -1,10 +1,4 @@
+ let s = float_of_string (String.sub (Sys.ocaml_version) 0 4) in
+-if (s < 3.09) then (
+   print_endline "Old camlp4 (loc)";
+   Sys.command "sed s/_loc/loc/ < pa_ulex.ml.src > pa_ulex.ml"
+-)
+-else  (
+-  print_endline "New camlp4 (_loc)";
+-  Sys.command "cp pa_ulex.ml.src pa_ulex.ml"
+-)
+ 
+--- ulex0.8.orig/pa_ulex.ml.src
++++ ulex0.8/pa_ulex.ml.src
+@@ -1,4 +1,4 @@
+-let _loc = (Lexing.dummy_pos,Lexing.dummy_pos)
++let _loc = Stdpp.dummy_loc
+ 
+ (* Named regexp *)
+ 
diff --git a/pkgs/development/ocaml-modules/ulex/0.8/default.nix b/pkgs/development/ocaml-modules/ulex/0.8/default.nix
new file mode 100644
index 000000000000..169f3bfad8c2
--- /dev/null
+++ b/pkgs/development/ocaml-modules/ulex/0.8/default.nix
@@ -0,0 +1,32 @@
+{stdenv, fetchurl, ocaml, findlib, camlp5 }:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.8";
+  pname = "ulex";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://www.cduce.org/download/old/${pname}-${version}.tar.gz";
+    sha256 = "19faabg8hzz155xlzmjwsl59d7slahb5m1l9zh1fqvvpp81r26cp";
+  };
+
+  buildInputs = [ocaml findlib camlp5];
+
+  createFindlibDestdir = true;
+
+  patches = [ ./meta_version.patch ./camlp5.patch ];
+
+  buildFlags = "all all.opt";
+
+  meta = {
+    homepage = http://www.cduce.org/download.html;
+    description = "ulex is a lexer generator for Unicode and OCaml";
+    license = "MIT";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/development/ocaml-modules/ulex/0.8/meta_version.patch b/pkgs/development/ocaml-modules/ulex/0.8/meta_version.patch
new file mode 100644
index 000000000000..7a39510cf0b4
--- /dev/null
+++ b/pkgs/development/ocaml-modules/ulex/0.8/meta_version.patch
@@ -0,0 +1,10 @@
+Author: Stefano Zacchiroli <zack@debian.org>
+Description: fix a typo in the findlib package version number specified in META
+--- ulex0.8.orig/META
++++ ulex0.8/META
+@@ -1,4 +1,4 @@
+-version = "0.7"
++version = "0.8"
+ requires = "camlp4"
+ description = "Runtime support for ulex"
+ archive(byte) = "ulexing.cma"
diff --git a/pkgs/development/ocaml-modules/ulex/default.nix b/pkgs/development/ocaml-modules/ulex/default.nix
new file mode 100644
index 000000000000..aee65a6e2ee8
--- /dev/null
+++ b/pkgs/development/ocaml-modules/ulex/default.nix
@@ -0,0 +1,28 @@
+{stdenv, fetchurl, ocaml, findlib }:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "1.1";
+  pname = "ulex";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://www.cduce.org/download/${pname}-${version}.tar.gz";
+    sha256 = "0fjlkwps14adfgxdrbb4yg65fhyimplvjjs1xqj5np197cig67x0";
+  };
+
+  buildInputs = [ocaml findlib];
+
+  buildFlags = "all all.opt";
+
+  meta = {
+    homepage = http://www.cduce.org/download.html;
+    description = "ulex is a lexer generator for Unicode and OCaml";
+    license = "MIT";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index a6d61f418f4d..be1617cd5b0c 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -2047,8 +2047,14 @@ let
 
     findlib = callPackage ../development/tools/ocaml/findlib { };
 
-    lablgtk = callPackage ../development/libraries/lablgtk {
-      inherit (gnome) libgnomecanvas;
+    gmetadom = callPackage ../development/ocaml-modules/gmetadom { };
+    
+    lablgtk = callPackage ../development/ocaml-modules/lablgtk {
+      inherit (gnome) libgnomecanvas libglade gtksourceview;
+    };
+
+    lablgtkmathview = callPackage ../development/ocaml-modules/lablgtkmathview { 
+      gtkmathview = callPackage ../development/libraries/gtkmathview { };
     };
 
     menhir = callPackage ../development/ocaml-modules/menhir { };
@@ -2057,8 +2063,14 @@ let
 
     ocaml_cryptgps = callPackage ../development/ocaml-modules/cryptgps { };
 
+    ocaml_expat = callPackage ../development/ocaml-modules/expat { };
+
+    ocaml_http = callPackage ../development/ocaml-modules/http { };
+
     ocaml_lwt = callPackage ../development/ocaml-modules/lwt { };
 
+    ocaml_mysql = callPackage ../development/ocaml-modules/mysql { };
+
     ocamlnet = callPackage ../development/ocaml-modules/ocamlnet { };
 
     ocaml_pcre = callPackage ../development/ocaml-modules/pcre {
@@ -2072,6 +2084,10 @@ let
     ocaml_ssl = callPackage ../development/ocaml-modules/ssl { };
 
     ounit = callPackage ../development/ocaml-modules/ounit { };
+
+    ulex08 = callPackage ../development/ocaml-modules/ulex/0.8 {
+      camlp5 = camlp5_transitional;
+    };
   };
 
   ocamlPackages = recurseIntoAttrs ocamlPackages_3_11_1;
@@ -2937,6 +2953,10 @@ let
     stdenv = overrideGCC stdenv gcc41;
   };
 
+  gdome2 = callPackage ../development/libraries/gdome2 {
+    inherit (gnome) gtkdoc;
+  };
+
   gdbm = callPackage ../development/libraries/gdbm { };
 
   gdk_pixbuf = callPackage ../development/libraries/gdk-pixbuf {
@@ -3131,6 +3151,8 @@ let
     inherit (gnome) gtk;
   };
 
+  gtkmathview = callPackage ../development/libraries/gtkmathview { };
+
   gtkLibs = gtkLibs220;
 
   glib = gtkLibs.glib;
@@ -7163,6 +7185,12 @@ let
 
   leo2 = callPackage ../applications/science/logic/leo2 {};
 
+  matita = callPackage ../applications/science/logic/matita {
+    inherit (ocamlPackages) findlib lablgtk ocaml_expat gmetadom ocaml_http 
+            lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre;
+    camlp5 = ocamlPackages.camlp5_transitional;
+  };
+
   minisat = callPackage ../applications/science/logic/minisat {};
 
   opensmt = callPackage ../applications/science/logic/opensmt { };