X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=d8d498a32018c047cd19d93cb15e344cae3686d6;hb=831f51f3a0a972c741705dcc3244e79fe6c1b634;hp=8ae9b00a37fb0e325058428be5ade6bb957abc66;hpb=f35d1a64255215087e0b15938eaa085152f1d787;p=helm.git diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 8ae9b00a3..d8d498a32 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -26,7 +26,7 @@ (* $Id$ *) type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry + ConfigurationFile | Db | Environment | Getter | CmdLine | Registry exception FailedToInitialize of thingsToInitilaize @@ -44,20 +44,22 @@ let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ "matita.debug", "false"; + "matita.debug_menu", "false"; "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; "matita.profile", "true"; "matita.system", "false"; - "matita.verbosity", "1"; - "matita.bench", "false"; + "matita.verbose", "false"; "matita.paste_unicode_as_tex", "false"; "matita.noinnertypes", "false"; - (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is - * intuitively verbose *) + "matita.do_heavy_checks", "true"; + "matita.moo", "true"; + "matita.extract", "false"; ] let set_registry_values = - List.iter (fun key, value -> Helm_registry.set ~key ~value) + List.iter + (fun key, value -> + if not (Helm_registry.has key) then Helm_registry.set ~key ~value) let fill_registry init_status = if not (already_configured [ Registry ] init_status) then begin @@ -102,16 +104,6 @@ let initialize_db init_status = else init_status -let initialize_makelib init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Makelib] init_status) then - begin - MatitamakeLib.initialize (); - Makelib::init_status - end - else - init_status - let initialize_environment init_status = wants [CmdLine] init_status; if not (already_configured [Getter;Environment] init_status) then @@ -136,76 +128,29 @@ let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) [ "matitac", - Printf.sprintf "MatitaC v%s + Printf.sprintf "Matita batch compiler v%s Usage: matitac [ OPTION ... ] FILE Options:" BuildTimeConf.version; - "gragrep", - Printf.sprintf "Grafite Grep v%s -Usage: gragrep [ -r ] PATH -Options:" - BuildTimeConf.version; - "matitaprover", - Printf.sprintf "Matita's prover v%s + "matitaprover", + Printf.sprintf "Matita (TPTP) prover v%s Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", - Printf.sprintf "Matita v%s -Usage: matita [ OPTION ... ] [ FILE ... ] -Options:" - BuildTimeConf.version; - "cicbrowser", - Printf.sprintf - "CIC Browser v%s -Usage: cicbrowser [ URL | WHELP QUERY ] + Printf.sprintf "Matita interactive theorem prover v%s +Usage: matita [ OPTION ... ] [ FILE ] Options:" BuildTimeConf.version; "matitadep", - Printf.sprintf "MatitaDep v%s -Usage: matitadep [ OPTION ... ] FILE ... + Printf.sprintf "Matita depency file generator v%s +Usage: matitadep [ OPTION ... ] Options:" BuildTimeConf.version; "matitaclean", Printf.sprintf "MatitaClean v%s Usage: matitaclean all - matitaclean [ (FILE | URI) ... ] -Options:" - BuildTimeConf.version; - "matitamake", - Printf.sprintf "MatitaMake v%s -Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) - init - Parameters: name (the name of the development, required) - root (the directory in which the delopment is rooted, - optional, default is current working directory) - Description: tells matitamake that a new development radicated - in the current working directory should be handled. - clean - Parameters: name (the name of the development to destroy, optional) - If omitted the development that holds the current working - directory is used (if any). - Description: clean the develpoment. - list - Parameters: - Description: lists the known developments and their roots. - destroy - Parameters: name (the name of the development to destroy, required) - Description: deletes a development (only from matitamake metadat, no - .ma files will be deleted). - build - Parameters: name (the name of the development to build, required) - Description: completely builds the develpoment. - publish - Parameters: name (the name of the development to publish, required) - Description: cleans the development in the user space, rebuilds it - in the system space ('ro' repositories, that for this operation - becames writable). -Notes: - If target is omitted an 'all' will be used as the default. - With -build you can build a development wherever it is. - If you specify a target it implicitly refers to the development that - holds the current working directory (if any). + matitaclean ( FILE | URI ) Options:" BuildTimeConf.version; ] @@ -219,6 +164,65 @@ let usage () = try Filename.chop_extension basename with Invalid_argument _ -> basename in try Hashtbl.find usages usage_key with Not_found -> default_usage +;; + +let dump f = + let module G = GrafiteAst in + let module L = LexiconAst in + let module H = HExtlib in + Helm_registry.set_bool "matita.moo" false; + let floc = H.dummy_floc in + let nl_ast = G.Comment (floc, G.Note (floc, "")) in + let och = open_out f in + let atexit () = close_out och in + let out_comment och s = + let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in + Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" + in + let out_line_comment och s = + let l = 70 - String.length s in + let s = Printf.sprintf " %s %s" s (String.make l '*') in + out_comment och s + in + let out_preamble och (path, lines) = + let ich = open_in path in + let rec print i = + if i > 0 then + let s = input_line ich in + begin Printf.fprintf och "%s\n" s; print (pred i) end + in + print lines; + out_line_comment och "This file was automatically generated: do not edit" + in + let pp_ast_statement st = + GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~lazy_term_pp:CicNotationPp.pp_term + ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st + in + let nl () = output_string och (pp_ast_statement nl_ast) in + let rt_base_dir = Filename.dirname Sys.argv.(0) in + let path = Filename.concat rt_base_dir "matita.ma.templ" in + let lines = 14 in + out_preamble och (path, lines); + let grafite_parser_cb fname = + let ast = G.Executable + (floc, G.Command (floc, G.Include (floc, fname))) in + output_string och (pp_ast_statement ast); nl (); nl () + in + let matita_engine_cb = function + | G.Executable (_, G.Macro (_, G.Inline _)) + | G.Executable (_, G.Command (_, G.Include _)) -> () + | ast -> + output_string och (pp_ast_statement ast); nl (); nl () + in + let matitac_lib_cb = output_string och in + GrafiteParser.set_callback grafite_parser_cb; + MatitaEngine.set_callback matita_engine_cb; + MatitacLib.set_callback matitac_lib_cb; + at_exit atexit +;; let extra_cmdline_specs = ref [] let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs @@ -228,27 +232,27 @@ let parse_cmdline init_status = wants [Registry] init_status; let includes = ref [] in let default_includes = [ - "."; BuildTimeConf.stdlib_dir_devel; BuildTimeConf.stdlib_dir_installed ; ] in let absolutize s = - if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd() ^"/"^s + if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s in let args = ref [] in let add_l l = fun s -> l := s :: !l in - let reduce_verbosity () = - Helm_registry.set_int "matita.verbosity" - (Helm_registry.get_int "matita.verbosity" - 1) in let print_version () = Printf.printf "%s\n" BuildTimeConf.version;exit 0 in - let increase_verbosity () = - Helm_registry.set_int "matita.verbosity" - (Helm_registry.get_int "matita.verbosity" + 1) in let no_innertypes () = Helm_registry.set_bool "matita.noinnertypes" true in + let set_baseuri s = + match Str.split (Str.regexp "::") s with + | [path; uri] -> Helm_registry.set "matita.baseuri" + (HExtlib.normalize_path (absolutize path)^" "^uri) + | _ -> raise (Failure "bad baseuri, use -b 'path::uri'") + in let arg_spec = let std_arg_spec = [ + "-b", Arg.String set_baseuri, " forces the baseuri of path"; "-I", Arg.String (add_l includes), (" Adds path to the list of searched paths for the " ^ "include command"); @@ -267,18 +271,15 @@ let parse_cmdline init_status = "-profile-only", Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), "Activates only profiler with label matching the provided regex"; - "-bench", - Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true), - "Turns on parsable output on stdout, that is timings for matitac..."; - "-preserve", - Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), - "Turns off automatic baseuri cleaning"; - "-q", Arg.Unit reduce_verbosity, "Reduce verbosity"; "-system", Arg.Unit (fun () -> Helm_registry.set_bool "matita.system" true), ("Act on the system library instead of the user one" ^ "\n WARNING: not for the casual user"); - "-v", Arg.Unit increase_verbosity, "Increase verbosity"; + "-dump", Arg.String dump, + " Dump with expanded macros to "; + "-v", + Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), + "Verbose mode"; "--version", Arg.Unit print_version, "Prints version"; ] in let debug_arg_spec = @@ -300,7 +301,9 @@ let parse_cmdline init_status = in Arg.parse arg_spec (add_l args) (usage ()); let includes = - List.map absolutize ((List.rev !includes) @ default_includes) in + List.map (fun x -> HExtlib.normalize_path (absolutize x)) + ((List.rev !includes) @ default_includes) + in set_list ~key:"matita.includes" includes; let args = List.rev (List.filter (fun x -> x <> "") !args) in set_list ~key:"matita.args" args; @@ -323,18 +326,12 @@ let conf_components = [ load_configuration; fill_registry; parse_cmdline] let other_components = - [ initialize_makelib; initialize_db; initialize_environment ] + [ initialize_db; initialize_environment ] let initialize_all () = status := List.fold_left (fun s f -> f s) !status (conf_components @ other_components) -(* initialize_notation - (initialize_environment - (initialize_db - (initialize_makelib - (load_configuration - (parse_cmdline !status))))) *) let parse_cmdline_and_configuration_file () = status := List.fold_left (fun s f -> f s) !status conf_components