]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaInit.ml
moved to pkg-ocaml-maint
[helm.git] / helm / software / matita / matitaInit.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 type thingsToInitilaize = 
29   ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
30   
31 exception FailedToInitialize of thingsToInitilaize
32
33 let wants s l = 
34   List.iter (
35     fun item -> 
36       if not (List.exists (fun x -> x = item) l) then
37         raise (FailedToInitialize item)) 
38   s
39
40 let already_configured s l =
41   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
42   
43 let conffile = ref BuildTimeConf.matita_conf
44
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     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
56      * intuitively verbose *)
57 ]
58
59 let set_registry_values =
60   List.iter (fun key, value -> Helm_registry.set ~key ~value)
61
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
66   end else
67     init_status
68
69 let load_configuration init_status =
70   if not (already_configured [ConfigurationFile] init_status) then
71     begin
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
76       end;
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
80         begin
81           HLog.message ("Loading additional conf file from " ^ user_conf_file);
82           try
83             Helm_registry.load_from user_conf_file
84           with exn -> 
85             HLog.error
86               ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
87         end;
88       ConfigurationFile::init_status 
89     end
90   else
91     init_status
92
93 let initialize_db init_status = 
94   wants [ ConfigurationFile; CmdLine ] init_status;
95   if not (already_configured [ Db ] init_status) then
96     begin
97       if not (Helm_registry.get_bool "matita.system") then
98         MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
99       LibraryDb.create_owner_environment ();
100       Db::init_status
101     end
102   else
103     init_status
104
105 let initialize_makelib init_status = 
106   wants [ConfigurationFile] init_status;
107   if not (already_configured [Makelib] init_status) then
108     begin
109       MatitamakeLib.initialize (); 
110       Makelib::init_status
111     end
112   else
113     init_status
114
115 let initialize_environment init_status = 
116   wants [CmdLine] init_status;
117   if not (already_configured [Getter;Environment] init_status) then
118     begin
119       Http_getter.init ();
120       if Helm_registry.get_bool "matita.system" then
121         Http_getter_storage.activate_system_mode ();
122       CicEnvironment.set_trust (* environment trust *)
123         (let trust =
124           Helm_registry.get_opt_default Helm_registry.get_bool
125             ~default:true "matita.environment_trust" in
126          fun _ -> trust);
127       Getter::Environment::init_status
128     end
129   else
130     init_status 
131   
132 let status = ref []
133
134 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
135 let _ =
136   List.iter
137     (fun (name, s) -> Hashtbl.replace usages name s)
138     [ "matitac", 
139         Printf.sprintf "MatitaC v%s
140 Usage: matitac [ OPTION ... ] FILE
141 Options:"
142           BuildTimeConf.version;
143       "gragrep",
144         Printf.sprintf "Grafite Grep v%s
145 Usage: gragrep [ -r ] PATH
146 Options:"
147           BuildTimeConf.version;
148       "matitaprover",
149         Printf.sprintf "Matita's prover v%s
150 Usage: matitaprover [ -tptppath ] FILE.p
151 Options:"
152           BuildTimeConf.version;
153       "matita",
154         Printf.sprintf "Matita v%s
155 Usage: matita [ OPTION ... ] [ FILE ... ]
156 Options:"
157           BuildTimeConf.version;
158       "cicbrowser",
159         Printf.sprintf
160           "CIC Browser v%s
161 Usage: cicbrowser [ URL | WHELP QUERY ]
162 Options:"
163           BuildTimeConf.version;
164       "matitadep",
165         Printf.sprintf "MatitaDep v%s
166 Usage: matitadep [ OPTION ... ] FILE ...
167 Options:"
168           BuildTimeConf.version;
169       "matitaclean",
170         Printf.sprintf "MatitaClean v%s
171 Usage: matitaclean all
172        matitaclean [ (FILE | URI) ... ]
173 Options:"
174           BuildTimeConf.version;
175       "matitamake",
176         Printf.sprintf "MatitaMake v%s
177 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
178   init
179     Parameters: name (the name of the development, required)
180                 root (the directory in which the delopment is rooted, 
181                       optional, default is current working directory)
182     Description: tells matitamake that a new development radicated 
183       in the current working directory should be handled.
184   clean
185     Parameters: name (the name of the development to destroy, optional)
186       If omitted the development that holds the current working 
187       directory is used (if any).
188     Description: clean the develpoment.
189   list
190     Parameters: 
191     Description: lists the known developments and their roots.
192   destroy
193     Parameters: name (the name of the development to destroy, required)
194     Description: deletes a development (only from matitamake metadat, no
195       .ma files will be deleted).
196   build
197     Parameters: name (the name of the development to build, required)
198     Description: completely builds the develpoment.
199   publish
200     Parameters: name (the name of the development to publish, required)
201     Description: cleans the development in the user space, rebuilds it
202       in the system space ('ro' repositories, that for this operation 
203       becames writable). 
204 Notes:
205   If target is omitted an 'all' will be used as the default.
206   With -build you can build a development wherever it is.
207   If you specify a target it implicitly refers to the development that
208   holds the current working directory (if any).
209 Options:"
210           BuildTimeConf.version;
211     ]
212 let default_usage =
213   Printf.sprintf 
214     "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
215
216 let usage () =
217   let basename = Filename.basename Sys.argv.(0) in
218   let usage_key =
219     try Filename.chop_extension basename with Invalid_argument  _ -> basename
220   in
221   try Hashtbl.find usages usage_key with Not_found -> default_usage
222
223 let extra_cmdline_specs = ref []
224 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
225
226 let parse_cmdline init_status =
227   if not (already_configured [CmdLine] init_status) then begin
228     wants [Registry] init_status;
229     let includes = ref [] in
230     let default_includes = [ 
231       ".";
232       BuildTimeConf.stdlib_dir_devel;
233       BuildTimeConf.stdlib_dir_installed ; ] 
234     in
235     let absolutize s =
236       if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s
237     in
238     let args = ref [] in
239     let add_l l = fun s -> l := s :: !l in
240     let reduce_verbosity () =
241       Helm_registry.set_int "matita.verbosity"
242         (Helm_registry.get_int "matita.verbosity" - 1) in
243     let print_version () =
244             Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
245     let increase_verbosity () =
246       Helm_registry.set_int "matita.verbosity"
247         (Helm_registry.get_int "matita.verbosity" + 1) in
248     let no_innertypes () =
249       Helm_registry.set_bool "matita.noinnertypes" true in
250     let arg_spec =
251       let std_arg_spec = [
252         "-I", Arg.String (add_l includes),
253           ("<path> Adds path to the list of searched paths for the "
254            ^ "include command");
255         "-conffile", Arg.Set_string conffile,
256           (Printf.sprintf ("<filename> Read configuration from filename"
257              ^^ "\n    Default: %s")
258             BuildTimeConf.matita_conf);
259         "-force",
260             Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
261             ("Force actions that would not be executed per default");
262         "-noprofile", 
263           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
264           "Turns off profiling printings";
265         "-noinnertypes", Arg.Unit no_innertypes, 
266           "Turns off inner types generation while publishing";
267         "-profile-only",
268           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
269           "Activates only profiler with label matching the provided regex";
270         "-bench", 
271           Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
272           "Turns on parsable output on stdout, that is timings for matitac...";
273         "-preserve",
274           Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
275           "Turns off automatic baseuri cleaning";
276         "-q", Arg.Unit reduce_verbosity, "Reduce verbosity";
277         "-system", Arg.Unit (fun () ->
278               Helm_registry.set_bool "matita.system" true),
279             ("Act on the system library instead of the user one"
280              ^ "\n    WARNING: not for the casual user");
281         "-v", Arg.Unit increase_verbosity, "Increase verbosity";
282         "--version", Arg.Unit print_version, "Prints version";
283       ] in
284       let debug_arg_spec =
285         if BuildTimeConf.debug then
286           [ "-debug",
287             Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
288               ("Do not catch top-level exception "
289               ^ "(useful for backtrace inspection)");
290             "-onepass",
291             Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
292             "Enable only one disambiguation pass";    
293           ]
294         else []
295       in
296       std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
297     in
298     let set_list ~key l =
299       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
300     in
301     Arg.parse arg_spec (add_l args) (usage ());
302     let includes = 
303       List.map absolutize ((List.rev !includes) @ default_includes) in
304     set_list ~key:"matita.includes" includes;
305     let args = List.rev (List.filter (fun x -> x <> "") !args) in
306     set_list ~key:"matita.args" args;
307     HExtlib.set_profiling_printings 
308       (fun s -> 
309         Helm_registry.get_bool "matita.profile" && 
310         Pcre.pmatch 
311           ~pat:(Helm_registry.get_opt_default 
312                   Helm_registry.string ~default:".*" "matita.profile_only") 
313           s);
314     CmdLine :: init_status
315   end else
316     init_status
317
318 let die_usage () =
319   print_endline (usage ());
320   exit 1
321
322 let conf_components = 
323   [ load_configuration; fill_registry; parse_cmdline]
324
325 let other_components =
326   [ initialize_makelib; initialize_db; initialize_environment ]
327
328 let initialize_all () =
329   status := 
330     List.fold_left (fun s f -> f s) !status
331     (conf_components @ other_components)
332 (*     initialize_notation 
333       (initialize_environment 
334         (initialize_db 
335           (initialize_makelib
336             (load_configuration
337               (parse_cmdline !status))))) *)
338
339 let parse_cmdline_and_configuration_file () =
340   status := List.fold_left (fun s f -> f s) !status conf_components
341
342 let initialize_environment () =
343   status := initialize_environment !status
344
345 let _ =
346   Inversion_principle.init ()