X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaInit.ml;h=1df34c4a1de2a066c9af182ca3b0a8339fda360c;hb=00f8f919262e3c84dd9e42477092cc1312171493;hp=53ff6b9d60f29bdb8d775ba61811f11b174e18ff;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 53ff6b9d6..1df34c4a1 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -44,16 +44,18 @@ 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 = [ + "db.nodb", "false"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.profile", "true"; + "matita.system", "false"; + "matita.verbosity", "1"; + "matita.bench", "false"; + (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is + * intuitively verbose *) +] let set_registry_values = List.iter (fun key, value -> Helm_registry.set ~key ~value) @@ -74,8 +76,6 @@ 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; ConfigurationFile::init_status end else @@ -108,6 +108,8 @@ let initialize_environment 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,13 +122,23 @@ 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 Usage: matitac [ OPTION ... ] FILE +Options:" + BuildTimeConf.version; + "gragrep", + sprintf "Grafite Grep v%s +Usage: gragrep [ -r ] PATH +Options:" + BuildTimeConf.version; + "matitaprover", + sprintf "Matita's prover v%s +Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", @@ -149,6 +161,42 @@ Options:" sprintf "MatitaClean v%s Usage: matitaclean all matitaclean [ (FILE | URI) ... ] +Options:" + BuildTimeConf.version; + "matitamake", + sprintf "MatitaMake v%s +Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) + init + Parameters: name (the name of the development, required) + root (the directory in which the delopment is rooted, + optional, default is current working directory) + Description: tells matitamake that a new development radicated + in the current working directory should be handled. + clean + Parameters: name (the name of the development to destroy, optional) + If omitted the development that holds the current working + directory is used (if any). + Description: clean the develpoment. + list + Parameters: + Description: lists the known developments and their roots. + destroy + Parameters: name (the name of the development to destroy, required) + Description: deletes a development (only from matitamake metadat, no + .ma files will be deleted). + build + Parameters: name (the name of the development to build, required) + Description: completely builds the develpoment. + publish + Parameters: name (the name of the development to publish, required) + Description: cleans the development in the user space, rebuilds it + in the system space ('ro' repositories, that for this operation + becames writable). +Notes: + If target is omitted an 'all' will be used as the default. + With -build you can build a development wherever it is. + If you specify a target it implicitly refers to the development that + holds the current working directory (if any). Options:" BuildTimeConf.version; ] @@ -162,34 +210,59 @@ let usage () = 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 + let includes = ref [ + BuildTimeConf.stdlib_dir_devel; + BuildTimeConf.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 reduce_verbosity () = + Helm_registry.set_int "matita.verbosity" + (Helm_registry.get_int "matita.verbosity" - 1) in + let increase_verbosity () = + Helm_registry.set_int "matita.verbosity" + (Helm_registry.get_int "matita.verbosity" + 1) 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"); "-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"; + "-force", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true), + ("Force actions that would not be executed per default"); + "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true), + ("Avoid using external database connection" + ^ "\n WARNING: disable many features"); + "-noprofile", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), + "Turns off profiling printings"; + "-profile-only", + Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), + "Activates only profiler with label matching the provided regex"; + "-bench", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true), + "Turns on parsable output on stdout, that is timings for matitac..."; "-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)"); + "-q", Arg.Unit reduce_verbosity, "Reduce verbosity"; "-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)"); - "-noprofile", - Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false), - "Turns off profiling printings"; + ^ "\n WARNING: not for the casual user"); + "-v", Arg.Unit increase_verbosity, "Increase verbosity"; ] in let debug_arg_spec = if BuildTimeConf.debug then @@ -200,16 +273,23 @@ let parse_cmdline init_status = ] 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:(List.rev l) in Arg.parse arg_spec (add_l args) (usage ()); + let includes = List.map absolutize !includes in set_list ~key:"matita.includes" includes; + let args = 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 @@ -221,9 +301,8 @@ let die_usage () = 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 ] + [ fill_registry; parse_cmdline; load_configuration; initialize_makelib; + initialize_db; initialize_environment ] (* initialize_notation (initialize_environment (initialize_db @@ -239,4 +318,6 @@ let parse_cmdline () = let fill_registry () = status := fill_registry !status +;; +Inversion_principle.init ()