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 =
63 if not (Helm_registry.has key) then Helm_registry.set ~key ~value)
65 let fill_registry init_status =
66 if not (already_configured [ Registry ] init_status) then begin
67 set_registry_values registry_defaults;
68 Registry :: init_status
72 let load_configuration init_status =
73 if not (already_configured [ConfigurationFile] init_status) then
75 Helm_registry.load_from !conffile;
76 if not (Helm_registry.has "user.name") then begin
77 let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
78 Helm_registry.set "user.name" login
80 let home = Helm_registry.get_string "matita.basedir" in
81 let user_conf_file = home ^ "/matita.conf.xml" in
82 if HExtlib.is_regular user_conf_file then
84 HLog.message ("Loading additional conf file from " ^ user_conf_file);
86 Helm_registry.load_from user_conf_file
89 ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
91 ConfigurationFile::init_status
96 let initialize_db init_status =
97 wants [ ConfigurationFile; CmdLine ] init_status;
98 if not (already_configured [ Db ] init_status) then
100 if not (Helm_registry.get_bool "matita.system") then
101 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
102 LibraryDb.create_owner_environment ();
108 let initialize_makelib init_status =
109 wants [ConfigurationFile] init_status;
110 if not (already_configured [Makelib] init_status) then
112 MatitamakeLib.initialize ();
118 let initialize_environment init_status =
119 wants [CmdLine] init_status;
120 if not (already_configured [Getter;Environment] init_status) then
123 if Helm_registry.get_bool "matita.system" then
124 Http_getter_storage.activate_system_mode ();
125 CicEnvironment.set_trust (* environment trust *)
127 Helm_registry.get_opt_default Helm_registry.get_bool
128 ~default:true "matita.environment_trust" in
130 Getter::Environment::init_status
137 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
140 (fun (name, s) -> Hashtbl.replace usages name s)
142 Printf.sprintf "MatitaC v%s
143 Usage: matitac [ OPTION ... ] FILE
145 BuildTimeConf.version;
147 Printf.sprintf "Grafite Grep v%s
148 Usage: gragrep [ -r ] PATH
150 BuildTimeConf.version;
152 Printf.sprintf "Matita's prover v%s
153 Usage: matitaprover [ -tptppath ] FILE.p
155 BuildTimeConf.version;
157 Printf.sprintf "Matita v%s
158 Usage: matita [ OPTION ... ] [ FILE ... ]
160 BuildTimeConf.version;
164 Usage: cicbrowser [ URL | WHELP QUERY ]
166 BuildTimeConf.version;
168 Printf.sprintf "MatitaDep v%s
169 Usage: matitadep [ OPTION ... ] FILE ...
171 BuildTimeConf.version;
173 Printf.sprintf "MatitaClean v%s
174 Usage: matitaclean all
175 matitaclean [ (FILE | URI) ... ]
177 BuildTimeConf.version;
179 Printf.sprintf "MatitaMake v%s
180 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
182 Parameters: name (the name of the development, required)
183 root (the directory in which the delopment is rooted,
184 optional, default is current working directory)
185 Description: tells matitamake that a new development radicated
186 in the current working directory should be handled.
188 Parameters: name (the name of the development to destroy, optional)
189 If omitted the development that holds the current working
190 directory is used (if any).
191 Description: clean the develpoment.
194 Description: lists the known developments and their roots.
196 Parameters: name (the name of the development to destroy, required)
197 Description: deletes a development (only from matitamake metadat, no
198 .ma files will be deleted).
200 Parameters: name (the name of the development to build, required)
201 Description: completely builds the develpoment.
203 Parameters: name (the name of the development to publish, required)
204 Description: cleans the development in the user space, rebuilds it
205 in the system space ('ro' repositories, that for this operation
208 If target is omitted an 'all' will be used as the default.
209 With -build you can build a development wherever it is.
210 If you specify a target it implicitly refers to the development that
211 holds the current working directory (if any).
213 BuildTimeConf.version;
217 "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
220 let basename = Filename.basename Sys.argv.(0) in
222 try Filename.chop_extension basename with Invalid_argument _ -> basename
224 try Hashtbl.find usages usage_key with Not_found -> default_usage
226 let extra_cmdline_specs = ref []
227 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
229 let parse_cmdline init_status =
230 if not (already_configured [CmdLine] init_status) then begin
231 wants [Registry] init_status;
232 let includes = ref [] in
233 let default_includes = [
235 BuildTimeConf.stdlib_dir_devel;
236 BuildTimeConf.stdlib_dir_installed ; ]
239 if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s
242 let add_l l = fun s -> l := s :: !l in
243 let reduce_verbosity () =
244 Helm_registry.set_int "matita.verbosity"
245 (Helm_registry.get_int "matita.verbosity" - 1) in
246 let print_version () =
247 Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
248 let increase_verbosity () =
249 Helm_registry.set_int "matita.verbosity"
250 (Helm_registry.get_int "matita.verbosity" + 1) in
251 let no_innertypes () =
252 Helm_registry.set_bool "matita.noinnertypes" true in
255 "-I", Arg.String (add_l includes),
256 ("<path> Adds path to the list of searched paths for the "
257 ^ "include command");
258 "-conffile", Arg.Set_string conffile,
259 (Printf.sprintf ("<filename> Read configuration from filename"
261 BuildTimeConf.matita_conf);
263 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
264 ("Force actions that would not be executed per default");
266 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
267 "Turns off profiling printings";
268 "-noinnertypes", Arg.Unit no_innertypes,
269 "Turns off inner types generation while publishing";
271 Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
272 "Activates only profiler with label matching the provided regex";
274 Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
275 "Turns on parsable output on stdout, that is timings for matitac...";
277 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
278 "Turns off automatic baseuri cleaning";
279 "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
280 "-system", Arg.Unit (fun () ->
281 Helm_registry.set_bool "matita.system" true),
282 ("Act on the system library instead of the user one"
283 ^ "\n WARNING: not for the casual user");
284 "-v", Arg.Unit increase_verbosity, "Increase verbosity";
285 "--version", Arg.Unit print_version, "Prints version";
288 if BuildTimeConf.debug then
290 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
291 ("Do not catch top-level exception "
292 ^ "(useful for backtrace inspection)");
294 Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
295 "Enable only one disambiguation pass";
299 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
301 let set_list ~key l =
302 Helm_registry.set_list Helm_registry.of_string ~key ~value:l
304 Arg.parse arg_spec (add_l args) (usage ());
306 List.map absolutize ((List.rev !includes) @ default_includes) in
307 set_list ~key:"matita.includes" includes;
308 let args = List.rev (List.filter (fun x -> x <> "") !args) in
309 set_list ~key:"matita.args" args;
310 HExtlib.set_profiling_printings
312 Helm_registry.get_bool "matita.profile" &&
314 ~pat:(Helm_registry.get_opt_default
315 Helm_registry.string ~default:".*" "matita.profile_only")
317 CmdLine :: init_status
322 print_endline (usage ());
325 let conf_components =
326 [ load_configuration; fill_registry; parse_cmdline]
328 let other_components =
329 [ initialize_makelib; initialize_db; initialize_environment ]
331 let initialize_all () =
333 List.fold_left (fun s f -> f s) !status
334 (conf_components @ other_components)
335 (* initialize_notation
336 (initialize_environment
340 (parse_cmdline !status))))) *)
342 let parse_cmdline_and_configuration_file () =
343 status := List.fold_left (fun s f -> f s) !status conf_components
345 let initialize_environment () =
346 status := initialize_environment !status
349 Inversion_principle.init ()