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/
30 type thingsToInitilaize =
31 ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
33 exception FailedToInitialize of thingsToInitilaize
38 if not (List.exists (fun x -> x = item) l) then
39 raise (FailedToInitialize item))
42 let already_configured s l =
43 List.for_all (fun item -> List.exists (fun x -> x = item) l) s
45 let conffile = ref BuildTimeConf.matita_conf
47 let registry_defaults = [
49 "matita.debug", "false";
50 "matita.external_editor", "gvim -f -c 'go %p' %f";
51 "matita.preserve", "false";
52 "matita.profile", "true";
53 "matita.system", "false";
54 "matita.verbosity", "1";
55 (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
56 * intuitively verbose *)
59 let set_registry_values =
60 List.iter (fun key, value -> 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 wants [ Registry ] 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 ConfigurationFile::init_status
83 let initialize_db init_status =
84 wants [ ConfigurationFile; CmdLine ] init_status;
85 if not (already_configured [ Db ] init_status) then
87 if not (Helm_registry.get_bool "matita.system") then
88 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
89 LibraryDb.create_owner_environment ();
95 let initialize_makelib init_status =
96 wants [ConfigurationFile] init_status;
97 if not (already_configured [Makelib] init_status) then
99 MatitamakeLib.initialize ();
105 let initialize_environment init_status =
106 wants [ConfigurationFile] 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)
130 Usage: matitac [ OPTION ... ] FILE
132 BuildTimeConf.version;
134 sprintf "Grafite Grep v%s
135 Usage: gragrep [ -r ] PATH
137 BuildTimeConf.version;
140 Usage: matita [ OPTION ... ] [ FILE ... ]
142 BuildTimeConf.version;
146 Usage: cicbrowser [ URL | WHELP QUERY ]
148 BuildTimeConf.version;
150 sprintf "MatitaDep v%s
151 Usage: matitadep [ OPTION ... ] FILE ...
153 BuildTimeConf.version;
155 sprintf "MatitaClean v%s
156 Usage: matitaclean all
157 matitaclean [ (FILE | URI) ... ]
159 BuildTimeConf.version;
161 sprintf "MatitaMake v%s
162 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
164 Parameters: name (the name of the development, required)
165 Description: tells matitamake that a new development radicated
166 in the current working directory should be handled.
168 Parameters: name (the name of the development to destroy, optional)
169 If omitted the development that holds the current working
170 directory is used (if any).
171 Description: clean the develpoment.
174 Description: lists the known developments and their roots.
176 Parameters: name (the name of the development to destroy, required)
177 Description: deletes a development (only from matitamake metadat, no
178 .ma files will be deleted).
180 Parameters: name (the name of the development to build, required)
181 Description: completely builds the develpoment.
183 Parameters: name (the name of the development to publish, required)
184 Description: cleans the development in the user space, rebuilds it
185 in the system space ('ro' repositories, that for this operation
188 If target is omitted an 'all' will be used as the default.
189 With -build you can build a development wherever it is.
190 If you specify a target it implicitly refers to the development that
191 holds the current working directory (if any).
193 BuildTimeConf.version;
196 sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
199 let basename = Filename.basename Sys.argv.(0) in
201 try Filename.chop_extension basename with Invalid_argument _ -> basename
203 try Hashtbl.find usages usage_key with Not_found -> default_usage
205 let extra_cmdline_specs = ref []
206 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
208 let parse_cmdline init_status =
209 if not (already_configured [CmdLine] init_status) then begin
211 BuildTimeConf.stdlib_dir_installed ;
212 BuildTimeConf.stdlib_dir_devel ]
215 let add_l l = fun s -> l := s :: !l in
216 let reduce_verbosity () =
217 Helm_registry.set_int "matita.verbosity"
218 (Helm_registry.get_int "matita.verbosity" - 1) in
219 let increase_verbosity () =
220 Helm_registry.set_int "matita.verbosity"
221 (Helm_registry.get_int "matita.verbosity" + 1) in
224 "-I", Arg.String (add_l includes),
225 ("<path> Adds path to the list of searched paths for the "
226 ^ "include command");
227 "-conffile", Arg.Set_string conffile,
228 (Printf.sprintf ("<filename> Read configuration from filename"
230 BuildTimeConf.matita_conf);
232 Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
233 ("Force actions that would not be executed per default");
234 "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
235 ("Avoid using external database connection"
236 ^ "\n WARNING: disable many features");
238 Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
239 "Turns off profiling printings";
241 Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
242 "Turns off automatic baseuri cleaning";
243 "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
244 "-system", Arg.Unit (fun () ->
245 Helm_registry.set_bool "matita.system" true),
246 ("Act on the system library instead of the user one"
247 ^ "\n WARNING: not for the casual user");
248 "-v", Arg.Unit increase_verbosity, "Increase verbosity";
251 if BuildTimeConf.debug then
253 Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
254 ("Do not catch top-level exception "
255 ^ "(useful for backtrace inspection)");
259 std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
261 let set_list ~key l =
262 Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
264 Arg.parse arg_spec (add_l args) (usage ());
265 set_list ~key:"matita.includes" includes;
266 set_list ~key:"matita.args" args;
267 HExtlib.set_profiling_printings
268 (fun () -> Helm_registry.get_bool "matita.profile");
269 CmdLine :: init_status
274 print_endline (usage ());
277 let initialize_all () =
279 List.fold_left (fun s f -> f s) !status
280 [ fill_registry; parse_cmdline; load_configuration; initialize_makelib;
281 initialize_db; initialize_environment ]
282 (* initialize_notation
283 (initialize_environment
287 (parse_cmdline !status))))) *)
289 let load_configuration_file () =
290 status := load_configuration !status
292 let parse_cmdline () =
293 status := parse_cmdline !status
295 let fill_registry () =
296 status := fill_registry !status
299 Inversion_principle.init ()