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