Adding a package for a preview release of Matita.

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

3 files changed, 113 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/matita/130312.nix b/pkgs/applications/science/logic/matita/130312.nix
new file mode 100644
index 00000000000..3501072fbfe
--- /dev/null
+++ b/pkgs/applications/science/logic/matita/130312.nix
@@ -0,0 +1,66 @@
+{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, ocaml_mysql, ocamlnet, ulex08, camlzip, ocaml_pcre, automake, autoconf }:
+
+let
+  ocaml_version = (builtins.parseDrvName ocaml.name).version;
+  version = "0.9.1pre130312";
+  pname = "matita";
+
+in
+
+stdenv.mkDerivation {
+  name = "${pname}-${version}";
+
+  src = fetchurl {
+    url = "http://matita.cs.unibo.it/sources/${pname}_130312.tar.gz"; 
+    sha256 = "13mjvvldv53dcdid6wmc6g8yn98xca26xq2rgq2jg700lqsni59s";
+  };
+
+  sourceRoot="${pname}-${version}";
+
+  unpackPhase = ''
+   mkdir $sourceRoot
+   tar -xvzf $src -C $sourceRoot
+   echo "source root is $sourceRoot"
+  '';
+
+  prePatch = ''
+   autoreconf -fvi 
+  '';
+
+  buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk ocaml_mysql ocamlnet ulex08 camlzip ocaml_pcre automake autoconf];
+
+  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_130312.patch ./130312.patch ];
+
+  preConfigure = ''
+    # Setup for findlib.
+    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
+    RTDIR=$out/share/matita
+    export configureFlags="--with-runtime-dir=$RTDIR"
+  '';
+
+  postInstall = ''
+    mkdir -p $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/applications/science/logic/matita/130312.patch b/pkgs/applications/science/logic/matita/130312.patch
new file mode 100644
index 00000000000..4596f7fde2e
--- /dev/null
+++ b/pkgs/applications/science/logic/matita/130312.patch
@@ -0,0 +1,42 @@
+--- matita/components/content_pres/cicNotationParser.ml 2012-03-25 15:47:03.144583445 -0400
++++ matita/components/content_pres/cicNotationParser.ml 2012-03-25 15:48:30.776209560 -0400
+@@ -209,8 +209,8 @@
+           match magic with
+           | Ast.List0 (_, None) -> Gramext.Slist0 s
+           | Ast.List1 (_, None) -> Gramext.Slist1 s
+-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
++          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
++          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+           | _ -> assert false
+         in
+         [ Env (List.map Env.list_declaration p_names),
+--- matita/components/grafite_parser/print_grammar.ml   2012-03-25 15:47:03.123583779 -0400
++++ matita/components/grafite_parser/print_grammar.ml   2012-03-25 15:49:43.900079528 -0400
+@@ -87,7 +87,7 @@
+   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
+   | Snterm e | Snterml (e, _) -> is_entry_dummy e
+   | Slist1 x | Slist0 x -> is_symbol_dummy x
+-  | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
++  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+   | Sopt x -> is_symbol_dummy x
+   | Sself | Snext -> false
+   | Stree t -> is_tree_dummy t
+@@ -186,7 +186,7 @@
+         let todo = visit_symbol symbol todo is_son in
+         Format.fprintf fmt "@]} @ ";
+         todo
+-    | Slist0sep (symbol,sep,false) ->
++    | Slist0sep (symbol,sep) ->
+         Format.fprintf fmt "[@[<hov2> ";
+         let todo = visit_symbol symbol todo is_son in
+         Format.fprintf fmt "{@[<hov2> ";
+@@ -200,7 +200,7 @@
+         let todo = visit_symbol symbol todo is_son in
+         Format.fprintf fmt "@]}+ @ ";
+         todo 
+-    | Slist1sep (symbol,sep,false) ->
++    | Slist1sep (symbol,sep) ->
+         let todo = visit_symbol symbol todo is_son  in
+         Format.fprintf fmt "{@[<hov2> ";
+         let todo = visit_symbol sep todo is_son in
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index b983c76c88c..f32d1023d58 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -8200,6 +8200,11 @@ let
             lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre;
   };
 
+  matita_130312 = lowPrio (callPackage ../applications/science/logic/matita/130312.nix {
+    inherit (ocamlPackages) findlib lablgtk ocaml_expat gmetadom ocaml_http
+            ocaml_mysql ocamlnet ulex08 camlzip ocaml_pcre;
+  });
+
   minisat = callPackage ../applications/science/logic/minisat {};
 
   opensmt = callPackage ../applications/science/logic/opensmt { };