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