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";
57 let set_registry_values =
60 if not (Helm_registry.has key) then Helm_registry.set ~key ~value)
62 let fill_registry 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_environment init_status =
106 wants [CmdLine] init_status;
107 if not (already_configured [Getter;Environment] init_status) then
110 if Helm_registry.get_bool "matita.system" then
111 Http_getter_storage.activate_system_mode ();
112 CicEnvironment.set_trust (* environment trust *)
114 Helm_registry.get_opt_default Helm_registry.get_bool
115 ~default:true "matita.environment_trust" in
117 Getter::Environment::init_status
124 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
127 (fun (name, s) -> Hashtbl.replace usages name s)
129 Printf.sprintf "MatitaC v%s
130 Usage: matitac [ OPTION ... ] FILE
132 BuildTimeConf.version;
134 Printf.sprintf "Grafite Grep v%s
135 Usage: gragrep [ -r ] PATH
137 BuildTimeConf.version;
139 Printf.sprintf "Matita's prover v%s
140 Usage: matitaprover [ -tptppath ] FILE.p
142 BuildTimeConf.version;
144 Printf.sprintf "Matita v%s
145 Usage: matita [ OPTION ... ] [ FILE ... ]
147 BuildTimeConf.version;
151 Usage: cicbrowser [ URL | WHELP QUERY ]
153 BuildTimeConf.version;
155 Printf.sprintf "MatitaDep v%s
156 Usage: matitadep [ OPTION ... ] FILE ...
158 BuildTimeConf.version;
160 Printf.sprintf "MatitaClean v%s
161 Usage: matitaclean all
162 matitaclean [ (FILE | URI) ... ]
164 BuildTimeConf.version;
166 Printf.sprintf "MatitaMake v%s
167 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
169 Parameters: name (the name of the development, required)
170 root (the directory in which the delopment is rooted,
171 optional, default is current working directory)
172 Description: tells matitamake that a new development radicated
173 in the current working directory should be handled.
175 Parameters: name (the name of the development to destroy, optional)
176 If omitted the development that holds the current working
177 directory is used (if any).
178 Description: clean the develpoment.
181 Description: lists the known developments and their roots.
183 Parameters: name (the name of the development to destroy, required)
184 Description: deletes a development (only from matitamake metadat, no
185 .ma files will be deleted).
187 Parameters: name (the name of the development to build, required)
188 Description: completely builds the develpoment.
190 Parameters: name (the name of the development to publish, required)
191 Description: cleans the development in the user space, rebuilds it
192 in the system space ('ro' repositories, that for this operation
195 If target is omitted an 'all' will be used as the default.
196 With -build you can build a development wherever it is.
197 If you specify a target it implicitly refers to the development that
198 holds the current working directory (if any).
200 BuildTimeConf.version;
204 "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
207 let basename = Filename.basename Sys.argv.(0) in
209 try Filename.chop_extension basename with Invalid_argument _ -> basename
211 try Hashtbl.find usages usage_key with Not_found -> default_usage
213 let extra_cmdline_specs = ref []
214 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
216 let parse_cmdline init_status =
217 if not (already_configured [CmdLine] init_status) then begin
218 wants [Registry] init_status;
219 let includes = ref [] in
220 let default_includes = [
222 BuildTimeConf.stdlib_dir_devel;
223 BuildTimeConf.stdlib_dir_installed ; ]
226 if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
229 let add_l l = fun s -> l := s :: !l in
230 let print_version () =
231 Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
232 let no_innertypes () =
233 Helm_registry.set_bool "matita.noinnertypes" true in
235 match Str.split (Str.regexp "::") s with
236 | [path; uri] -> Helm_registry.set "matita.baseuri"
237 (HExtlib.normalize_path (absolutize path)^" "^uri)
238 | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
242 "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
243 "-I", Arg.String (add_l includes),
244 ("<path> Adds path to the list of searched paths for the "
245 ^ "include command");
246 "-conffile", Arg.Set_string conffile,
247 (Printf.sprintf ("<filename> Read configuration from filename"
249 BuildTimeConf.matita_conf);
251 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
252 ("Force actions that would not be executed per default");
254 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
255 "Turns off profiling printings";
256 "-noinnertypes", Arg.Unit no_innertypes,
257 "Turns off inner types generation while publishing";
259 Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
260 "Activates only profiler with label matching the provided regex";
262 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
263 "Turns off automatic baseuri cleaning";
264 "-system", Arg.Unit (fun () ->
265 Helm_registry.set_bool "matita.system" true),
266 ("Act on the system library instead of the user one"
267 ^ "\n WARNING: not for the casual user");
269 Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true),
271 "--version", Arg.Unit print_version, "Prints version";
274 if BuildTimeConf.debug then
276 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
277 ("Do not catch top-level exception "
278 ^ "(useful for backtrace inspection)");
280 Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
281 "Enable only one disambiguation pass";
285 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
287 let set_list ~key l =
288 Helm_registry.set_list Helm_registry.of_string ~key ~value:l
290 Arg.parse arg_spec (add_l args) (usage ());
292 List.map (fun x -> HExtlib.normalize_path (absolutize x))
293 ((List.rev !includes) @ default_includes)
295 set_list ~key:"matita.includes" includes;
296 let args = List.rev (List.filter (fun x -> x <> "") !args) in
297 set_list ~key:"matita.args" args;
298 HExtlib.set_profiling_printings
300 Helm_registry.get_bool "matita.profile" &&
302 ~pat:(Helm_registry.get_opt_default
303 Helm_registry.string ~default:".*" "matita.profile_only")
305 CmdLine :: init_status
310 print_endline (usage ());
313 let conf_components =
314 [ load_configuration; fill_registry; parse_cmdline]
316 let other_components =
317 [ initialize_db; initialize_environment ]
319 let initialize_all () =
321 List.fold_left (fun s f -> f s) !status
322 (conf_components @ other_components)
324 let parse_cmdline_and_configuration_file () =
325 status := List.fold_left (fun s f -> f s) !status conf_components
327 let initialize_environment () =
328 status := initialize_environment !status
331 Inversion_principle.init ()