X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=b34f1dfc5b67ced099ea20aa9aec97599c964b6b;hb=aef659e5893b4bf8c8544d0c54714e10f5b5493a;hp=53ff6b9d60f29bdb8d775ba61811f11b174e18ff;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 53ff6b9d6..b34f1dfc5 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/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,18 @@ 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; "matita", @@ -149,6 +156,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 +205,53 @@ 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_installed ; + BuildTimeConf.stdlib_dir_devel ] + 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"; + "-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,7 +262,7 @@ 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) @@ -221,9 +283,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 +300,6 @@ let parse_cmdline () = let fill_registry () = status := fill_registry !status +;; +Inversion_principle.init ()