From: Stefano Zacchiroli Date: Mon, 6 Feb 2006 17:19:28 +0000 (+0000) Subject: - uniformed command line handling of matitamake with that of other matita tools X-Git-Tag: make_still_working~7623 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76566c28a29c9f80bea13fb72c57d6a881fb3544;p=helm.git - uniformed command line handling of matitamake with that of other matita tools - changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1 unit - added "-v" flag: it increase the "matita.verbosity" value by 1 - "matita.quiet" is no longer in use --- diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 53ff6b9d6..a135fec80 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -44,16 +44,17 @@ 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"; + (** 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 +75,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 @@ -120,7 +119,7 @@ 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) @@ -149,6 +148,35 @@ 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) + 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. +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; ] @@ -167,29 +195,39 @@ let parse_cmdline init_status = let includes = ref [ BuildTimeConf.stdlib_dir ] 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"; "-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 @@ -221,9 +259,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 diff --git a/helm/software/matita/matitamake.ml b/helm/software/matita/matitamake.ml index f0e17eb8b..36cf79b36 100644 --- a/helm/software/matita/matitamake.ml +++ b/helm/software/matita/matitamake.ml @@ -29,6 +29,7 @@ module MK = MatitamakeLib ;; let main () = MatitaInit.fill_registry (); + MatitaInit.parse_cmdline (); MatitaInit.load_configuration_file (); MK.initialize (); let usage = ref (fun () -> ()) in @@ -46,21 +47,18 @@ let main () = exit 1 | Some d -> d in - let init_dev_doc = " -\tParameters: name (the name of the development, required) -\tDescription: tells matitamake that a new development radicated -\t\tin the current working directory should be handled." - in let init_dev args = - if List.length args <> 1 then !usage (); - match MK.initialize_development (List.hd args) (Unix.getcwd ()) with + let name, path = + match args with + | [ name; path ] when path.[0] = '/' -> name, path + | [ name; path ] -> name, Unix.getcwd () ^ "/" ^ path + | [ name ] -> name, Unix.getcwd () + | _ -> !usage (); (* should not be reached *) assert false + in + match MK.initialize_development name path with | None -> exit 2 | Some _ -> exit 0 in - let list_dev_doc = " -\tParameters: -\tDescription: lists the known developments and their roots." - in let list_dev args = if List.length args <> 0 then !usage (); match MK.list_known_developments () with @@ -72,11 +70,6 @@ let main () = l; exit 0 in - let destroy_dev_doc = " -\tParameters: name (the name of the development to destroy, required) -\tDescription: deletes a development (only from matitamake metadat, no -\t\t.ma files will be deleted)." - in let destroy_dev args = if List.length args <> 1 then !usage (); let name = (List.hd args) in @@ -84,12 +77,6 @@ let main () = MK.destroy_development dev; exit 0 in - let clean_dev_doc = " -\tParameters: name (the name of the development to destroy, optional) -\t\tIf omitted the development that holds the current working -\t\tdirectory is used (if any). -\tDescription: clean the develpoment." - in let clean_dev args = let dev = match args with @@ -101,10 +88,6 @@ let main () = | true -> exit 0 | false -> exit 1 in - let build_dev_doc = " -\tParameters: name (the name of the development to build, required) -\tDescription: completely builds the develpoment." - in let build_dev args = if List.length args <> 1 then !usage (); let name = (List.hd args) in @@ -113,11 +96,6 @@ let main () = | true -> exit 0 | false -> exit 1 in - let nodb_doc = " -\tParameters: -\tDescription: avoid using external database connection." - in - let nodb _ = Helm_registry.set_bool "db.nodb" true in let target args = if List.length args < 1 then !usage (); let dev = dev_for_dir (Unix.getcwd ()) in @@ -127,37 +105,20 @@ let main () = args in let params = [ - "-init", init_dev, init_dev_doc; - "-clean", clean_dev, clean_dev_doc; - "-list", list_dev, list_dev_doc; - "-destroy", destroy_dev, destroy_dev_doc; - "-build", build_dev, build_dev_doc; - "-nodb", nodb, nodb_doc; - "-h", (fun _ -> !usage()), "print this help screen"; - "-help", (fun _ -> !usage()), "print this help screen"; + "init", init_dev; + "clean", clean_dev; + "list", list_dev; + "destroy", destroy_dev; + "build", build_dev; ] in - usage := (fun () -> - let p = prerr_endline in - p "\nusage:"; - p "\tmatitamake(.opt) [command [options]]\n"; - p "\tmatitamake(.opt) [target]\n"; - p "commands:"; - List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params; - p "\nIf target is omitted a 'all' will be used as the default."; - p "With -build you can build a development wherever it is."; - p "If you specify a target it implicitly refers to the development that"; - p "holds the current working directory (if any).\n"; - exit 1); - let rec parse args = + usage := MatitaInit.die_usage; + let parse args = match args with - | [] -> target ["all"] - | s::tl -> - try - let _,f,_ = List.find (fun (n,_,_) -> n = s) params in - f tl; - parse tl + | [] -> target [ "all" ] + | s :: tl -> + try (List.assoc s params) tl with Not_found -> if s.[0] = '-' then !usage () else target args in - parse (List.tl (Array.to_list Sys.argv)) + parse (Helm_registry.get_list Helm_registry.string "matita.args")