- centralized parsing of cmdline options in matitaInit. All top level programs which need to parse cmdline will now invoke either MatitaInit.parse_cmdline or MatitaInit.initialize_all and then refer to the relevant keys in the registry
- changed dependencies on hMySql since now it is in a separate library
OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
+
+MATITA_FLAGS =
+NODB=false
+ifeq ($(NODB),true)
+ MATITA_FLAGS += -nodb
+endif
+
+
# objects for matita (GTK GUI)
NULL =
CMOS = \
@echo
coq.moo: coq.ma matitac
- ./matitac coq.ma
+ ./matitac $(MATITA_FLAGS) coq.ma
coq.moo.opt: coq.ma matitac.opt
- ./matitac.opt coq.ma
+ ./matitac.opt $(MATITA_FLAGS) coq.ma
ifeq ($(HAVE_OCAMLOPT),yes)
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
pcre \
mysql \
helm-registry \
+helm-extlib \
+helm-hmysql \
helm-cic_disambiguation \
helm-paramodulation \
"
addDebugItem "getter: getalluris" (fun _ ->
List.iter prerr_endline (Http_getter.getalluris ()));
addDebugItem "dump script status" script#dump;
+ addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
+ Helm_registry.save_to "./foo.conf.xml");
addDebugItem "dump metasenv"
(fun _ ->
if script#onGoingProof () then
(** {2 Command line parsing} *)
-let debug = ref false
-let args = ref []
-let add_arg arg = args := arg :: !args
-
-let arg_spec =
- let std_arg_spec = [] in
- let debug_arg_spec =
- if BuildTimeConf.debug then
- [ "-debug", Arg.Set debug,
- "Do not catch top-level exception (useful for backtrace inspection)"; ]
- else []
- in
- std_arg_spec @ debug_arg_spec
-
-let usage () =
- let heading = sprintf "Matita v%s\nUsage: " BuildTimeConf.version in
- if Helm_registry.get "matita.mode" = "cicbrowser" then
- heading ^ "cicbrowser [ URL | Whelp query ]\nOptions:"
- else
- heading ^ "matita [ FILE ]"
-
let set_matita_mode () =
let matita_mode =
if Filename.basename Sys.argv.(0) = "cicbrowser"
let _ =
set_matita_mode ();
- Arg.parse arg_spec add_arg (usage ());
- Helm_registry.set_bool "matita.catch_top_level_exn" (not !debug);
at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
Sys.catch_break true;
+ let args = Helm_registry.get_list Helm_registry.string "matita.args" in
if Helm_registry.get "matita.mode" = "cicbrowser" then (* cicbrowser *)
let browser = MatitaMathView.cicBrowser () in
- let uri = match !args with [] -> "cic:/" | _ -> String.concat " " !args in
+ let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in
browser#loadInput uri
else begin (* matita *)
- (try gui#loadScript (List.hd !args) with Failure _ -> ());
+ (try gui#loadScript (List.hd args) with Failure _ -> ());
gui#main#mainWin#show ();
end;
try
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
(fun exn ->
- if Helm_registry.get_bool "matita.catch_top_level_exn" then
+ if not (Helm_registry.get_bool "matita.debug") then
MatitaLog.error (MatitaExcPp.to_string exn)
else raise exn);
(* script *)
* http://helm.cs.unibo.it/
*)
+open Printf
+
type thingsToInitilaize =
ConfigurationFile | Db | Environment | Getter | Notation |
- Paramodulation | Makelib
+ Paramodulation | Makelib | CmdLine
exception FailedToInitialize of thingsToInitilaize
init_status
let initialize_db init_status =
- wants [ConfigurationFile] init_status;
- if not (already_configured [Db] init_status) then
+ wants [ ConfigurationFile; CmdLine ] init_status;
+ if not (already_configured [ Db ] init_status) then
begin
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
MatitaDb.create_owner_environment ();
init_status
let status = ref []
-
+
+let usages = Hashtbl.create 11
+let _ =
+ List.iter
+ (fun (name, s) -> Hashtbl.replace usages name s)
+ [ "matitac",
+ sprintf "MatitaC v%s
+Usage: matitac [ OPTION ... ] FILE
+Options:"
+ BuildTimeConf.version;
+ "matita",
+ sprintf "Matita v%s
+Usage: matita [ OPTION ... ] [ FILE ... ]
+Options:"
+ BuildTimeConf.version;
+ "cicbrowser",
+ sprintf
+ "CIC Browser v%s
+Usage: cicbrowser [ URL | WHELP QUERY ]
+Options:"
+ BuildTimeConf.version;
+ "matitadep",
+ sprintf "MatitaDep v%s
+Usage: matitadep [ OPTION ... ] FILE ...
+Options:"
+ BuildTimeConf.version;
+ "matitaclean",
+ sprintf "MatitaClean v%s
+Usage: matitaclean all
+ matitaclean [ (FILE | URI) ... ]
+Options:"
+ BuildTimeConf.version;
+ ]
+let default_usage =
+ sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
+
+let usage () =
+ let basename = Filename.basename Sys.argv.(0) in
+ let usage_key =
+ try Filename.chop_extension basename with Invalid_argument _ -> basename
+ in
+ try Hashtbl.find usages usage_key with Not_found -> default_usage
+
+let registry_defaults =
+ [ "matita.debug", "false";
+ "matita.quiet", "false";
+ "matita.preserve", "false";
+ "db.nodb", "false";
+ ]
+
+let set_registry_values =
+ List.iter (fun key, value -> Helm_registry.set ~key ~value)
+
+let parse_cmdline init_status =
+ if not (already_configured [CmdLine] init_status) then begin
+ let includes = ref [] in
+ let args = ref [] in
+ let add_l l = fun s -> l := s :: !l in
+ let arg_spec =
+ let std_arg_spec = [
+ "-I", Arg.String (add_l includes),
+ ("<path> Adds path to the list of searched paths for the "
+ ^ "include command");
+ "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true),
+ "Turn off verbose compilation";
+ "-preserve",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
+ "Turns off automatic baseuri cleaning";
+ "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
+ ("Avoid using external database connection "
+ ^ "(WARNING: disable many features)");
+ ] in
+ let debug_arg_spec =
+ if BuildTimeConf.debug then
+ [ "-debug",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
+ ("Do not catch top-level exception "
+ ^ "(useful for backtrace inspection)");
+ ]
+ else []
+ in
+ std_arg_spec @ debug_arg_spec
+ in
+ let set_list ~key l =
+ Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)
+ in
+ set_registry_values registry_defaults;
+ Arg.parse arg_spec (add_l args) (usage ());
+ set_list ~key:"matita.includes" includes;
+ set_list ~key:"matita.args" args;
+Helm_registry.save_to "./foo.conf.xml";
+ CmdLine :: init_status
+ end else
+ init_status
+
+let die_usage () =
+ print_endline (usage ());
+ exit 1
+
let initialize_all () =
status :=
initialize_notation
(initialize_db
(initialize_paramodulation
(initialize_makelib
- (load_configuration !status)))))
+ (load_configuration
+ (parse_cmdline !status))))))
-let load_config_only () =
+let load_configuration_file () =
status := load_configuration !status
let initialize_notation () =
status := initialize_notation (load_configuration !status)
-
+
+let parse_cmdline () =
+ status := parse_cmdline !status
+
* http://helm.cs.unibo.it/
*)
-val load_config_only: unit -> unit
+ (** {2 global initialization} *)
val initialize_all: unit -> unit
+
+ (** {2 per-components initialization} *)
+val parse_cmdline: unit -> unit (** parse cmdline setting registry keys *)
+val load_configuration_file: unit -> unit
val initialize_notation: unit -> unit
+ (** {2 Utilities} *)
+
+ (** die nicely: exit with return code 1 printing usage error message *)
+val die_usage: unit -> 'a
+
try
f ()
with exn ->
- if Helm_registry.get_bool "matita.catch_top_level_exn" then
+ if not (Helm_registry.get_bool "matita.debug") then
fail (MatitaExcPp.to_string exn)
else raise exn
in
(** {2 Initialization} *)
- (** If set to true matitac wont catch top level exception, so that backtrace
- * could be inspected setting OCAMLRUNPARAM=b. This flag is enabled passing
- * -debug *)
-let debug = ref false
-let paths_to_search_in = ref [];;
-let quiet_compilation = ref false;;
-let dont_delete_baseuri = ref false;;
-
-let add_l l = fun s -> l := s :: !l ;;
-
-let arg_spec =
- let std_arg_spec = [
- "-I", Arg.String (add_l paths_to_search_in),
- "<path> Adds path to the list of searched paths for the include command";
- "-q", Arg.Set quiet_compilation, "Turn off verbose compilation";
- "-preserve", Arg.Set dont_delete_baseuri,
- "Turns off automatic baseuri cleaning";
- ] in
- let debug_arg_spec =
- if BuildTimeConf.debug then
- [ "-debug", Arg.Set debug,
- "Do not catch top-level exception (useful for backtrace inspection)"; ]
- else []
- in
- std_arg_spec @ debug_arg_spec
-
-let usage =
- sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:"
- BuildTimeConf.version
-
let status = ref None
let run_script is eval_function =
in
let slash_n_RE = Pcre.regexp "\\n" in
let cb =
- if !quiet_compilation then
- fun _ _ -> ()
+ if Helm_registry.get_bool "matita.quiet" then
+ (fun _ _ -> ())
else
- fun status stm ->
+ (fun status stm ->
(* dump_status status; *)
let stm = GrafiteAstPp.pp_statement stm in
let stm = Pcre.replace ~rex:slash_n_RE stm in
else
stm
in
- MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
+ MatitaLog.debug ("Executing: ``" ^ stm ^ "''"))
in
try
eval_function status is cb
raise exn
let fname () =
- let acc = ref [] in
- let add_script fname = acc := fname :: !acc in
- Arg.parse arg_spec add_script usage;
- match !acc with
+ match Helm_registry.get_list Helm_registry.string "matita.args" with
| [x] -> x
- | _ -> print_endline usage; exit 1
+ | _ -> MatitaInit.die_usage ()
let pp_ocaml_mode () =
MatitaLog.message "";
let str = Ulexing.from_utf8_channel stdin in
try
run_script str
- (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in)
+ (MatitaEngine.eval_from_stream_greedy
+ ~include_paths:(Helm_registry.get_list Helm_registry.string
+ "matita.includes"))
with
| MatitaEngine.Drop -> pp_ocaml_mode ()
| Sys.Break -> MatitaLog.error "user break!"; interactive_loop ()
let main ~mode =
MatitaInit.initialize_all ();
+ (* must be called after init since args are set by cmdline parsing *)
+ let fname = fname () in
status := Some (ref (Lazy.force MatitaEngine.initial_status));
Sys.catch_break true;
let origcb = MatitaLog.get_log_callback () in
| `Debug | `Message -> ()
| `Warning | `Error -> origcb tag s
in
- let fname = fname () in
- if !quiet_compilation then
+ if Helm_registry.get_bool "matita.quiet" then
MatitaLog.set_log_callback newcb;
try
let time = Unix.time () in
- if !quiet_compilation then
+ if Helm_registry.get_bool "matita.quiet" then
origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
else
MatitaLog.message (sprintf "execution of %s started:" fname);
in
run_script is
(MatitaEngine.eval_from_stream
- ~include_paths:!paths_to_search_in
- ~clean_baseuri:(not !dont_delete_baseuri));
+ ~include_paths:(Helm_registry.get_list Helm_registry.string
+ "matita.includes")
+ ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
let elapsed = Unix.time () -. time in
let tm = Unix.gmtime elapsed in
let sec =
else
pp_ocaml_mode ()
| exn ->
- if !debug then raise exn;
+ if Helm_registry.get_bool "matita.debug" then raise exn;
if mode = `COMPILER then
clean_exit (Some 3)
else
* http://helm.cs.unibo.it/
*)
-module UM = UriManager;;
-module TA = GrafiteAst;;
+open Printf
+
+module UM = UriManager
+module TA = GrafiteAst
let _ = MatitaInit.initialize_all ()
let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
-let usage () =
- prerr_endline "
-usage:
-\tmatitaclean all
-\t\tcleans the whole environment
-\tmatitaclean files...
-\t\tcleans the output of the compilation of files...
-";
- exit 1
-
let _ =
- if Array.length Sys.argv < 2 then usage ();
- if Sys.argv.(1) = "all" then
- begin
+ let uris_to_remove = ref [] in
+ let files_to_remove = ref [] in
+ (match Helm_registry.get_list Helm_registry.string "matita.args" with
+ | [ "all" ] ->
MatitaDb.clean_owner_environment ();
let xmldir = Helm_registry.get "matita.basedir" ^ "/xml" in
ignore
(Sys.command ("find " ^ xmldir ^
" -type d -exec rmdir -p {} \\; 2> /dev/null"));
exit 0
- end
- let uris_to_remove =ref [] in
- let files_to_remove =ref [] in
- (try
- for i = 1 to Array.length Sys.argv - 1 do
- let suri = Sys.argv.(i) in
- let uri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with
- UM.IllFormedUri _ ->
- files_to_remove := suri :: !files_to_remove;
- let u = MatitaMisc.baseuri_of_file suri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- begin
- MatitaLog.error ("File " ^ suri ^ " defines a bad baseuri: "^u);
- exit 1
- end
- else
- u
- in
- uris_to_remove := uri :: !uris_to_remove
- done
- with
- Invalid_argument _ -> usage ());
+ | [] -> MatitaInit.die_usage ()
+ | files ->
+ List.iter
+ (fun suri ->
+ let uri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with UM.IllFormedUri _ ->
+ files_to_remove := suri :: !files_to_remove;
+ let u = MatitaMisc.baseuri_of_file suri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
+ MatitaLog.error (sprintf "File %s defines a bad baseuri: %s"
+ suri u);
+ exit 1
+ end else
+ u
+ in
+ uris_to_remove := uri :: !uris_to_remove)
+ files);
main !uris_to_remove;
let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in
List.iter MatitaMisc.safe_remove moos
* http://helm.cs.unibo.it/
*)
+open Printf
+
let debug = false
let debug_prerr = if debug then prerr_endline else ignore
let buri = buri ^ "/" in
let buri = HMysql.escape buri in
let obj_tbl = MetadataTypes.obj_tbl () in
- Printf.sprintf
- "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+ sprintf
+ "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'"
+ obj_tbl buri
in
try
let rc = HMysql.exec (MatitaDb.instance ()) query in
with
exn -> raise exn (* no errors should be accepted *)
end
-
let safe_buri_of_suri suri =
try
MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
MetadataTypes.count_tbl()]
end
+
* http://helm.cs.unibo.it/
*)
-let paths_to_search_in = ref [];;
-
-let add_l l = fun s -> l := s :: !l ;;
-
-let arg_spec = [
- "-I", Arg.String (add_l paths_to_search_in),
- "<path> Adds path to the list of searched paths for the include command";
-]
-let usage =
- Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:"
- BuildTimeConf.version
-
module GA = GrafiteAst
module U = UriManager
close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path
with Sys_error _ -> aux tl
in
- let paths = !paths_to_search_in in
+ let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in
try
aux paths
with Sys_error _ as exc ->
;;
let main () =
- MatitaInit.load_config_only ();
- let files = ref [] in
- Arg.parse arg_spec (add_l files) usage;
+ MatitaInit.load_configuration_file ();
+ MatitaInit.parse_cmdline ();
List.iter
(fun file ->
let ic = open_in file in
MatitaLog.warn
("Unable to find " ^ path ^ " that is included in " ^ file))
dependencies)
- !files;
+ (Helm_registry.get_list Helm_registry.string "matita.args");
Hashtbl.iter
(fun file alias ->
let dep = resolve alias (Hashtbl.find baseuri_of file) in
let moo = MatitaMisc.obj_file_of_script file in
Printf.printf "%s: %s\n" moo (String.concat " " deps);
Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo)
- !files
+ (Helm_registry.get_list Helm_registry.string "matita.args")
;;
let _ =
module MK = MatitamakeLib ;;
let _ =
- MatitaInit.load_config_only ();
+ MatitaInit.load_configuration_file ();
MK.initialize ()
;;
projects / helm.git / commitdiff