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 | 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"; (* FIXME, inutile pure lei *)
49 "matita.profile", "true";
50 "matita.system", "false";
51 "matita.verbose", "false";
52 "matita.paste_unicode_as_tex", "false";
53 "matita.noinnertypes", "false";
54 "matita.do_heavy_checks", "true";
58 let set_registry_values =
61 if not (Helm_registry.has key) then 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_environment init_status =
107 wants [CmdLine] 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)
130 Printf.sprintf "MatitaC v%s
131 Usage: matitac [ OPTION ... ] FILE
133 BuildTimeConf.version;
135 Printf.sprintf "Grafite Grep v%s
136 Usage: gragrep [ -r ] PATH
138 BuildTimeConf.version;
140 Printf.sprintf "Matita's prover v%s
141 Usage: matitaprover [ -tptppath ] FILE.p
143 BuildTimeConf.version;
145 Printf.sprintf "Matita v%s
146 Usage: matita [ OPTION ... ] [ FILE ... ]
148 BuildTimeConf.version;
152 Usage: cicbrowser [ URL | WHELP QUERY ]
154 BuildTimeConf.version;
156 Printf.sprintf "MatitaDep v%s
157 Usage: matitadep [ OPTION ... ] FILE ...
159 BuildTimeConf.version;
161 Printf.sprintf "MatitaClean v%s
162 Usage: matitaclean all
163 matitaclean [ (FILE | URI) ... ]
165 BuildTimeConf.version;
167 Printf.sprintf "MatitaMake v%s
168 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
170 Parameters: name (the name of the development, required)
171 root (the directory in which the delopment is rooted,
172 optional, default is current working directory)
173 Description: tells matitamake that a new development radicated
174 in the current working directory should be handled.
176 Parameters: name (the name of the development to destroy, optional)
177 If omitted the development that holds the current working
178 directory is used (if any).
179 Description: clean the develpoment.
182 Description: lists the known developments and their roots.
184 Parameters: name (the name of the development to destroy, required)
185 Description: deletes a development (only from matitamake metadat, no
186 .ma files will be deleted).
188 Parameters: name (the name of the development to build, required)
189 Description: completely builds the develpoment.
191 Parameters: name (the name of the development to publish, required)
192 Description: cleans the development in the user space, rebuilds it
193 in the system space ('ro' repositories, that for this operation
196 If target is omitted an 'all' will be used as the default.
197 With -build you can build a development wherever it is.
198 If you specify a target it implicitly refers to the development that
199 holds the current working directory (if any).
201 BuildTimeConf.version;
205 "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
208 let basename = Filename.basename Sys.argv.(0) in
210 try Filename.chop_extension basename with Invalid_argument _ -> basename
212 try Hashtbl.find usages usage_key with Not_found -> default_usage
214 let extra_cmdline_specs = ref []
215 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
217 let parse_cmdline init_status =
218 if not (already_configured [CmdLine] init_status) then begin
219 wants [Registry] init_status;
220 let includes = ref [] in
221 let default_includes = [
223 BuildTimeConf.stdlib_dir_devel;
224 BuildTimeConf.stdlib_dir_installed ; ]
227 if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
230 let add_l l = fun s -> l := s :: !l in
231 let print_version () =
232 Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
233 let no_innertypes () =
234 Helm_registry.set_bool "matita.noinnertypes" true in
236 match Str.split (Str.regexp "::") s with
237 | [path; uri] -> Helm_registry.set "matita.baseuri"
238 (HExtlib.normalize_path (absolutize path)^" "^uri)
239 | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
243 "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
244 "-I", Arg.String (add_l includes),
245 ("<path> Adds path to the list of searched paths for the "
246 ^ "include command");
247 "-conffile", Arg.Set_string conffile,
248 (Printf.sprintf ("<filename> Read configuration from filename"
250 BuildTimeConf.matita_conf);
252 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
253 ("Force actions that would not be executed per default");
255 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
256 "Turns off profiling printings";
257 "-noinnertypes", Arg.Unit no_innertypes,
258 "Turns off inner types generation while publishing";
260 Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
261 "Activates only profiler with label matching the provided regex";
263 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
264 "Turns off automatic baseuri cleaning";
265 "-system", Arg.Unit (fun () ->
266 Helm_registry.set_bool "matita.system" true),
267 ("Act on the system library instead of the user one"
268 ^ "\n WARNING: not for the casual user");
270 Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true),
272 "--version", Arg.Unit print_version, "Prints version";
275 if BuildTimeConf.debug then
277 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
278 ("Do not catch top-level exception "
279 ^ "(useful for backtrace inspection)");
281 Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
282 "Enable only one disambiguation pass";
286 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
288 let set_list ~key l =
289 Helm_registry.set_list Helm_registry.of_string ~key ~value:l
291 Arg.parse arg_spec (add_l args) (usage ());
293 List.map (fun x -> HExtlib.normalize_path (absolutize x))
294 ((List.rev !includes) @ default_includes)
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 [ load_configuration; fill_registry; parse_cmdline]
317 let other_components =
318 [ initialize_db; initialize_environment ]
320 let initialize_all () =
322 List.fold_left (fun s f -> f s) !status
323 (conf_components @ other_components)
325 let parse_cmdline_and_configuration_file () =
326 status := List.fold_left (fun s f -> f s) !status conf_components
328 let initialize_environment () =
329 status := initialize_environment !status
332 Inversion_principle.init ()