From: Enrico Tassi Date: Fri, 4 Jan 2008 16:32:27 +0000 (+0000) Subject: matitac now compiles like make (recorsively) if needed. X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5356519d50425dfca5b42ad5faeb2181d4240c78 matitac now compiles like make (recorsively) if needed. baseuri is not a non optional field of the grafite status, since you can always know it at the beginnig --- diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 625b23323..766408c13 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -38,7 +38,6 @@ type 'a disambiguator_input = string * int * 'a type options = { do_heavy_checks: bool ; - clean_baseuri: bool } (** create a ProofEngineTypes.mk_fresh_name_type function which uses given @@ -409,7 +408,6 @@ type eval_ast = Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> @@ -481,10 +479,10 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri arity saturations baseuri = +let eval_coercion status ~add_composites uri arity saturations = let status,compounds = GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity - saturations baseuri + saturations (GrafiteTypes.get_baseuri status) in let moo_content = List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds) @@ -569,7 +567,7 @@ let add_coercions_of_record_to_moo obj lemmas status = with Not_found -> false,0 with Not_found -> assert false in - let buri, status = GrafiteTypes.get_baseuri status in + let buri = GrafiteTypes.get_baseuri status in (* looking at the fields we can know the 'wanted' coercions, but not the * actually generated ones. So, only the intersection between the wanted * and the actual should be in the moo as coercion, while everithing in @@ -648,8 +646,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status = GrafiteTypes.add_moo_content [cmd] status in status,[] | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> - eval_coercion status ~add_composites uri arity saturations - (GrafiteTypes.get_string_option status "baseuri") + eval_coercion status ~add_composites uri arity saturations | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] @@ -725,7 +722,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ".ind", (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in - let buri, status = GrafiteTypes.get_baseuri status in + let buri = GrafiteTypes.get_baseuri status in let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in @@ -830,13 +827,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status) status moo } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command -~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status +~disambiguate_macro ?(do_heavy_checks=false) status (text,prefix_len,st) -> - let opts = { - do_heavy_checks = do_heavy_checks ; - clean_baseuri = clean_baseuri } - in + let opts = { do_heavy_checks = do_heavy_checks ; } in match st with | GrafiteAst.Executable (_,ex) -> eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command diff --git a/components/grafite_engine/grafiteEngine.mli b/components/grafite_engine/grafiteEngine.mli index 63580ad2e..d1a07a4ed 100644 --- a/components/grafite_engine/grafiteEngine.mli +++ b/components/grafite_engine/grafiteEngine.mli @@ -51,7 +51,6 @@ val eval_ast : Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index 133dad2c0..ca3d873c5 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -55,7 +55,6 @@ let uris_for_inductive_type uri obj = | _ -> [uri] let add_obj refinement_toolkit uri obj status = - let baseuri, status = GrafiteTypes.get_baseuri status in let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in let add_to_universe (universe,status) uri = let term = CicUtil.term_of_uri uri in @@ -134,7 +133,7 @@ let time_travel ~present ~past = List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; List.iter LibrarySync.remove_obj objs_to_remove -let init () = +let init baseuri = LibrarySync.remove_all_coercions (); LibraryObjects.reset_defaults (); { @@ -144,5 +143,5 @@ let init () = objects = []; coercions = []; universe = Universe.empty; - baseuri = None; + baseuri = baseuri; } diff --git a/components/grafite_engine/grafiteSync.mli b/components/grafite_engine/grafiteSync.mli index 0a2595430..fbe1fc8db 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -40,4 +40,4 @@ val time_travel: present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit (* also resets the imperative part of the status *) -val init: unit -> GrafiteTypes.status +val init: string -> GrafiteTypes.status diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml index 01fb19c58..af819555b 100644 --- a/components/grafite_engine/grafiteTypes.ml +++ b/components/grafite_engine/grafiteTypes.ml @@ -58,7 +58,7 @@ type status = { objects: UriManager.uri list; coercions: UriManager.uri list; universe:Universe.universe; - baseuri: string option; + baseuri: string; } let get_current_proof status = @@ -142,13 +142,7 @@ let get_option status name = StringMap.find name status.options with Not_found -> raise (Option_error (name, "not found")) -let get_baseuri status = - match status.baseuri with - | Some b -> b, status - | None -> - let _,baseuri,_ = Librarian.baseuri_of_script (Librarian.filename()) in - baseuri, {status with baseuri = Some baseuri} -;; +let get_baseuri status = status.baseuri;; let set_option status name value = let types = [ (* no set options defined! *) ] in diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli index a8eb19ac9..8d9b81ed8 100644 --- a/components/grafite_engine/grafiteTypes.mli +++ b/components/grafite_engine/grafiteTypes.mli @@ -55,7 +55,7 @@ type status = { objects: UriManager.uri list; (** in-scope objects *) coercions: UriManager.uri list; (** defined coercions *) universe:Universe.universe; (** universe of terms used by auto *) - baseuri: string option; + baseuri: string; } val dump_status : status -> unit @@ -66,8 +66,7 @@ val add_moo_content: GrafiteMarshal.ast_command list -> status -> status val get_option : status -> string -> option_value val get_string_option : status -> string -> string val set_option : status -> string -> string -> status -(* to cache the baseuri of current file *) -val get_baseuri: status -> string * status +val get_baseuri: status -> string val get_current_proof: status -> ProofEngineTypes.proof val get_proof_metasenv: status -> Cic.metasenv diff --git a/matita/.depend b/matita/.depend index b0d8efc5b..6b220fd25 100644 --- a/matita/.depend +++ b/matita/.depend @@ -6,6 +6,8 @@ gragrep.cmo: matitaInit.cmi buildTimeConf.cmo gragrep.cmi gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi +make.cmo: make.cmi +make.cmx: make.cmi matitaAutoGui.cmo: matitaGeneratedGui.cmo applyTransformation.cmi \ matitaAutoGui.cmi matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ @@ -13,17 +15,15 @@ matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \ - applyTransformation.cmi matitacLib.cmi + matitaExcPp.cmi make.cmi buildTimeConf.cmo matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitacLib.cmi + matitaExcPp.cmx make.cmx buildTimeConf.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ matitacLib.cmi matitaWiki.cmo matitaInit.cmi matitaEngine.cmi gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx -matitadep.cmo: matitaInit.cmi matitadep.cmi -matitadep.cmx: matitaInit.cmx matitadep.cmi +matitadep.cmo: matitamakeLib.cmi matitaInit.cmi matitadep.cmi +matitadep.cmx: matitamakeLib.cmx matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaExcPp.cmi @@ -80,6 +80,8 @@ matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmo applyTransformation.cmi matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx applyTransformation.cmx +rottener.cmo: matitaInit.cmi buildTimeConf.cmo +rottener.cmx: matitaInit.cmx buildTimeConf.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo diff --git a/matita/Makefile b/matita/Makefile index 6595af73e..4c8e313fd 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -28,6 +28,7 @@ ifeq ($(NODB),true) endif MLI = \ + make.mli \ lablGraphviz.mli \ matitaTypes.mli \ matitaMisc.mli \ @@ -45,6 +46,7 @@ MLI = \ matitaGui.mli \ $(NULL) CMLI = \ + make.mli \ matitaTypes.mli \ matitaMisc.mli \ matitamakeLib.mli \ diff --git a/matita/make.ml b/matita/make.ml new file mode 100644 index 000000000..b1136642a --- /dev/null +++ b/matita/make.ml @@ -0,0 +1,143 @@ + +module type Format = sig + + type source_object + type target_object + + val target_of : source_object -> target_object + val string_of_source_object : source_object -> string + val string_of_target_object : target_object -> string + + val build : source_object -> bool + + val mtime_of_source_object : source_object -> float option + val mtime_of_target_object : target_object -> float option +end + +module Make = functor (F:Format) -> struct + + let prerr_endline _ = ();; + + let younger_s_t a b = + match F.mtime_of_source_object a, F.mtime_of_target_object b with + | Some a, Some b -> a < b + | _ -> false (* XXX check if correct *) + ;; + let younger_t_t a b = + match F.mtime_of_target_object a, F.mtime_of_target_object b with + | Some a, Some b -> a < b + | _ -> false (* XXX check if correct *) + ;; + + let is_built t = younger_s_t t (F.target_of t);; + + let rec needs_build deps compiled (t,dependencies) = + prerr_endline ("Checking if "^F.string_of_source_object t^" needs to be built"); + if List.mem t compiled then + (prerr_endline "already compiled"; + false) + else + if not (is_built t) then + (prerr_endline (F.string_of_source_object t^ + " is not built, thus needs to be built"); + true) + else + try + let unsat = + List.find + (needs_build deps compiled) + (List.map (fun x -> x, List.assoc x deps) dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^F.string_of_source_object (fst unsat)^ + " that needs to be built, thus needs to be built"); + true + with Not_found -> + try + let unsat = + List.find (younger_t_t (F.target_of t)) (List.map F.target_of dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^F.string_of_target_object + unsat^" and "^F.string_of_source_object t^".o is younger than "^ + F.string_of_target_object unsat^", thus needs to be built"); + true + with Not_found -> false + ;; + + let is_buildable compiled deps (t,dependencies) = + prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable"); + let b = needs_build deps compiled (t,dependencies) in + if not b then + (prerr_endline (F.string_of_source_object t^ + " does not need to be built, thus it not buildable"); + false) + else + try + let unsat = + List.find (needs_build deps compiled) + (List.map (fun x -> x, List.assoc x deps) dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^ + F.string_of_source_object (fst unsat)^ + " that needs build, thus is not buildable"); + false + with Not_found -> + prerr_endline + ("None of "^F.string_of_source_object t^ + " dependencies needs to be built, thus it is buildable"); + true + ;; + + let rec make compiled failed deps = + let todo = List.filter (is_buildable compiled deps) deps in + let todo = List.filter (fun (f,_) -> not (List.mem f failed)) todo in + if todo <> [] then + let compiled, failed = + List.fold_left + (fun (c,f) (file,_) -> + if F.build file then (file::c,f) + else (c,file::f)) + (compiled,failed) todo + in + make compiled failed deps + ;; + + let rec purge_unwanted_roots wanted deps = + let roots, rest = + List.partition + (fun (t,d) -> + not (List.exists (fun (_,d1) -> List.mem t d1) deps)) + deps + in + let newroots = List.filter (fun (t,_) -> List.mem t wanted) roots in + if newroots = roots then + deps + else + purge_unwanted_roots wanted (newroots @ rest) + ;; + + let make deps targets = + if targets = [] then + make [] [] deps + else + make [] [] (purge_unwanted_roots targets deps) + ;; + +end + +let load_deps_file f = + let deps = ref [] in + let ic = open_in f in + try + while true do + begin + let l = input_line ic in + match Str.split (Str.regexp " ") l with + | [] -> HLog.error "malformed deps file"; exit 1 + | he::tl -> deps := (he,tl) :: !deps + end + done; !deps + with End_of_file -> !deps +;; diff --git a/matita/make.mli b/matita/make.mli new file mode 100644 index 000000000..883586c46 --- /dev/null +++ b/matita/make.mli @@ -0,0 +1,22 @@ + +module type Format = + sig + type source_object + type target_object + val target_of : source_object -> target_object + val string_of_source_object : source_object -> string + val string_of_target_object : target_object -> string + val build : source_object -> bool + val mtime_of_source_object : source_object -> float option + val mtime_of_target_object : target_object -> float option + end + +module Make : + functor (F : Format) -> + sig + (* make [deps] [targets], targets = [] means make all *) + val make : (F.source_object * F.source_object list) list -> + F.source_object list -> unit + end + +val load_deps_file: string -> (string * string list) list diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml index 74c857caf..7ca67976a 100644 --- a/matita/matitaEngine.ml +++ b/matita/matitaEngine.ml @@ -41,7 +41,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t GrafiteTypes.set_metasenv metasenv grafite_status,tac let disambiguate_command lexicon_status_ref grafite_status cmd = - let baseuri, grafite_status = GrafiteTypes.get_baseuri grafite_status in + let baseuri = GrafiteTypes.get_baseuri grafite_status in let lexicon_status,metasenv,cmd = GrafiteDisambiguate.disambiguate_command ~baseuri !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd @@ -58,17 +58,17 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = in GrafiteTypes.set_metasenv metasenv grafite_status,macro -let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status +let eval_ast ?do_heavy_checks lexicon_status grafite_status (text,prefix_len,ast) = let lexicon_status_ref = ref lexicon_status in - let baseuri, grafite_status = GrafiteTypes.get_baseuri grafite_status in + let baseuri = GrafiteTypes.get_baseuri grafite_status in let new_grafite_status,new_objs = GrafiteEngine.eval_ast ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) ~disambiguate_command:(disambiguate_command lexicon_status_ref) ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) - ?do_heavy_checks ?clean_baseuri grafite_status (text,prefix_len,ast) in + ?do_heavy_checks grafite_status (text,prefix_len,ast) in let new_lexicon_status = LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in let new_aliases = @@ -104,7 +104,7 @@ let out = ref ignore let set_callback f = out := f let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) - ?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true) + ?do_heavy_checks ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb = let rec loop lexicon_status grafite_status statuses = @@ -133,7 +133,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) !out ast; cb grafite_status ast; let new_statuses = - eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + eval_ast ?do_heavy_checks lexicon_status grafite_status ("",0,ast) in if enforce_no_new_aliases then List.iter diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli index 83b549ec4..1db991f51 100644 --- a/matita/matitaEngine.mli +++ b/matita/matitaEngine.mli @@ -25,7 +25,6 @@ val eval_ast : ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> LexiconEngine.status -> GrafiteTypes.status -> string * int * @@ -47,7 +46,6 @@ val eval_from_stream : include_paths:string list -> ?prompt:bool -> ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> ?enforce_no_new_aliases:bool -> (* default true *) ?watch_statuses:(LexiconEngine.status -> GrafiteTypes.status -> unit) -> LexiconEngine.status -> diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index 8888b8dfe..14e7a0db8 100644 --- a/matita/matitaExcPp.ml +++ b/matita/matitaExcPp.ml @@ -117,10 +117,6 @@ let rec to_string = let _,msg = to_string exn in let (x, y) = HExtlib.loc_of_floc floc in Some floc, sprintf "Error at %d-%d: %s" x y msg - | GrafiteTypes.Option_error ("baseuri", "not found" ) -> - None, - "Baseuri not set for this script. " - ^ "Use 'set \"baseuri\" \"\".' to set it." | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 182f6e165..c5239ffb4 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -743,14 +743,14 @@ class script ~(source_view: GSourceView.source_view) () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in -let initial_statuses () = +let initial_statuses baseuri = (* these include_paths are used only to load the initial notation *) let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in let lexicon_status = CicNotation2.load_notation ~include_paths BuildTimeConf.core_notation_script in - let grafite_status = GrafiteSync.init () in + let grafite_status = GrafiteSync.init baseuri in grafite_status,lexicon_status in object (self) @@ -773,7 +773,7 @@ object (self) val mutable statements = [] (** executed statements *) - val mutable history = [ initial_statuses () ] + val mutable history = [ initial_statuses "cic:/matita/test/" ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -933,7 +933,8 @@ object (self) method assignFileName file = let root, buri, file = Librarian.baseuri_of_script ~include_paths file in - Helm_registry.set "matita.filename" file + Helm_registry.set "matita.filename" file; + self#reset_buffer method saveToFile () = let oc = open_out (Librarian.filename ()) in @@ -967,8 +968,10 @@ object (self) LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status method private reset_buffer = + let file = Librarian.filename () in + let root, buri, file = Librarian.baseuri_of_script file in statements <- []; - history <- [ initial_statuses () ]; + history <- [ initial_statuses buri ]; userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml index 3c5607bd7..ed884bda8 100644 --- a/matita/matitaWiki.ml +++ b/matita/matitaWiki.ml @@ -212,7 +212,7 @@ let main () = Helm_registry.set_int "matita.verbosity" 0; let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in - grafite_status := [GrafiteSync.init ()]; + grafite_status := [GrafiteSync.init "cic:/matita/tests/"]; lexicon_status := [CicNotation2.load_notation ~include_paths BuildTimeConf.core_notation_script] ; diff --git a/matita/matitac.ml b/matita/matitac.ml index 31258f694..d603d1b85 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -100,8 +100,7 @@ let main () = | _ -> let dump_msg = " Dump source with expanded macros to " in MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; - let _ = MatitacLib.main `COMPILER in - () + MatitacLib.main () let _ = main () diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 3cb8ae419..e1ebfd79e 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -37,69 +37,11 @@ let set_callback f = out := f let pp_ast_statement st = GrafiteAstPp.pp_statement - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st -(** {2 Initialization} *) - -let grafite_status = (ref None : GrafiteTypes.status option ref) -let lexicon_status = (ref None : LexiconEngine.status option ref) - -let run_script is eval_function = - let lexicon_status',grafite_status' = - match !lexicon_status,!grafite_status with - | Some ss, Some s -> ss,s - | _,_ -> assert false - in - let slash_n_RE = Pcre.regexp "\\n" in - let cb = - if Helm_registry.get_int "matita.verbosity" < 1 then - (fun _ _ -> ()) - else - (fun grafite_status stm -> - (* dump_status grafite_status; *) - let stm = pp_ast_statement stm in - let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = - if String.length stm > 50 then - String.sub stm 0 50 ^ " ..." - else - stm - in - HLog.debug ("Executing: ``" ^ stm ^ "''")) - in - let matita_debug = Helm_registry.get_bool "matita.debug" in - try - match eval_function lexicon_status' grafite_status' is cb with - [] -> raise End_of_file - | ((grafite_status'',lexicon_status''),None)::_ -> - lexicon_status := Some lexicon_status''; - grafite_status := Some grafite_status'' - | (s,Some _)::_ -> raise AttemptToInsertAnAlias - with - | GrafiteEngine.Drop - | End_of_file - | CicNotationParser.Parse_error _ - | GrafiteEngine.Macro _ as exn -> raise exn - | exn -> - if not matita_debug then - HLog.error (snd (MatitaExcPp.to_string exn)) ; - raise exn - -let fname () = - let rec aux = function - | ""::tl -> aux tl - | [x] -> x - | [] -> MatitaInit.die_usage () - | l -> - prerr_endline - ("Wrong commands: " ^ - String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l)); - MatitaInit.die_usage () - in - aux (Helm_registry.get_list Helm_registry.string "matita.args") +(* NOBODY EVER USER matitatop let pp_ocaml_mode () = HLog.message ""; @@ -108,31 +50,6 @@ let pp_ocaml_mode () = HLog.message "Type 'go ();;' to enter an interactive matitac"; HLog.message "" -let clean_exit n = - let opt_exit = - function - None -> () - | Some n -> exit n - in - match !grafite_status with - None -> opt_exit n - | Some grafite_status -> - try - let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in - LibraryClean.clean_baseuris ~verbose:false [baseuri]; - opt_exit n - with GrafiteTypes.Option_error("baseuri", "not found") -> - (* no baseuri ==> nothing to clean yet *) - opt_exit n - -let get_macro_context = function - | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> [] - | Some status -> - let stack = GrafiteTypes.get_stack status in - let goal = Continuationals.Stack.find_goal stack in - GrafiteTypes.get_proof_context status goal - | None -> assert false - let rec interactive_loop () = let str = Ulexing.from_utf8_channel stdin in try @@ -161,7 +78,7 @@ let rec interactive_loop () = | GrafiteTypes.Command_error _ -> interactive_loop () | End_of_file -> print_newline (); - clean_exit (Some 0) + clean_exit fname (Some 0) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let x, y = HExtlib.loc_of_floc floc in HLog.error (sprintf "Parse error at %d-%d: %s" x y err); @@ -186,7 +103,77 @@ let go () = BuildTimeConf.core_notation_script); Sys.catch_break true; interactive_loop () +;; +*) +(* snippet for extraction, should be moved to the build function + if false then + (let baseuri = + (* This does not work yet :-( + let baseuri = + GrafiteTypes.get_string_option + (match !grafite_status with None -> assert false | Some s -> s) + "baseuri" in*) + lazy + (let _root, buri, _fname = Librarian.baseuri_of_script ~include_paths:[] fname in + buri) + in + let mangled_baseuri = + lazy + ( let baseuri = Lazy.force baseuri in + let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in + let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in + String.uncapitalize baseuri + ) in + let f = + lazy + (open_out + (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in + LibrarySync.set_object_declaration_hook + (fun _ obj -> + output_string (Lazy.force f) + (CicExportation.ppobj (Lazy.force baseuri) obj); + flush (Lazy.force f))); +*) + +(** {2 Initialization} *) + +let slash_n_RE = Pcre.regexp "\\n" ;; + +let run_script is lexicon_status' grafite_status' eval_function = + let print_cb = + if Helm_registry.get_int "matita.verbosity" < 1 then + (fun _ _ -> ()) + else + (fun grafite_status stm -> + let stm = pp_ast_statement stm in + let stm = Pcre.replace ~rex:slash_n_RE stm in + let stm = + if String.length stm > 50 then String.sub stm 0 50 ^ " ..." + else stm + in + HLog.debug ("Executing: ``" ^ stm ^ "''")) + in + match eval_function lexicon_status' grafite_status' is print_cb with + | [] -> raise End_of_file + | ((grafite_status'',lexicon_status''),None)::_ -> + grafite_status'', lexicon_status'' + | (s,Some _)::_ -> raise AttemptToInsertAnAlias +;; + +let clean_exit baseuri rc = + LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc +;; + +let get_macro_context = function + | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> [] + | Some status -> + let stack = GrafiteTypes.get_stack status in + let goal = Continuationals.Stack.find_goal stack in + GrafiteTypes.get_proof_context status goal + | None -> assert false +;; + let pp_times fname bench_mode rc big_bang = if bench_mode then begin @@ -231,213 +218,185 @@ let pp_times fname bench_mode rc big_bang = end ;; -let rec compiler_loop fname big_bang mode buf = - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in - let matita_debug = Helm_registry.get_bool "matita.debug" in - let bench_mode = Helm_registry.get_bool "matita.bench" in - try - run_script buf - (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - ~clean_baseuri) - with - | End_of_file -> () +let rec compiler_loop fname = + (* initialization, MOVE OUTSIDE *) + let matita_debug = Helm_registry.get_bool "matita.debug" in + let bench_mode = Helm_registry.get_bool "matita.bench" in + let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" + in + (* sanity checks *) + let _,baseuri,fname = Librarian.baseuri_of_script ~include_paths fname in + let moo_fname = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true + in + let lexicon_fname= + LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true + in + if Http_getter_storage.is_read_only baseuri then + HLog.error + (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); + (* cleanup of previously compiled objects *) + if (not (Http_getter_storage.is_empty ~local:true baseuri) || + LibraryClean.db_uris_of_baseuri baseuri <> []) && clean_baseuri + then begin + HLog.message ("baseuri " ^ baseuri ^ " is not empty"); + HLog.message ("cleaning baseuri " ^ baseuri); + LibraryClean.clean_baseuris [baseuri]; + assert (Http_getter_storage.is_empty ~local:true baseuri); + end; + (* create dir for XML files *) + if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" + ~default:false) + then + HExtlib.mkdir + (Filename.dirname + (Http_getter.filename ~local:true ~writable:true (baseuri ^ + "foo.con"))); + (* begin of compilation *) + let grafite_status = GrafiteSync.init baseuri in + let lexicon_status = + CicNotation2.load_notation ~include_paths:[] + BuildTimeConf.core_notation_script + in + let big_bang = Unix.gettimeofday () in + let time = Unix.time () in + HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); + let buf = Ulexing.from_utf8_channel (open_in fname) in + try + let grafite_status, lexicon_status = + run_script buf lexicon_status grafite_status + (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths) + in + let elapsed = Unix.time () -. time in + let proof_status,moo_content_rev,lexicon_content_rev = + grafite_status.proof_status, grafite_status.moo_content_rev, + lexicon_status.LexiconEngine.lexicon_content_rev + in + if proof_status <> GrafiteTypes.No_proof then + (HLog.error + "there are still incomplete proofs at the end of the script"; + pp_times fname bench_mode false big_bang; + clean_exit baseuri false) + else + (if Helm_registry.get_bool "matita.moo" then begin + (* FG: we do not generate .moo when dumping .mma files *) + GrafiteMarshal.save_moo moo_fname moo_content_rev; + LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + end; + let tm = Unix.gmtime elapsed in + let sec = string_of_int tm.Unix.tm_sec ^ "''" in + let min = + if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else "" + in + let hou = + if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else "" + in + HLog.message + (sprintf "execution of %s completed in %s." fname (hou^min^sec)); + pp_times fname bench_mode true big_bang; + true) + with + | End_of_file -> HLog.error "End_of_file?!"; clean_exit baseuri false | Sys.Break as exn -> if matita_debug then raise exn; - HLog.error "user break!"; - pp_times fname bench_mode false big_bang; - if mode = `COMPILER then - clean_exit (Some ~-1) - else - pp_ocaml_mode () - | GrafiteEngine.Drop -> - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () + HLog.error "user break!"; + pp_times fname bench_mode false big_bang; + clean_exit baseuri false | GrafiteEngine.Macro (floc, f) -> - begin match f (get_macro_context !grafite_status) with - | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = - ApplyTransformation.txt_of_inline_macro style suri prefix - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") in - !out str; - compiler_loop fname big_bang mode buf - | _ -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () - end + ((* THIS CODE IS NOW BROKEN *) HLog.warn "Codice da rivedere"; + match f (get_macro_context (Some grafite_status)) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in + print_endline str; + compiler_loop fname + | _ -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "A macro has been found at %d-%d" x y); + pp_times fname bench_mode false big_bang; + clean_exit baseuri false) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let (x, y) = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err); - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () + let (x, y) = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); + pp_times fname bench_mode false big_bang; + clean_exit baseuri false | exn -> - if matita_debug then raise exn; - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 3) - end - else - pp_ocaml_mode () - -exception ReadOnlyUri of string + if matita_debug then raise exn; + HLog.error (snd (MatitaExcPp.to_string exn)); + pp_times fname bench_mode false big_bang; + clean_exit baseuri false +;; -let main ~mode = - let big_bang = Unix.gettimeofday () in +let main () = MatitaInit.initialize_all (); + (* targets and deps *) + let targets = Helm_registry.get_list Helm_registry.string "matita.args" in + let deps = + match targets with + | [] -> + (match Librarian.find_roots_in_dir (Sys.getcwd ()) with + | [x] -> + HLog.message ("Using the following root: " ^ x); + Make.load_deps_file (Filename.dirname x ^ "/depends") + | [] -> + HLog.error "No targets and no root found"; exit 1 + | roots -> + HLog.error ("Too many roots found, move into one and retry: "^ + String.concat ", " roots);exit 1); + | hd::_ -> + let root, _, _ = Librarian.baseuri_of_script hd in + HLog.message ("Using the following root: " ^ root); + Make.load_deps_file (root ^ "/depends") + in (* must be called after init since args are set by cmdline parsing *) - let fname = fname () in - if false then - (let baseuri = - (* This does not work yet :-( - let baseuri = - GrafiteTypes.get_string_option - (match !grafite_status with None -> assert false | Some s -> s) - "baseuri" in*) - lazy - (let _root, buri, _fname = Librarian.baseuri_of_script ~include_paths:[] fname in - buri) - in - let mangled_baseuri = - lazy - ( let baseuri = Lazy.force baseuri in - let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in - let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in - String.uncapitalize baseuri - ) in - let f = - lazy - (open_out - (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in - LibrarySync.set_object_declaration_hook - (fun _ obj -> - output_string (Lazy.force f) - (CicExportation.ppobj (Lazy.force baseuri) obj); - flush (Lazy.force f))); let system_mode = Helm_registry.get_bool "matita.system" in let bench_mode = Helm_registry.get_bool "matita.bench" in - if bench_mode then - Helm_registry.set_int "matita.verbosity" 0; - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - grafite_status := Some (GrafiteSync.init ()); - lexicon_status := - Some (CicNotation2.load_notation ~include_paths - BuildTimeConf.core_notation_script); - Sys.catch_break true; - let origcb = HLog.get_log_callback () in - let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in - let newcb tag s = - match tag with - | `Debug | `Message -> () - | `Warning | `Error -> origcb tag s - in - if Helm_registry.get_int "matita.verbosity" < 1 then - HLog.set_log_callback newcb; + if bench_mode then Helm_registry.set_int "matita.verbosity" 0; + if system_mode then HLog.message "Compiling in system space"; if bench_mode then MatitaMisc.shutup (); - let ich, fname, baseuri = - if fname = "stdin" || fname = "-" then - let fname = "/dev/fd/0" in - let _,baseuri,fname = - Librarian.baseuri_of_script ~include_paths:[] fname - in - stdin, fname, baseuri - else - let _,baseuri,fname = - Librarian.baseuri_of_script ~include_paths fname - in - open_in fname, fname, baseuri - in - (* PUT THIS IN A FUNCTION *) - if Http_getter_storage.is_read_only baseuri then begin - HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" - baseuri); - raise (ReadOnlyUri baseuri) - end; - if (not (Http_getter_storage.is_empty ~local:true baseuri) || - LibraryClean.db_uris_of_baseuri baseuri <> []) - then begin - HLog.message ("baseuri " ^ baseuri ^ " is not empty"); - HLog.message ("cleaning baseuri " ^ baseuri); - LibraryClean.clean_baseuris [baseuri]; - assert (Http_getter_storage.is_empty ~local:true baseuri); - end; - if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" - ~default:false) - then - HExtlib.mkdir - (Filename.dirname - (Http_getter.filename ~local:true ~writable:true (baseuri ^ - "foo.con"))); - (* PUT THIS IN A FUNCTION *) - let time = Unix.time () in - if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then - origcb `Message ("compiling " ^ - Filename.basename fname ^ " in " ^ baseuri ^ " ...") - else - HLog.message (sprintf "execution of %s started in %s:" - (Filename.basename fname) baseuri); - let buf = Ulexing.from_utf8_channel ich in - compiler_loop fname big_bang mode buf; - let elapsed = Unix.time () -. time in - let tm = Unix.gmtime elapsed in - let sec = string_of_int tm.Unix.tm_sec ^ "''" in - let min = - if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" - in - let hou = - if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" - in - let proof_status,moo_content_rev,lexicon_content_rev = - match !lexicon_status,!grafite_status with - | Some ss, Some s -> - s.proof_status, s.moo_content_rev, - ss.LexiconEngine.lexicon_content_rev - | _,_ -> assert false + (* here we go *) + let module F = + struct + type source_object = string + type target_object = string + let string_of_source_object s = s;; + let string_of_target_object s = s;; + + let target_of mafile = + let _,baseuri,_ = Librarian.baseuri_of_script mafile in + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true + ;; + + let mtime_of_source_object s = + try Some (Unix.stat s).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> + raise (Failure ("Unable to stat a source file: " ^ s)) + ;; + + let mtime_of_target_object s = + try Some (Unix.stat s).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None + ;; + + let build fname = + let oldfname = + Helm_registry.get_opt + Helm_registry.string "matita.filename" + in + Helm_registry.set_string "matita.filename" fname; + let rc = compiler_loop fname in + (match oldfname with + | Some n -> Helm_registry.set_string "matita.filename" n; + | _ -> Helm_registry.unset "matita.filename"); + rc + ;; + end in - if proof_status <> GrafiteTypes.No_proof then - begin - HLog.error - "there are still incomplete proofs at the end of the script"; - pp_times fname bench_mode true big_bang; - clean_exit (Some 2) - end - else - begin - let moo_fname = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in - let lexicon_fname= - LibraryMisc.lexicon_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in - (* FG: we do not generate .moo when dumping .mma files *) - if Helm_registry.get_bool "matita.moo" then begin - GrafiteMarshal.save_moo moo_fname moo_content_rev; - LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - end; - HLog.message - (sprintf "execution of %s completed in %s." fname (hou^min^sec)); - pp_times fname bench_mode true big_bang; - exit 0 - end + let module Make = Make.Make(F) in + Make.make deps targets + diff --git a/matita/matitacLib.mli b/matita/matitacLib.mli index 5e8a2635b..6921ac534 100644 --- a/matita/matitacLib.mli +++ b/matita/matitacLib.mli @@ -23,18 +23,7 @@ * http://helm.cs.unibo.it/ *) -val interactive_loop : unit -> unit - -(** go initializes the status and calls interactive_loop *) -val go : unit -> unit -val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit - -(** clean_exit n - if n = Some n it performs an exit [n] after a complete clean-up of what was - partially compiled - otherwise it performs the clean-up without exiting -*) -val clean_exit : int option -> unit +val main: unit -> unit (* this callback is called on the expansion of every inline macro *) val set_callback: (string -> unit) -> unit diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 2fc72ad8a..4e309ae75 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -88,7 +88,7 @@ let main () = let ma_files = args in (* here we go *) (* fills: - Hashtbl.add include_deps ma_file moo_file + Hashtbl.add include_deps ma_file ma_file Hashtbl.add include_deps_dot ma_file baseuri *) List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files; diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml index 7a6503ab3..79ab7683b 100644 --- a/matita/matitaprover.ml +++ b/matita/matitaprover.ml @@ -104,7 +104,7 @@ let main () = in (* prerr_endline data; *) let is = Ulexing.from_utf8_string data in - let gs = GrafiteSync.init () in + let gs = GrafiteSync.init "cic:/TPTP/" in let ls = CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script @@ -115,7 +115,6 @@ let main () = MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths:[] - ~clean_baseuri:true ~do_heavy_checks:false ~prompt:false ls gs is