Reparing stable build of Matita.
Also correcting the version and simplifying the prerelease package of Matita. svn path=/nixpkgs/trunk/; revision=33420
This commit is contained in:
parent
4bccef4db2
commit
ec5dda12d2
@ -2,7 +2,7 @@
|
|||||||
|
|
||||||
let
|
let
|
||||||
ocaml_version = (builtins.parseDrvName ocaml.name).version;
|
ocaml_version = (builtins.parseDrvName ocaml.name).version;
|
||||||
version = "0.9.1pre130312";
|
version = "0.99.1pre130312";
|
||||||
pname = "matita";
|
pname = "matita";
|
||||||
|
|
||||||
in
|
in
|
||||||
@ -43,7 +43,7 @@ stdenv.mkDerivation {
|
|||||||
substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
|
substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
|
||||||
'';
|
'';
|
||||||
|
|
||||||
patches = [ ./configure_130312.patch ./130312.patch ];
|
patches = [ ./configure_130312.patch ];
|
||||||
|
|
||||||
preConfigure = ''
|
preConfigure = ''
|
||||||
# Setup for findlib.
|
# Setup for findlib.
|
||||||
|
@ -1,42 +0,0 @@
|
|||||||
--- 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
|
|
@ -2465,7 +2465,7 @@ let
|
|||||||
ulex = callPackage ../development/ocaml-modules/ulex { };
|
ulex = callPackage ../development/ocaml-modules/ulex { };
|
||||||
|
|
||||||
ulex08 = callPackage ../development/ocaml-modules/ulex/0.8 {
|
ulex08 = callPackage ../development/ocaml-modules/ulex/0.8 {
|
||||||
camlp5 = camlp5_5_transitional;
|
camlp5 = camlp5_transitional;
|
||||||
};
|
};
|
||||||
|
|
||||||
ocaml_typeconv = callPackage ../development/ocaml-modules/typeconv { };
|
ocaml_typeconv = callPackage ../development/ocaml-modules/typeconv { };
|
||||||
@ -8196,8 +8196,10 @@ let
|
|||||||
leo2 = callPackage ../applications/science/logic/leo2 {};
|
leo2 = callPackage ../applications/science/logic/leo2 {};
|
||||||
|
|
||||||
matita = callPackage ../applications/science/logic/matita {
|
matita = callPackage ../applications/science/logic/matita {
|
||||||
inherit (ocamlPackages) findlib lablgtk ocaml_expat gmetadom ocaml_http
|
ocaml = ocaml_3_11_2;
|
||||||
lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre;
|
inherit (ocamlPackages_3_11_2) findlib lablgtk ocaml_expat gmetadom ocaml_http
|
||||||
|
lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet camlzip ocaml_pcre;
|
||||||
|
ulex08 = ocamlPackages_3_11_2.ulex08.override { camlp5 = ocamlPackages_3_11_2.camlp5_5_transitional; };
|
||||||
};
|
};
|
||||||
|
|
||||||
matita_130312 = lowPrio (callPackage ../applications/science/logic/matita/130312.nix {
|
matita_130312 = lowPrio (callPackage ../applications/science/logic/matita/130312.nix {
|
||||||
|
Loading…
x
Reference in New Issue
Block a user