1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 type thingsToInitilaize =
31 ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
33 exception FailedToInitialize of thingsToInitilaize
38 if not (List.exists (fun x -> x = item) l) then
39 raise (FailedToInitialize item))
42 let already_configured s l =
43 List.for_all (fun item -> List.exists (fun x -> x = item) l) s
45 let conffile = ref BuildTimeConf.matita_conf
47 let registry_defaults = [
49 "matita.debug", "false";
50 "matita.external_editor", "gvim -f -c 'go %p' %f";
51 "matita.preserve", "false";
52 "matita.profile", "true";
53 "matita.system", "false";
54 "matita.verbosity", "1";
55 "matita.bench", "false";
56 (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
57 * intuitively verbose *)
60 let set_registry_values =
61 List.iter (fun key, value -> Helm_registry.set ~key ~value)
63 let fill_registry init_status =
64 if not (already_configured [ Registry ] init_status) then begin
65 set_registry_values registry_defaults;
66 Registry :: init_status
70 let load_configuration init_status =
71 wants [ Registry ] init_status;
72 if not (already_configured [ConfigurationFile] init_status) then
74 Helm_registry.load_from !conffile;
75 if not (Helm_registry.has "user.name") then begin
76 let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
77 Helm_registry.set "user.name" login
79 ConfigurationFile::init_status
84 let initialize_db init_status =
85 wants [ ConfigurationFile; CmdLine ] init_status;
86 if not (already_configured [ Db ] init_status) then
88 if not (Helm_registry.get_bool "matita.system") then
89 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
90 LibraryDb.create_owner_environment ();
96 let initialize_makelib init_status =
97 wants [ConfigurationFile] init_status;
98 if not (already_configured [Makelib] init_status) then
100 MatitamakeLib.initialize ();
106 let initialize_environment init_status =
107 wants [ConfigurationFile] init_status;
108 if not (already_configured [Getter;Environment] init_status) then
111 if Helm_registry.get_bool "matita.system" then
112 Http_getter_storage.activate_system_mode ();
113 CicEnvironment.set_trust (* environment trust *)
115 Helm_registry.get_opt_default Helm_registry.get_bool
116 ~default:true "matita.environment_trust" in
118 Getter::Environment::init_status
125 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
128 (fun (name, s) -> Hashtbl.replace usages name s)
131 Usage: matitac [ OPTION ... ] FILE
133 BuildTimeConf.version;
135 sprintf "Grafite Grep v%s
136 Usage: gragrep [ -r ] PATH
138 BuildTimeConf.version;
141 Usage: matita [ OPTION ... ] [ FILE ... ]
143 BuildTimeConf.version;
147 Usage: cicbrowser [ URL | WHELP QUERY ]
149 BuildTimeConf.version;
151 sprintf "MatitaDep v%s
152 Usage: matitadep [ OPTION ... ] FILE ...
154 BuildTimeConf.version;
156 sprintf "MatitaClean v%s
157 Usage: matitaclean all
158 matitaclean [ (FILE | URI) ... ]
160 BuildTimeConf.version;
162 sprintf "MatitaMake v%s
163 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
165 Parameters: name (the name of the development, required)
166 Description: tells matitamake that a new development radicated
167 in the current working directory should be handled.
169 Parameters: name (the name of the development to destroy, optional)
170 If omitted the development that holds the current working
171 directory is used (if any).
172 Description: clean the develpoment.
175 Description: lists the known developments and their roots.
177 Parameters: name (the name of the development to destroy, required)
178 Description: deletes a development (only from matitamake metadat, no
179 .ma files will be deleted).
181 Parameters: name (the name of the development to build, required)
182 Description: completely builds the develpoment.
184 Parameters: name (the name of the development to publish, required)
185 Description: cleans the development in the user space, rebuilds it
186 in the system space ('ro' repositories, that for this operation
189 If target is omitted an 'all' will be used as the default.
190 With -build you can build a development wherever it is.
191 If you specify a target it implicitly refers to the development that
192 holds the current working directory (if any).
194 BuildTimeConf.version;
197 sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
200 let basename = Filename.basename Sys.argv.(0) in
202 try Filename.chop_extension basename with Invalid_argument _ -> basename
204 try Hashtbl.find usages usage_key with Not_found -> default_usage
206 let extra_cmdline_specs = ref []
207 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
209 let parse_cmdline init_status =
210 if not (already_configured [CmdLine] init_status) then begin
212 BuildTimeConf.stdlib_dir_installed ;
213 BuildTimeConf.stdlib_dir_devel ]
216 let add_l l = fun s -> l := s :: !l in
217 let reduce_verbosity () =
218 Helm_registry.set_int "matita.verbosity"
219 (Helm_registry.get_int "matita.verbosity" - 1) in
220 let increase_verbosity () =
221 Helm_registry.set_int "matita.verbosity"
222 (Helm_registry.get_int "matita.verbosity" + 1) in
225 "-I", Arg.String (add_l includes),
226 ("<path> Adds path to the list of searched paths for the "
227 ^ "include command");
228 "-conffile", Arg.Set_string conffile,
229 (Printf.sprintf ("<filename> Read configuration from filename"
231 BuildTimeConf.matita_conf);
233 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
234 ("Force actions that would not be executed per default");
235 "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
236 ("Avoid using external database connection"
237 ^ "\n WARNING: disable many features");
239 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
240 "Turns off profiling printings";
242 Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
243 "Turns on timing prints";
245 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
246 "Turns off automatic baseuri cleaning";
247 "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
248 "-system", Arg.Unit (fun () ->
249 Helm_registry.set_bool "matita.system" true),
250 ("Act on the system library instead of the user one"
251 ^ "\n WARNING: not for the casual user");
252 "-v", Arg.Unit increase_verbosity, "Increase verbosity";
255 if BuildTimeConf.debug then
257 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
258 ("Do not catch top-level exception "
259 ^ "(useful for backtrace inspection)");
263 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
265 let set_list ~key l =
266 Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
268 Arg.parse arg_spec (add_l args) (usage ());
269 set_list ~key:"matita.includes" includes;
270 set_list ~key:"matita.args" args;
271 HExtlib.set_profiling_printings
272 (fun () -> Helm_registry.get_bool "matita.profile");
273 CmdLine :: init_status
278 print_endline (usage ());
281 let initialize_all () =
283 List.fold_left (fun s f -> f s) !status
284 [ fill_registry; parse_cmdline; load_configuration; initialize_makelib;
285 initialize_db; initialize_environment ]
286 (* initialize_notation
287 (initialize_environment
291 (parse_cmdline !status))))) *)
293 let load_configuration_file () =
294 status := load_configuration !status
296 let parse_cmdline () =
297 status := parse_cmdline !status
299 let fill_registry () =
300 status := fill_registry !status
303 Inversion_principle.init ()