X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=70125f54c222bb5dc3c3d146a8a7cc8aecfee294;hb=2c31f199f35d96d7b0dd86f738c8d4887b37446d;hp=53ff6b9d60f29bdb8d775ba61811f11b174e18ff;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 53ff6b9d6..70125f54c 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -25,12 +25,10 @@ (* $Id$ *) -open Printf - -type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry +type thingsToInitialize = + ConfigurationFile | Db | Environment | Getter | CmdLine | Registry -exception FailedToInitialize of thingsToInitilaize +exception FailedToInitialize of thingsToInitialize let wants s l = List.iter ( @@ -44,19 +42,25 @@ let already_configured s l = let conffile = ref BuildTimeConf.matita_conf -let registry_defaults = - [ - "db.nodb", "false"; - "matita.system", "false"; - "matita.debug", "false"; - "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; - "matita.quiet", "false"; - "matita.profile", "true"; - ] +let registry_defaults = [ + "matita.debug", "false"; + "matita.debug_menu", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.profile", "true"; + "matita.system", "false"; + "matita.verbose", "false"; + "matita.paste_unicode_as_tex", "false"; + "matita.noinnertypes", "false"; + "matita.do_heavy_checks", "true"; + "matita.moo", "true"; + "matita.extract", "false"; + "matita.execcomments", "false"; +] let set_registry_values = - List.iter (fun key, value -> Helm_registry.set ~key ~value) + List.iter + (fun key, value -> + if not (Helm_registry.has key) then Helm_registry.set ~key ~value) let fill_registry init_status = if not (already_configured [ Registry ] init_status) then begin @@ -66,7 +70,6 @@ let fill_registry init_status = init_status let load_configuration init_status = - wants [ Registry ] init_status; if not (already_configured [ConfigurationFile] init_status) then begin Helm_registry.load_from !conffile; @@ -74,8 +77,17 @@ let load_configuration init_status = let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in Helm_registry.set "user.name" login end; - if Helm_registry.get_bool "matita.system" then - Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir; + let home = Helm_registry.get_string "matita.basedir" in + let user_conf_file = home ^ "/matita.conf.xml" in + if HExtlib.is_regular user_conf_file then + begin + HLog.message ("Loading additional conf file from " ^ user_conf_file); + try + Helm_registry.load_from user_conf_file + with exn -> + HLog.error + ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn)) + end; ConfigurationFile::init_status end else @@ -93,21 +105,13 @@ let initialize_db init_status = else init_status -let initialize_makelib init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Makelib] init_status) then - begin - MatitamakeLib.initialize (); - Makelib::init_status - end - else - init_status - let initialize_environment init_status = - wants [ConfigurationFile] init_status; + wants [CmdLine] init_status; if not (already_configured [Getter;Environment] init_status) then begin Http_getter.init (); + if Helm_registry.get_bool "matita.system" then + Http_getter_storage.activate_system_mode (); CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_opt_default Helm_registry.get_bool @@ -120,40 +124,40 @@ let initialize_environment init_status = let status = ref [] -let usages = Hashtbl.create 11 +let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *) let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) [ "matitac", - sprintf "MatitaC v%s + Printf.sprintf "Matita batch compiler v%s Usage: matitac [ OPTION ... ] FILE Options:" BuildTimeConf.version; - "matita", - sprintf "Matita v%s -Usage: matita [ OPTION ... ] [ FILE ... ] + "matitaprover", + Printf.sprintf "Matita (TPTP) prover v%s +Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; - "cicbrowser", - sprintf - "CIC Browser v%s -Usage: cicbrowser [ URL | WHELP QUERY ] + "matita", + Printf.sprintf "Matita interactive theorem prover v%s +Usage: matita [ OPTION ... ] [ FILE ] Options:" BuildTimeConf.version; "matitadep", - sprintf "MatitaDep v%s -Usage: matitadep [ OPTION ... ] FILE ... + Printf.sprintf "Matita depency file generator v%s +Usage: matitadep [ OPTION ... ] Options:" BuildTimeConf.version; "matitaclean", - sprintf "MatitaClean v%s + Printf.sprintf "MatitaClean v%s Usage: matitaclean all - matitaclean [ (FILE | URI) ... ] + matitaclean ( FILE | URI ) Options:" BuildTimeConf.version; ] let default_usage = - sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version + Printf.sprintf + "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version let usage () = let basename = Filename.basename Sys.argv.(0) in @@ -161,35 +165,72 @@ let usage () = try Filename.chop_extension basename with Invalid_argument _ -> basename in try Hashtbl.find usages usage_key with Not_found -> default_usage +;; + +let extra_cmdline_specs = ref [] +let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs let parse_cmdline init_status = if not (already_configured [CmdLine] init_status) then begin - let includes = ref [ BuildTimeConf.stdlib_dir ] in + wants [Registry] init_status; + let includes = ref [] in + let default_includes = [ + BuildTimeConf.stdlib_dir_devel; + BuildTimeConf.stdlib_dir_installed ; + BuildTimeConf.new_stdlib_dir_devel; + BuildTimeConf.new_stdlib_dir_installed ; + ] + in + let absolutize s = + if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s + in let args = ref [] in let add_l l = fun s -> l := s :: !l in + let print_version () = + Printf.printf "%s\n" BuildTimeConf.version;exit 0 in + let no_innertypes () = + Helm_registry.set_bool "matita.noinnertypes" true in + let set_baseuri s = + match Str.split (Str.regexp "::") s with + | [path; uri] -> Helm_registry.set "matita.baseuri" + (HExtlib.normalize_path (absolutize path)^" "^uri) + | _ -> raise (Failure "bad baseuri, use -b 'path::uri'") + in + let no_default_includes = ref false in + let execcomments = ref false in let arg_spec = let std_arg_spec = [ + "-b", Arg.String set_baseuri, " forces the baseuri of path"; "-I", Arg.String (add_l includes), (" Adds path to the list of searched paths for the " ^ "include command"); "-conffile", Arg.Set_string conffile, - (Printf.sprintf " Read configuration from filename (default: %s)" + (Printf.sprintf (" Read configuration from filename" + ^^ "\n Default: %s") BuildTimeConf.matita_conf); - "-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)"); - "-system", Arg.Unit (fun () -> - Helm_registry.set_bool "matita.system" true), - ("Act on the system library instead of the user one" - ^ "(WARNING: not for the casual user)"); + "-force", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true), + ("Force actions that would not be executed per default"); "-noprofile", Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), "Turns off profiling printings"; + "-noinnertypes", Arg.Unit no_innertypes, + "Turns off inner types generation while publishing"; + "-profile-only", + Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), + "Activates only profiler with label matching the provided regex"; + "-system", Arg.Unit (fun () -> + Helm_registry.set_bool "matita.system" true), + ("Act on the system library instead of the user one" + ^ "\n WARNING: not for the casual user"); + "-no-default-includes", Arg.Set no_default_includes, + "Do not include the default searched paths for the include command"; + "-execcomments", Arg.Set execcomments, + "Execute the content of (** ... *) comments"; + "-v", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), + "Verbose mode"; + "--version", Arg.Unit print_version, "Prints version" ] in let debug_arg_spec = if BuildTimeConf.debug then @@ -197,19 +238,34 @@ let parse_cmdline init_status = Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true), ("Do not catch top-level exception " ^ "(useful for backtrace inspection)"); + "-onepass", + Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true), + "Enable only one disambiguation pass"; ] else [] in - std_arg_spec @ debug_arg_spec + std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs in let set_list ~key l = - Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l) + Helm_registry.set_list Helm_registry.of_string ~key ~value:l in Arg.parse arg_spec (add_l args) (usage ()); + Helm_registry.set_bool ~key:"matita.execcomments" ~value:!execcomments; + let default_includes = if !no_default_includes then [] else default_includes in + let includes = + List.map (fun x -> HExtlib.normalize_path (absolutize x)) + ((List.rev !includes) @ default_includes) + in set_list ~key:"matita.includes" includes; + let args = List.rev (List.filter (fun x -> x <> "") !args) in set_list ~key:"matita.args" args; HExtlib.set_profiling_printings - (fun () -> Helm_registry.get_bool "matita.profile"); + (fun s -> + Helm_registry.get_bool "matita.profile" && + Pcre.pmatch + ~pat:(Helm_registry.get_opt_default + Helm_registry.string ~default:".*" "matita.profile_only") + s); CmdLine :: init_status end else init_status @@ -218,25 +274,27 @@ let die_usage () = print_endline (usage ()); exit 1 +let conf_components = + [ load_configuration; fill_registry; parse_cmdline] + +let other_components = + [ initialize_db; initialize_environment ] + let initialize_all () = status := List.fold_left (fun s f -> f s) !status - [ fill_registry; - parse_cmdline; load_configuration; initialize_makelib; - initialize_db; initialize_environment ] -(* initialize_notation - (initialize_environment - (initialize_db - (initialize_makelib - (load_configuration - (parse_cmdline !status))))) *) - -let load_configuration_file () = - status := load_configuration !status + (conf_components @ other_components); + NCicLibrary.init () -let parse_cmdline () = - status := parse_cmdline !status +let parse_cmdline_and_configuration_file () = + status := List.fold_left (fun s f -> f s) !status conf_components -let fill_registry () = - status := fill_registry !status +let initialize_environment () = + status := initialize_environment !status +let _ = + CicFix.init (); + Inversion_principle.init (); + CicRecord.init (); + CicElim.init () +;;