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/
28 type thingsToInitilaize =
29 ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
31 exception FailedToInitialize of thingsToInitilaize
36 if not (List.exists (fun x -> x = item) l) then
37 raise (FailedToInitialize item))
40 let already_configured s l =
41 List.for_all (fun item -> List.exists (fun x -> x = item) l) s
43 let conffile = ref BuildTimeConf.matita_conf
45 let registry_defaults = [
46 "matita.debug", "false";
47 "matita.external_editor", "gvim -f -c 'go %p' %f";
48 "matita.preserve", "false";
49 "matita.profile", "true";
50 "matita.system", "false";
51 "matita.verbosity", "1";
52 "matita.bench", "false";
53 "matita.paste_unicode_as_tex", "false"
54 (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
55 * intuitively verbose *)
58 let set_registry_values =
59 List.iter (fun key, value -> Helm_registry.set ~key ~value)
61 let fill_registry init_status =
62 wants [ ConfigurationFile ] init_status;
63 if not (already_configured [ Registry ] init_status) then begin
64 set_registry_values registry_defaults;
65 Registry :: init_status
69 let load_configuration init_status =
70 if not (already_configured [ConfigurationFile] init_status) then
72 Helm_registry.load_from !conffile;
73 if not (Helm_registry.has "user.name") then begin
74 let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
75 Helm_registry.set "user.name" login
77 let home = Helm_registry.get_string "matita.basedir" in
78 let user_conf_file = home ^ "/matita.conf.xml" in
79 if HExtlib.is_regular user_conf_file then
81 HLog.message ("Loading additional conf file from " ^ user_conf_file);
83 Helm_registry.load_from user_conf_file
86 ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
88 ConfigurationFile::init_status
93 let initialize_db init_status =
94 wants [ ConfigurationFile; CmdLine ] init_status;
95 if not (already_configured [ Db ] init_status) then
97 if not (Helm_registry.get_bool "matita.system") then
98 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
99 LibraryDb.create_owner_environment ();
105 let initialize_makelib init_status =
106 wants [ConfigurationFile] init_status;
107 if not (already_configured [Makelib] init_status) then
109 MatitamakeLib.initialize ();
115 let initialize_environment init_status =
116 wants [ConfigurationFile] init_status;
117 if not (already_configured [Getter;Environment] init_status) then
120 if Helm_registry.get_bool "matita.system" then
121 Http_getter_storage.activate_system_mode ();
122 CicEnvironment.set_trust (* environment trust *)
124 Helm_registry.get_opt_default Helm_registry.get_bool
125 ~default:true "matita.environment_trust" in
127 Getter::Environment::init_status
134 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
137 (fun (name, s) -> Hashtbl.replace usages name s)
139 Printf.sprintf "MatitaC v%s
140 Usage: matitac [ OPTION ... ] FILE
142 BuildTimeConf.version;
144 Printf.sprintf "Grafite Grep v%s
145 Usage: gragrep [ -r ] PATH
147 BuildTimeConf.version;
149 Printf.sprintf "Matita's prover v%s
150 Usage: matitaprover [ -tptppath ] FILE.p
152 BuildTimeConf.version;
154 Printf.sprintf "Matita v%s
155 Usage: matita [ OPTION ... ] [ FILE ... ]
157 BuildTimeConf.version;
161 Usage: cicbrowser [ URL | WHELP QUERY ]
163 BuildTimeConf.version;
165 Printf.sprintf "MatitaDep v%s
166 Usage: matitadep [ OPTION ... ] FILE ...
168 BuildTimeConf.version;
170 Printf.sprintf "MatitaClean v%s
171 Usage: matitaclean all
172 matitaclean [ (FILE | URI) ... ]
174 BuildTimeConf.version;
176 Printf.sprintf "MatitaMake v%s
177 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
179 Parameters: name (the name of the development, required)
180 root (the directory in which the delopment is rooted,
181 optional, default is current working directory)
182 Description: tells matitamake that a new development radicated
183 in the current working directory should be handled.
185 Parameters: name (the name of the development to destroy, optional)
186 If omitted the development that holds the current working
187 directory is used (if any).
188 Description: clean the develpoment.
191 Description: lists the known developments and their roots.
193 Parameters: name (the name of the development to destroy, required)
194 Description: deletes a development (only from matitamake metadat, no
195 .ma files will be deleted).
197 Parameters: name (the name of the development to build, required)
198 Description: completely builds the develpoment.
200 Parameters: name (the name of the development to publish, required)
201 Description: cleans the development in the user space, rebuilds it
202 in the system space ('ro' repositories, that for this operation
205 If target is omitted an 'all' will be used as the default.
206 With -build you can build a development wherever it is.
207 If you specify a target it implicitly refers to the development that
208 holds the current working directory (if any).
210 BuildTimeConf.version;
214 "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
217 let basename = Filename.basename Sys.argv.(0) in
219 try Filename.chop_extension basename with Invalid_argument _ -> basename
221 try Hashtbl.find usages usage_key with Not_found -> default_usage
223 let extra_cmdline_specs = ref []
224 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
226 let parse_cmdline init_status =
227 if not (already_configured [CmdLine] init_status) then begin
228 let includes = ref [] in
229 let default_includes = [
231 BuildTimeConf.stdlib_dir_devel;
232 BuildTimeConf.stdlib_dir_installed ; ]
235 if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s
238 let add_l l = fun s -> l := s :: !l in
239 let reduce_verbosity () =
240 Helm_registry.set_int "matita.verbosity"
241 (Helm_registry.get_int "matita.verbosity" - 1) in
242 let increase_verbosity () =
243 Helm_registry.set_int "matita.verbosity"
244 (Helm_registry.get_int "matita.verbosity" + 1) in
247 "-I", Arg.String (add_l includes),
248 ("<path> Adds path to the list of searched paths for the "
249 ^ "include command");
250 "-conffile", Arg.Set_string conffile,
251 (Printf.sprintf ("<filename> Read configuration from filename"
253 BuildTimeConf.matita_conf);
255 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
256 ("Force actions that would not be executed per default");
258 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
259 "Turns off profiling printings";
261 Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
262 "Activates only profiler with label matching the provided regex";
264 Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
265 "Turns on parsable output on stdout, that is timings for matitac...";
267 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
268 "Turns off automatic baseuri cleaning";
269 "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
270 "-system", Arg.Unit (fun () ->
271 Helm_registry.set_bool "matita.system" true),
272 ("Act on the system library instead of the user one"
273 ^ "\n WARNING: not for the casual user");
274 "-v", Arg.Unit increase_verbosity, "Increase verbosity";
277 if BuildTimeConf.debug then
279 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
280 ("Do not catch top-level exception "
281 ^ "(useful for backtrace inspection)");
283 Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
284 "Enable only one disambiguation pass";
288 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
290 let set_list ~key l =
291 Helm_registry.set_list Helm_registry.of_string ~key ~value:l
293 Arg.parse arg_spec (add_l args) (usage ());
295 List.map absolutize ((List.rev !includes) @ default_includes) in
296 set_list ~key:"matita.includes" includes;
297 let args = List.rev (List.filter (fun x -> x <> "") !args) in
298 set_list ~key:"matita.args" args;
299 HExtlib.set_profiling_printings
301 Helm_registry.get_bool "matita.profile" &&
303 ~pat:(Helm_registry.get_opt_default
304 Helm_registry.string ~default:".*" "matita.profile_only")
306 CmdLine :: init_status
311 print_endline (usage ());
314 let conf_components =
315 [ parse_cmdline; load_configuration; fill_registry ]
317 let other_components =
318 [ initialize_makelib; initialize_db; initialize_environment ]
320 let initialize_all () =
322 List.fold_left (fun s f -> f s) !status
323 (conf_components @ other_components)
324 (* initialize_notation
325 (initialize_environment
329 (parse_cmdline !status))))) *)
331 let parse_cmdline_and_configuration_file () =
332 status := List.fold_left (fun s f -> f s) !status conf_components
336 Inversion_principle.init ()