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 "matita.noinnertypes", "false";
55 "matita.do_heavy_checks", "true";
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 if not (already_configured [ConfigurationFile] init_status) then
73 Helm_registry.load_from !conffile;
74 if not (Helm_registry.has "user.name") then begin
75 let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
76 Helm_registry.set "user.name" login
78 let home = Helm_registry.get_string "matita.basedir" in
79 let user_conf_file = home ^ "/matita.conf.xml" in
80 if HExtlib.is_regular user_conf_file then
82 HLog.message ("Loading additional conf file from " ^ user_conf_file);
84 Helm_registry.load_from user_conf_file
87 ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
89 ConfigurationFile::init_status
94 let initialize_db init_status =
95 wants [ ConfigurationFile; CmdLine ] init_status;
96 if not (already_configured [ Db ] init_status) then
98 if not (Helm_registry.get_bool "matita.system") then
99 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
100 LibraryDb.create_owner_environment ();
106 let initialize_makelib init_status =
107 wants [ConfigurationFile] init_status;
108 if not (already_configured [Makelib] init_status) then
110 MatitamakeLib.initialize ();
116 let initialize_environment init_status =
117 wants [CmdLine] init_status;
118 if not (already_configured [Getter;Environment] init_status) then
121 if Helm_registry.get_bool "matita.system" then
122 Http_getter_storage.activate_system_mode ();
123 CicEnvironment.set_trust (* environment trust *)
125 Helm_registry.get_opt_default Helm_registry.get_bool
126 ~default:true "matita.environment_trust" in
128 Getter::Environment::init_status
135 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
138 (fun (name, s) -> Hashtbl.replace usages name s)
140 Printf.sprintf "MatitaC v%s
141 Usage: matitac [ OPTION ... ] FILE
143 BuildTimeConf.version;
145 Printf.sprintf "Grafite Grep v%s
146 Usage: gragrep [ -r ] PATH
148 BuildTimeConf.version;
150 Printf.sprintf "Matita's prover v%s
151 Usage: matitaprover [ -tptppath ] FILE.p
153 BuildTimeConf.version;
155 Printf.sprintf "Matita v%s
156 Usage: matita [ OPTION ... ] [ FILE ... ]
158 BuildTimeConf.version;
162 Usage: cicbrowser [ URL | WHELP QUERY ]
164 BuildTimeConf.version;
166 Printf.sprintf "MatitaDep v%s
167 Usage: matitadep [ OPTION ... ] FILE ...
169 BuildTimeConf.version;
171 Printf.sprintf "MatitaClean v%s
172 Usage: matitaclean all
173 matitaclean [ (FILE | URI) ... ]
175 BuildTimeConf.version;
177 Printf.sprintf "MatitaMake v%s
178 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
180 Parameters: name (the name of the development, required)
181 root (the directory in which the delopment is rooted,
182 optional, default is current working directory)
183 Description: tells matitamake that a new development radicated
184 in the current working directory should be handled.
186 Parameters: name (the name of the development to destroy, optional)
187 If omitted the development that holds the current working
188 directory is used (if any).
189 Description: clean the develpoment.
192 Description: lists the known developments and their roots.
194 Parameters: name (the name of the development to destroy, required)
195 Description: deletes a development (only from matitamake metadat, no
196 .ma files will be deleted).
198 Parameters: name (the name of the development to build, required)
199 Description: completely builds the develpoment.
201 Parameters: name (the name of the development to publish, required)
202 Description: cleans the development in the user space, rebuilds it
203 in the system space ('ro' repositories, that for this operation
206 If target is omitted an 'all' will be used as the default.
207 With -build you can build a development wherever it is.
208 If you specify a target it implicitly refers to the development that
209 holds the current working directory (if any).
211 BuildTimeConf.version;
215 "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
218 let basename = Filename.basename Sys.argv.(0) in
220 try Filename.chop_extension basename with Invalid_argument _ -> basename
222 try Hashtbl.find usages usage_key with Not_found -> default_usage
224 let extra_cmdline_specs = ref []
225 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
227 let parse_cmdline init_status =
228 if not (already_configured [CmdLine] init_status) then begin
229 wants [Registry] init_status;
230 let includes = ref [] in
231 let default_includes = [
233 BuildTimeConf.stdlib_dir_devel;
234 BuildTimeConf.stdlib_dir_installed ; ]
237 if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s
240 let add_l l = fun s -> l := s :: !l in
241 let reduce_verbosity () =
242 Helm_registry.set_int "matita.verbosity"
243 (Helm_registry.get_int "matita.verbosity" - 1) in
244 let print_version () =
245 Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
246 let increase_verbosity () =
247 Helm_registry.set_int "matita.verbosity"
248 (Helm_registry.get_int "matita.verbosity" + 1) in
249 let no_innertypes () =
250 Helm_registry.set_bool "matita.noinnertypes" true in
253 "-I", Arg.String (add_l includes),
254 ("<path> Adds path to the list of searched paths for the "
255 ^ "include command");
256 "-conffile", Arg.Set_string conffile,
257 (Printf.sprintf ("<filename> Read configuration from filename"
259 BuildTimeConf.matita_conf);
261 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
262 ("Force actions that would not be executed per default");
264 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
265 "Turns off profiling printings";
266 "-noinnertypes", Arg.Unit no_innertypes,
267 "Turns off inner types generation while publishing";
269 Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
270 "Activates only profiler with label matching the provided regex";
272 Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
273 "Turns on parsable output on stdout, that is timings for matitac...";
275 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
276 "Turns off automatic baseuri cleaning";
277 "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
278 "-system", Arg.Unit (fun () ->
279 Helm_registry.set_bool "matita.system" true),
280 ("Act on the system library instead of the user one"
281 ^ "\n WARNING: not for the casual user");
282 "-v", Arg.Unit increase_verbosity, "Increase verbosity";
283 "--version", Arg.Unit print_version, "Prints version";
286 if BuildTimeConf.debug then
288 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
289 ("Do not catch top-level exception "
290 ^ "(useful for backtrace inspection)");
292 Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
293 "Enable only one disambiguation pass";
297 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
299 let set_list ~key l =
300 Helm_registry.set_list Helm_registry.of_string ~key ~value:l
302 Arg.parse arg_spec (add_l args) (usage ());
304 List.map absolutize ((List.rev !includes) @ default_includes) in
305 set_list ~key:"matita.includes" includes;
306 let args = List.rev (List.filter (fun x -> x <> "") !args) in
307 set_list ~key:"matita.args" args;
308 HExtlib.set_profiling_printings
310 Helm_registry.get_bool "matita.profile" &&
312 ~pat:(Helm_registry.get_opt_default
313 Helm_registry.string ~default:".*" "matita.profile_only")
315 CmdLine :: init_status
320 print_endline (usage ());
323 let conf_components =
324 [ load_configuration; fill_registry; parse_cmdline]
326 let other_components =
327 [ initialize_makelib; initialize_db; initialize_environment ]
329 let initialize_all () =
331 List.fold_left (fun s f -> f s) !status
332 (conf_components @ other_components)
333 (* initialize_notation
334 (initialize_environment
338 (parse_cmdline !status))))) *)
340 let parse_cmdline_and_configuration_file () =
341 status := List.fold_left (fun s f -> f s) !status conf_components
343 let initialize_environment () =
344 status := initialize_environment !status
347 Inversion_principle.init ()