From: Stefano Zacchiroli Date: Wed, 5 Oct 2005 09:12:23 +0000 (+0000) Subject: - added support for "-nodb" flag (still missing support for matitaclean which relies... X-Git-Tag: V_0_7_2_3~248 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afe21e48aefe81db3ca150fac9a5bbfbc893fa59;p=helm.git - added support for "-nodb" flag (still missing support for matitaclean which relies on the db) - centralized parsing of cmdline options in matitaInit. All top level programs which need to parse cmdline will now invoke either MatitaInit.parse_cmdline or MatitaInit.initialize_all and then refer to the relevant keys in the registry - changed dependencies on hMySql since now it is in a separate library --- diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index f5c9a341f..b4cb75bd4 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -22,6 +22,14 @@ OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) + +MATITA_FLAGS = +NODB=false +ifeq ($(NODB),true) + MATITA_FLAGS += -nodb +endif + + # objects for matita (GTK GUI) NULL = CMOS = \ @@ -91,9 +99,9 @@ matita.conf.xml.sample: matita.conf.xml.sample.in @echo coq.moo: coq.ma matitac - ./matitac coq.ma + ./matitac $(MATITA_FLAGS) coq.ma coq.moo.opt: coq.ma matitac.opt - ./matitac.opt coq.ma + ./matitac.opt $(MATITA_FLAGS) coq.ma ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 91ae69482..bad92774b 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -30,6 +30,8 @@ FINDLIB_DEPREQUIRES="\ pcre \ mysql \ helm-registry \ +helm-extlib \ +helm-hmysql \ helm-cic_disambiguation \ helm-paramodulation \ " diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index c3fdb2459..1d62cadb5 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -122,6 +122,8 @@ let _ = addDebugItem "getter: getalluris" (fun _ -> List.iter prerr_endline (Http_getter.getalluris ())); addDebugItem "dump script status" script#dump; + addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ -> + Helm_registry.save_to "./foo.conf.xml"); addDebugItem "dump metasenv" (fun _ -> if script#onGoingProof () then @@ -148,27 +150,6 @@ let _ = (** {2 Command line parsing} *) -let debug = ref false -let args = ref [] -let add_arg arg = args := arg :: !args - -let arg_spec = - let std_arg_spec = [] in - let debug_arg_spec = - if BuildTimeConf.debug then - [ "-debug", Arg.Set debug, - "Do not catch top-level exception (useful for backtrace inspection)"; ] - else [] - in - std_arg_spec @ debug_arg_spec - -let usage () = - let heading = sprintf "Matita v%s\nUsage: " BuildTimeConf.version in - if Helm_registry.get "matita.mode" = "cicbrowser" then - heading ^ "cicbrowser [ URL | Whelp query ]\nOptions:" - else - heading ^ "matita [ FILE ]" - let set_matita_mode () = let matita_mode = if Filename.basename Sys.argv.(0) = "cicbrowser" @@ -181,16 +162,15 @@ let set_matita_mode () = let _ = set_matita_mode (); - Arg.parse arg_spec add_arg (usage ()); - Helm_registry.set_bool "matita.catch_top_level_exn" (not !debug); at_exit (fun () -> print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; + let args = Helm_registry.get_list Helm_registry.string "matita.args" in if Helm_registry.get "matita.mode" = "cicbrowser" then (* cicbrowser *) let browser = MatitaMathView.cicBrowser () in - let uri = match !args with [] -> "cic:/" | _ -> String.concat " " !args in + let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in browser#loadInput uri else begin (* matita *) - (try gui#loadScript (List.hd !args) with Failure _ -> ()); + (try gui#loadScript (List.hd args) with Failure _ -> ()); gui#main#mainWin#show (); end; try diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8351426f8..5c5b24c4d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -568,7 +568,7 @@ class gui () = MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := (fun exn -> - if Helm_registry.get_bool "matita.catch_top_level_exn" then + if not (Helm_registry.get_bool "matita.debug") then MatitaLog.error (MatitaExcPp.to_string exn) else raise exn); (* script *) diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index aab815601..f7003796b 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -23,9 +23,11 @@ * http://helm.cs.unibo.it/ *) +open Printf + type thingsToInitilaize = ConfigurationFile | Db | Environment | Getter | Notation | - Paramodulation | Makelib + Paramodulation | Makelib | CmdLine exception FailedToInitialize of thingsToInitilaize @@ -49,8 +51,8 @@ let load_configuration init_status = init_status let initialize_db init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Db] init_status) then + wants [ ConfigurationFile; CmdLine ] init_status; + if not (already_configured [ Db ] init_status) then begin MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment (); @@ -103,7 +105,105 @@ let initialize_environment init_status = init_status let status = ref [] - + +let usages = Hashtbl.create 11 +let _ = + List.iter + (fun (name, s) -> Hashtbl.replace usages name s) + [ "matitac", + sprintf "MatitaC v%s +Usage: matitac [ OPTION ... ] FILE +Options:" + BuildTimeConf.version; + "matita", + sprintf "Matita v%s +Usage: matita [ OPTION ... ] [ FILE ... ] +Options:" + BuildTimeConf.version; + "cicbrowser", + sprintf + "CIC Browser v%s +Usage: cicbrowser [ URL | WHELP QUERY ] +Options:" + BuildTimeConf.version; + "matitadep", + sprintf "MatitaDep v%s +Usage: matitadep [ OPTION ... ] FILE ... +Options:" + BuildTimeConf.version; + "matitaclean", + sprintf "MatitaClean v%s +Usage: matitaclean all + matitaclean [ (FILE | URI) ... ] +Options:" + BuildTimeConf.version; + ] +let default_usage = + sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version + +let usage () = + let basename = Filename.basename Sys.argv.(0) in + let usage_key = + try Filename.chop_extension basename with Invalid_argument _ -> basename + in + try Hashtbl.find usages usage_key with Not_found -> default_usage + +let registry_defaults = + [ "matita.debug", "false"; + "matita.quiet", "false"; + "matita.preserve", "false"; + "db.nodb", "false"; + ] + +let set_registry_values = + List.iter (fun key, value -> Helm_registry.set ~key ~value) + +let parse_cmdline init_status = + if not (already_configured [CmdLine] init_status) then begin + let includes = ref [] in + let args = ref [] in + let add_l l = fun s -> l := s :: !l in + let arg_spec = + let std_arg_spec = [ + "-I", Arg.String (add_l includes), + (" Adds path to the list of searched paths for the " + ^ "include command"); + "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true), + "Turn off verbose compilation"; + "-preserve", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), + "Turns off automatic baseuri cleaning"; + "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true), + ("Avoid using external database connection " + ^ "(WARNING: disable many features)"); + ] in + let debug_arg_spec = + if BuildTimeConf.debug then + [ "-debug", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true), + ("Do not catch top-level exception " + ^ "(useful for backtrace inspection)"); + ] + else [] + in + std_arg_spec @ debug_arg_spec + in + let set_list ~key l = + Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l) + in + set_registry_values registry_defaults; + Arg.parse arg_spec (add_l args) (usage ()); + set_list ~key:"matita.includes" includes; + set_list ~key:"matita.args" args; +Helm_registry.save_to "./foo.conf.xml"; + CmdLine :: init_status + end else + init_status + +let die_usage () = + print_endline (usage ()); + exit 1 + let initialize_all () = status := initialize_notation @@ -111,11 +211,15 @@ let initialize_all () = (initialize_db (initialize_paramodulation (initialize_makelib - (load_configuration !status))))) + (load_configuration + (parse_cmdline !status)))))) -let load_config_only () = +let load_configuration_file () = status := load_configuration !status let initialize_notation () = status := initialize_notation (load_configuration !status) - + +let parse_cmdline () = + status := parse_cmdline !status + diff --git a/helm/matita/matitaInit.mli b/helm/matita/matitaInit.mli index be6abfc7a..e8050f9be 100644 --- a/helm/matita/matitaInit.mli +++ b/helm/matita/matitaInit.mli @@ -23,7 +23,16 @@ * http://helm.cs.unibo.it/ *) -val load_config_only: unit -> unit + (** {2 global initialization} *) val initialize_all: unit -> unit + + (** {2 per-components initialization} *) +val parse_cmdline: unit -> unit (** parse cmdline setting registry keys *) +val load_configuration_file: unit -> unit val initialize_notation: unit -> unit + (** {2 Utilities} *) + + (** die nicely: exit with return code 1 printing usage error message *) +val die_usage: unit -> 'a + diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index be144b949..7d2a47a94 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -591,7 +591,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) try f () with exn -> - if Helm_registry.get_bool "matita.catch_top_level_exn" then + if not (Helm_registry.get_bool "matita.debug") then fail (MatitaExcPp.to_string exn) else raise exn in diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index fa7e487a9..0db34ea88 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -29,36 +29,6 @@ open MatitaTypes (** {2 Initialization} *) - (** If set to true matitac wont catch top level exception, so that backtrace - * could be inspected setting OCAMLRUNPARAM=b. This flag is enabled passing - * -debug *) -let debug = ref false -let paths_to_search_in = ref [];; -let quiet_compilation = ref false;; -let dont_delete_baseuri = ref false;; - -let add_l l = fun s -> l := s :: !l ;; - -let arg_spec = - let std_arg_spec = [ - "-I", Arg.String (add_l paths_to_search_in), - " Adds path to the list of searched paths for the include command"; - "-q", Arg.Set quiet_compilation, "Turn off verbose compilation"; - "-preserve", Arg.Set dont_delete_baseuri, - "Turns off automatic baseuri cleaning"; - ] in - let debug_arg_spec = - if BuildTimeConf.debug then - [ "-debug", Arg.Set debug, - "Do not catch top-level exception (useful for backtrace inspection)"; ] - else [] - in - std_arg_spec @ debug_arg_spec - -let usage = - sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" - BuildTimeConf.version - let status = ref None let run_script is eval_function = @@ -69,10 +39,10 @@ let run_script is eval_function = in let slash_n_RE = Pcre.regexp "\\n" in let cb = - if !quiet_compilation then - fun _ _ -> () + if Helm_registry.get_bool "matita.quiet" then + (fun _ _ -> ()) else - fun status stm -> + (fun status stm -> (* dump_status status; *) let stm = GrafiteAstPp.pp_statement stm in let stm = Pcre.replace ~rex:slash_n_RE stm in @@ -82,7 +52,7 @@ let run_script is eval_function = else stm in - MatitaLog.debug ("Executing: ``" ^ stm ^ "''") + MatitaLog.debug ("Executing: ``" ^ stm ^ "''")) in try eval_function status is cb @@ -95,12 +65,9 @@ let run_script is eval_function = raise exn let fname () = - let acc = ref [] in - let add_script fname = acc := fname :: !acc in - Arg.parse arg_spec add_script usage; - match !acc with + match Helm_registry.get_list Helm_registry.string "matita.args" with | [x] -> x - | _ -> print_endline usage; exit 1 + | _ -> MatitaInit.die_usage () let pp_ocaml_mode () = MatitaLog.message ""; @@ -130,7 +97,9 @@ let rec interactive_loop () = let str = Ulexing.from_utf8_channel stdin in try run_script str - (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in) + (MatitaEngine.eval_from_stream_greedy + ~include_paths:(Helm_registry.get_list Helm_registry.string + "matita.includes")) with | MatitaEngine.Drop -> pp_ocaml_mode () | Sys.Break -> MatitaLog.error "user break!"; interactive_loop () @@ -159,6 +128,8 @@ let go () = let main ~mode = MatitaInit.initialize_all (); + (* must be called after init since args are set by cmdline parsing *) + let fname = fname () in status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; let origcb = MatitaLog.get_log_callback () in @@ -167,12 +138,11 @@ let main ~mode = | `Debug | `Message -> () | `Warning | `Error -> origcb tag s in - let fname = fname () in - if !quiet_compilation then + if Helm_registry.get_bool "matita.quiet" then MatitaLog.set_log_callback newcb; try let time = Unix.time () in - if !quiet_compilation then + if Helm_registry.get_bool "matita.quiet" then origcb `Message ("compiling " ^ Filename.basename fname ^ "...") else MatitaLog.message (sprintf "execution of %s started:" fname); @@ -184,8 +154,9 @@ let main ~mode = in run_script is (MatitaEngine.eval_from_stream - ~include_paths:!paths_to_search_in - ~clean_baseuri:(not !dont_delete_baseuri)); + ~include_paths:(Helm_registry.get_list Helm_registry.string + "matita.includes") + ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve"))); let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = @@ -236,7 +207,7 @@ let main ~mode = else pp_ocaml_mode () | exn -> - if !debug then raise exn; + if Helm_registry.get_bool "matita.debug" then raise exn; if mode = `COMPILER then clean_exit (Some 3) else diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index f49c47de3..e15f736dc 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -23,27 +23,20 @@ * http://helm.cs.unibo.it/ *) -module UM = UriManager;; -module TA = GrafiteAst;; +open Printf + +module UM = UriManager +module TA = GrafiteAst let _ = MatitaInit.initialize_all () let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove -let usage () = - prerr_endline " -usage: -\tmatitaclean all -\t\tcleans the whole environment -\tmatitaclean files... -\t\tcleans the output of the compilation of files... -"; - exit 1 - let _ = - if Array.length Sys.argv < 2 then usage (); - if Sys.argv.(1) = "all" then - begin + let uris_to_remove = ref [] in + let files_to_remove = ref [] in + (match Helm_registry.get_list Helm_registry.string "matita.args" with + | [ "all" ] -> MatitaDb.clean_owner_environment (); let xmldir = Helm_registry.get "matita.basedir" ^ "/xml" in ignore @@ -55,31 +48,25 @@ let _ = (Sys.command ("find " ^ xmldir ^ " -type d -exec rmdir -p {} \\; 2> /dev/null")); exit 0 - end - let uris_to_remove =ref [] in - let files_to_remove =ref [] in - (try - for i = 1 to Array.length Sys.argv - 1 do - let suri = Sys.argv.(i) in - let uri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with - UM.IllFormedUri _ -> - files_to_remove := suri :: !files_to_remove; - let u = MatitaMisc.baseuri_of_file suri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - begin - MatitaLog.error ("File " ^ suri ^ " defines a bad baseuri: "^u); - exit 1 - end - else - u - in - uris_to_remove := uri :: !uris_to_remove - done - with - Invalid_argument _ -> usage ()); + | [] -> MatitaInit.die_usage () + | files -> + List.iter + (fun suri -> + let uri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with UM.IllFormedUri _ -> + files_to_remove := suri :: !files_to_remove; + let u = MatitaMisc.baseuri_of_file suri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin + MatitaLog.error (sprintf "File %s defines a bad baseuri: %s" + suri u); + exit 1 + end else + u + in + uris_to_remove := uri :: !uris_to_remove) + files); main !uris_to_remove; let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in List.iter MatitaMisc.safe_remove moos diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 77a7d7b6f..2d1cbfdef 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + let debug = false let debug_prerr = if debug then prerr_endline else ignore @@ -49,8 +51,9 @@ let one_step_depend suri = let buri = buri ^ "/" in let buri = HMysql.escape buri in let obj_tbl = MetadataTypes.obj_tbl () in - Printf.sprintf - "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri + sprintf + "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" + obj_tbl buri in try let rc = HMysql.exec (MatitaDb.instance ()) query in @@ -66,7 +69,6 @@ let one_step_depend suri = with exn -> raise exn (* no errors should be accepted *) end - let safe_buri_of_suri suri = try @@ -156,3 +158,4 @@ let clean_baseuris ?(verbose=true) buris = MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); MetadataTypes.count_tbl()] end + diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 40f91235a..3eb83af00 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -23,18 +23,6 @@ * http://helm.cs.unibo.it/ *) -let paths_to_search_in = ref [];; - -let add_l l = fun s -> l := s :: !l ;; - -let arg_spec = [ - "-I", Arg.String (add_l paths_to_search_in), - " Adds path to the list of searched paths for the include command"; -] -let usage = - Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:" - BuildTimeConf.version - module GA = GrafiteAst module U = UriManager @@ -58,7 +46,7 @@ let find path = close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path with Sys_error _ -> aux tl in - let paths = !paths_to_search_in in + let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in try aux paths with Sys_error _ as exc -> @@ -68,9 +56,8 @@ let find path = ;; let main () = - MatitaInit.load_config_only (); - let files = ref [] in - Arg.parse arg_spec (add_l files) usage; + MatitaInit.load_configuration_file (); + MatitaInit.parse_cmdline (); List.iter (fun file -> let ic = open_in file in @@ -94,7 +81,7 @@ let main () = MatitaLog.warn ("Unable to find " ^ path ^ " that is included in " ^ file)) dependencies) - !files; + (Helm_registry.get_list Helm_registry.string "matita.args"); Hashtbl.iter (fun file alias -> let dep = resolve alias (Hashtbl.find baseuri_of file) in @@ -112,7 +99,7 @@ let main () = let moo = MatitaMisc.obj_file_of_script file in Printf.printf "%s: %s\n" moo (String.concat " " deps); Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) - !files + (Helm_registry.get_list Helm_registry.string "matita.args") ;; let _ = diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml index 5a3ecf5ee..8bd5900f5 100644 --- a/helm/matita/matitamake.ml +++ b/helm/matita/matitamake.ml @@ -26,7 +26,7 @@ module MK = MatitamakeLib ;; let _ = - MatitaInit.load_config_only (); + MatitaInit.load_configuration_file (); MK.initialize () ;;