X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitaprover.ml;h=7a6503ab36e7f15c2730770ce5c55d3aa7a3d504;hb=27d1c17647fd6d8ec4749160f921c404da0028e3;hp=b3115ec26e6feefff346bfba3ebb9f36b8053035;hpb=d0e212dcd4bdbeaee9979e53bedd3258cd8e8d0f;p=helm.git

diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml
index b3115ec26..7a6503ab3 100644
--- a/matita/matitaprover.ml
+++ b/matita/matitaprover.ml
@@ -41,6 +41,15 @@ theorem trans_eq :
 intros.elim H1.assumption.
 qed.
 
+default \"equality\"
+ " ^ buri ^ "/eq.ind
+ " ^ buri ^ "/sym_eq.con
+ " ^ buri ^ "/trans_eq.con
+ " ^ buri ^ "/eq_ind.con
+ " ^ buri ^ "/eq_elim_r.con
+ " ^ buri ^ "/eq_f.con
+ " ^ buri ^ "/eq_f1.con.
+
 theorem eq_f: \\forall  A,B:Type.\\forall f:A\\to B.
   \\forall x,y:A. eq A x y \\to eq B (f x) (f y).
 intros.elim H.reflexivity.
@@ -51,15 +60,6 @@ theorem eq_f1: \\forall  A,B:Type.\\forall f:A\\to B.
 intros.elim H.reflexivity.
 qed.
 
-default \"equality\"
- " ^ buri ^ "/eq.ind
- " ^ buri ^ "/sym_eq.con
- " ^ buri ^ "/trans_eq.con
- " ^ buri ^ "/eq_ind.con
- " ^ buri ^ "/eq_elim_r.con
- " ^ buri ^ "/eq_f.con
- " ^ buri ^ "/eq_f1.con.
-
 inductive ex (A:Type) (P:A \\to Prop) : Prop \\def
     ex_intro: \\forall x:A. P x \\to ex A P.
 interpretation \"exists\" 'exists \\eta.x =
@@ -74,23 +74,23 @@ for @{ 'exists ${default
 "
 ;;
 
-let p_to_ma ~tptppath ~filename = 
+let p_to_ma ?timeout ~tptppath ~filename () = 
   let data = 
-     Tptp2grafite.tptp2grafite ~filename ~tptppath:tptppath
+     Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath
      ~raw_preamble ()
   in
   data
 ;;
 
 let main () =
-  MatitaInit.fill_registry ();
   let tptppath = ref "./" in
+  let timeout = ref 600 in
   MatitaInit.add_cmdline_spec
     ["-tptppath",Arg.String (fun s -> tptppath:= s),
-      "Where to find the Axioms/ and Problems/ directory"];
-  MatitaInit.parse_cmdline ();
-  MatitaInit.load_configuration_file ();
-  Helm_registry.set_bool "db.nodb" true;
+       "Where to find the Axioms/ and Problems/ directory";
+     "-timeout", Arg.Int (fun x -> timeout := x),
+       "Timeout in seconds"];
+  MatitaInit.parse_cmdline_and_configuration_file ();
   Helm_registry.set_bool "matita.nodisk" true;
   HLog.set_log_callback (fun _ _ -> ()); 
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
@@ -99,7 +99,9 @@ let main () =
     | [file] -> file
     | _ -> prerr_endline "You must specify exactly one .p file."; exit 1
   in
-  let data = p_to_ma ~filename:inputfile ~tptppath:!tptppath in
+  let data = 
+    p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath ()
+  in
 (*   prerr_endline data; *)
   let is = Ulexing.from_utf8_string data in
   let gs = GrafiteSync.init () in