]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaInit.ml
...
[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 | 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.debug_menu",           "false";
48   "matita.external_editor",      "gvim -f -c 'go %p' %f";
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";
55   "matita.moo",                  "true";
56   "matita.extract",              "false";
57 ]
58
59 let set_registry_values =
60   List.iter 
61     (fun key, value -> 
62        if not (Helm_registry.has key) then Helm_registry.set ~key ~value)
63
64 let fill_registry init_status =
65   if not (already_configured [ Registry ] init_status) then begin
66     set_registry_values registry_defaults;
67     Registry :: init_status
68   end else
69     init_status
70
71 let load_configuration init_status =
72   if not (already_configured [ConfigurationFile] init_status) then
73     begin
74       Helm_registry.load_from !conffile;
75       if not (Helm_registry.has "user.name") then begin
76         let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
77         Helm_registry.set "user.name" login
78       end;
79       let home = Helm_registry.get_string "matita.basedir" in
80       let user_conf_file = home ^ "/matita.conf.xml" in
81       if HExtlib.is_regular user_conf_file then
82         begin
83           HLog.message ("Loading additional conf file from " ^ user_conf_file);
84           try
85             Helm_registry.load_from user_conf_file
86           with exn -> 
87             HLog.error
88               ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
89         end;
90       ConfigurationFile::init_status 
91     end
92   else
93     init_status
94
95 let initialize_db init_status = 
96   wants [ ConfigurationFile; CmdLine ] init_status;
97   if not (already_configured [ Db ] init_status) then
98     begin
99       if not (Helm_registry.get_bool "matita.system") then
100         MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
101       LibraryDb.create_owner_environment ();
102       Db::init_status
103     end
104   else
105     init_status
106
107 let initialize_environment init_status = 
108   wants [CmdLine] init_status;
109   if not (already_configured [Getter;Environment] init_status) then
110     begin
111       Http_getter.init ();
112       if Helm_registry.get_bool "matita.system" then
113         Http_getter_storage.activate_system_mode ();
114       CicEnvironment.set_trust (* environment trust *)
115         (let trust =
116           Helm_registry.get_opt_default Helm_registry.get_bool
117             ~default:true "matita.environment_trust" in
118          fun _ -> trust);
119       Getter::Environment::init_status
120     end
121   else
122     init_status 
123   
124 let status = ref []
125
126 let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
127 let _ =
128   List.iter
129     (fun (name, s) -> Hashtbl.replace usages name s)
130     [ "matitac", 
131         Printf.sprintf "Matita batch compiler v%s
132 Usage: matitac [ OPTION ... ] FILE
133 Options:"
134           BuildTimeConf.version;
135         "matitaprover",
136         Printf.sprintf "Matita (TPTP) prover v%s
137 Usage: matitaprover [ -tptppath ] FILE.p
138 Options:"
139           BuildTimeConf.version;
140       "matita",
141         Printf.sprintf "Matita interactive theorem prover v%s
142 Usage: matita [ OPTION ... ] [ FILE ]
143 Options:"
144           BuildTimeConf.version;
145       "matitadep",
146         Printf.sprintf "Matita depency file generator v%s
147 Usage: matitadep [ OPTION ... ] 
148 Options:"
149           BuildTimeConf.version;
150       "matitaclean",
151         Printf.sprintf "MatitaClean v%s
152 Usage: matitaclean all
153        matitaclean ( FILE | URI )
154 Options:"
155           BuildTimeConf.version;
156     ]
157 let default_usage =
158   Printf.sprintf 
159     "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
160
161 let usage () =
162   let basename = Filename.basename Sys.argv.(0) in
163   let usage_key =
164     try Filename.chop_extension basename with Invalid_argument  _ -> basename
165   in
166   try Hashtbl.find usages usage_key with Not_found -> default_usage
167 ;;
168
169 let extra_cmdline_specs = ref []
170 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
171
172 let parse_cmdline init_status =
173   if not (already_configured [CmdLine] init_status) then begin
174     wants [Registry] init_status;
175     let includes = ref [] in
176     let default_includes = [ 
177       BuildTimeConf.stdlib_dir_devel;
178       BuildTimeConf.stdlib_dir_installed ; ] 
179     in
180     let absolutize s =
181       if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
182     in
183     let args = ref [] in
184     let add_l l = fun s -> l := s :: !l in
185     let print_version () =
186             Printf.printf "%s\n" BuildTimeConf.version;exit 0 in
187     let no_innertypes () =
188       Helm_registry.set_bool "matita.noinnertypes" true in
189     let set_baseuri s =
190       match Str.split (Str.regexp "::") s with
191       | [path; uri] -> Helm_registry.set "matita.baseuri"
192           (HExtlib.normalize_path (absolutize path)^" "^uri)
193       | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
194     in
195     let arg_spec =
196       let std_arg_spec = [
197         "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
198         "-I", Arg.String (add_l includes),
199           ("<path> Adds path to the list of searched paths for the "
200            ^ "include command");
201         "-conffile", Arg.Set_string conffile,
202           (Printf.sprintf ("<filename> Read configuration from filename"
203              ^^ "\n    Default: %s")
204             BuildTimeConf.matita_conf);
205         "-force",
206             Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
207             ("Force actions that would not be executed per default");
208         "-noprofile", 
209           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
210           "Turns off profiling printings";
211         "-noinnertypes", Arg.Unit no_innertypes, 
212           "Turns off inner types generation while publishing";
213         "-profile-only",
214           Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex),
215           "Activates only profiler with label matching the provided regex";
216         "-system", Arg.Unit (fun () ->
217               Helm_registry.set_bool "matita.system" true),
218             ("Act on the system library instead of the user one"
219              ^ "\n    WARNING: not for the casual user");
220         "-v", 
221           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
222           "Verbose mode";
223         "--version", Arg.Unit print_version, "Prints version";
224       ] in
225       let debug_arg_spec =
226         if BuildTimeConf.debug then
227           [ "-debug",
228             Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
229               ("Do not catch top-level exception "
230               ^ "(useful for backtrace inspection)");
231             "-onepass",
232             Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
233             "Enable only one disambiguation pass";    
234           ]
235         else []
236       in
237       std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
238     in
239     let set_list ~key l =
240       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
241     in
242     Arg.parse arg_spec (add_l args) (usage ());
243     let includes = 
244       List.map (fun x -> HExtlib.normalize_path (absolutize x)) 
245        ((List.rev !includes) @ default_includes) 
246     in
247     set_list ~key:"matita.includes" includes;
248     let args = List.rev (List.filter (fun x -> x <> "") !args) in
249     set_list ~key:"matita.args" args;
250     HExtlib.set_profiling_printings 
251       (fun s -> 
252         Helm_registry.get_bool "matita.profile" && 
253         Pcre.pmatch 
254           ~pat:(Helm_registry.get_opt_default 
255                   Helm_registry.string ~default:".*" "matita.profile_only") 
256           s);
257     CmdLine :: init_status
258   end else
259     init_status
260
261 let die_usage () =
262   print_endline (usage ());
263   exit 1
264
265 let conf_components = 
266   [ load_configuration; fill_registry; parse_cmdline]
267
268 let other_components =
269   [ initialize_db; initialize_environment ]
270
271 let initialize_all () =
272   status := 
273     List.fold_left (fun s f -> f s) !status
274     (conf_components @ other_components)
275
276 let parse_cmdline_and_configuration_file () =
277   status := List.fold_left (fun s f -> f s) !status conf_components
278
279 let initialize_environment () =
280   status := initialize_environment !status
281
282 let _ =
283   Inversion_principle.init ()