From: Enrico Tassi Date: Fri, 4 Jan 2008 18:31:43 +0000 (+0000) Subject: make directory erased, no more -bench since it is the default, X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a1a902e5c22ca2d322604551cffa5570e96542d0 make directory erased, no more -bench since it is the default, -v activates verbose mode, no more "matita.verbosity" and "matita.bench" just "matita.verbose". erased matitatop. --- diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index a1f2a0cfc..6998c1cbf 100644 --- a/components/library/libraryClean.ml +++ b/components/library/libraryClean.ml @@ -242,7 +242,7 @@ let clean_baseuris ?(verbose=true) buris = let buri = UriManager.buri_of_uri uri in if buri <> !last_baseuri then begin - if Helm_registry.get_bool "matita.bench" then + if not (Helm_registry.get_bool "matita.verbose") then (print_endline ("matitaclean " ^ buri ^ "/");flush stdout) else HLog.message ("Removing: " ^ buri ^ "/*"); diff --git a/make/main.ml b/make/main.ml deleted file mode 100644 index 0b9cf949a..000000000 --- a/make/main.ml +++ /dev/null @@ -1,34 +0,0 @@ - -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 s = s ^ ".o" - let build t = - print_string ("build "^t^"\n"); flush stdout; - ignore(Unix.system ("touch "^target_of t)) - ;; - 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 -> - prerr_endline ("Source file not found: "^s);assert false - ;; - let mtime_of_target_object t = - try Some (Unix.stat t).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = t -> None - ;; -end - -module M = Make.Make(F) - -let deps = [ - "a.c", [ "b.c"; "d.c" ]; - "b.c", [ "c.c"; "d.c" ]; - "c.c", []; - "d.c", ["e.c"]; - "e.c", []; - ] -;; - -M.make deps (Array.to_list Sys.argv);; diff --git a/make/make.ml b/make/make.ml deleted file mode 100644 index 5a0dc85ce..000000000 --- a/make/make.ml +++ /dev/null @@ -1,122 +0,0 @@ - -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 -> unit - - 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 deps = - let todo = List.filter (is_buildable compiled deps) deps in - if todo <> [] then - (List.iter F.build (List.map fst todo); - make (compiled@List.map fst todo) 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 - diff --git a/make/make.mli b/make/make.mli deleted file mode 100644 index 5346c82e7..000000000 --- a/make/make.mli +++ /dev/null @@ -1,20 +0,0 @@ - -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 -> unit - 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 diff --git a/make/test/a.c b/make/test/a.c deleted file mode 100644 index e69de29bb..000000000 diff --git a/make/test/b.c b/make/test/b.c deleted file mode 100644 index e69de29bb..000000000 diff --git a/make/test/c.c b/make/test/c.c deleted file mode 100644 index e69de29bb..000000000 diff --git a/make/test/d.c b/make/test/d.c deleted file mode 100644 index e69de29bb..000000000 diff --git a/make/test/e.c b/make/test/e.c deleted file mode 100644 index e69de29bb..000000000 diff --git a/matita/.depend b/matita/.depend index 6b220fd25..9b802e20b 100644 --- a/matita/.depend +++ b/matita/.depend @@ -14,14 +14,16 @@ matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \ matitaAutoGui.cmi 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 make.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx make.cmx buildTimeConf.cmx matitacLib.cmi +matitacLib.cmo: matitamakeLib.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmo applyTransformation.cmi matitacLib.cmi +matitacLib.cmx: matitamakeLib.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi matitaWiki.cmo matitaInit.cmi matitaEngine.cmi gragrep.cmi + matitacLib.cmi matitaWiki.cmo matitaMisc.cmi matitaInit.cmi \ + matitaEngine.cmi make.cmi gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx matitaMisc.cmx matitaInit.cmx \ + matitaEngine.cmx make.cmx gragrep.cmx matitadep.cmo: matitamakeLib.cmi matitaInit.cmi matitadep.cmi matitadep.cmx: matitamakeLib.cmx matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi diff --git a/matita/Makefile b/matita/Makefile index 4c8e313fd..2aef5b8fa 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -73,7 +73,7 @@ MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ matita matitac cicbrowser matitadep matitaclean \ matitamake matitaprover matitawiki -PROGRAMS = $(PROGRAMS_BYTE) matitatop +PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = dump_moo gragrep NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) @@ -149,10 +149,6 @@ rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) clean-rottened: find . -type f -name "*.ma.*.rottened" -exec rm {} \; -matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< - matitaprover: matitac $(H)test -f $@ || ln -s $< $@ matitaprover.opt: matitac.opt diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index e4cd8bfe5..350d332ff 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -48,13 +48,10 @@ let registry_defaults = [ "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"; "matita.do_heavy_checks", "true"; - (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is - * intuitively verbose *) ] let set_registry_values = @@ -240,14 +237,8 @@ let parse_cmdline init_status = 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 = @@ -277,18 +268,16 @@ 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"; + "-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 = diff --git a/matita/matitaMisc.ml b/matita/matitaMisc.ml index bb745f703..211295261 100644 --- a/matita/matitaMisc.ml +++ b/matita/matitaMisc.ml @@ -156,6 +156,8 @@ let list_tl_at ?(equality=(==)) e l = let shutup () = HLog.set_log_callback (fun _ _ -> ()); +(* let out = open_out "/dev/null" in Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr) +*) diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml index ed884bda8..b5dc5ccf7 100644 --- a/matita/matitaWiki.ml +++ b/matita/matitaWiki.ml @@ -209,7 +209,6 @@ let main () = ); (* must be called after init since args are set by cmdline parsing *) let system_mode = Helm_registry.get_bool "matita.system" in - Helm_registry.set_int "matita.verbosity" 0; let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in grafite_status := [GrafiteSync.init "cic:/matita/tests/"]; diff --git a/matita/matitac.ml b/matita/matitac.ml index d603d1b85..868326a8d 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -58,8 +58,6 @@ let pp_ast_statement st = "matita.paste_unicode_as_tex") ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st -(**) - let dump f = Helm_registry.set_bool "matita.moo" false; let floc = H.dummy_floc in @@ -86,7 +84,74 @@ let dump f = MatitaEngine.set_callback matita_engine_cb; MatitacLib.set_callback matitac_lib_cb; at_exit atexit - +;; + +(* compiler ala pascal/java using make *) +let main_compiler () = + 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] -> + 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 + Make.load_deps_file (root ^ "/depends") + in + (* must be called after init since args are set by cmdline parsing *) + let system_mode = Helm_registry.get_bool "matita.system" in + if system_mode then HLog.message "Compiling in system space"; + if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); + (* 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 + let rc = MatitacLib.compile fname in + (match oldfname with + | Some n -> Helm_registry.set_string "matita.filename" n; + | _ -> Helm_registry.unset "matita.filename"); + rc + ;; + end + in + let module Make = Make.Make(F) in + Make.make deps targets +;; + let main () = Helm_registry.set_bool "matita.moo" true; match Filename.basename Sys.argv.(0) with @@ -98,9 +163,9 @@ let main () = |"matitaprover.opt.static" ->Matitaprover.main() |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main() | _ -> - let dump_msg = " Dump source with expanded macros to " in - MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; - MatitacLib.main () + let dump_msg = " Dump with expanded macros to " in + MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; + main_compiler () let _ = main () diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index e1ebfd79e..80e81c2d7 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -32,133 +32,23 @@ open GrafiteTypes exception AttemptToInsertAnAlias let out = ref ignore - 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") - ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st - -(* NOBODY EVER USER matitatop - -let pp_ocaml_mode () = - HLog.message ""; - HLog.message " ** Entering Ocaml mode ** "; - HLog.message ""; - HLog.message "Type 'go ();;' to enter an interactive matitac"; - HLog.message "" - -let rec interactive_loop () = - let str = Ulexing.from_utf8_channel stdin in - try - run_script str - (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true - ~include_paths:(Helm_registry.get_list Helm_registry.string - "matita.includes")) - with - | GrafiteEngine.Drop -> pp_ocaml_mode () - | 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; - interactive_loop () - | _ -> - 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); - interactive_loop () - end - | Sys.Break -> HLog.error "user break!"; interactive_loop () - | GrafiteTypes.Command_error _ -> interactive_loop () - | End_of_file -> - print_newline (); - 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); - interactive_loop () - | exn -> HLog.error (Printexc.to_string exn); interactive_loop () - -let go () = - Helm_registry.load_from BuildTimeConf.matita_conf; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - LibraryDb.create_owner_environment (); - CicEnvironment.set_trust (* environment trust *) - (let trust = - Helm_registry.get_opt_default Helm_registry.get_bool - ~default:true "matita.environment_trust" in - fun _ -> trust); - 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; - 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 ^ "''")) +let pp_ast_statement grafite_status stm = + let stm = GrafiteAstPp.pp_statement + ~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) 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 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 ^ "''") ;; let clean_exit baseuri rc = @@ -174,60 +64,45 @@ let get_macro_context = function | None -> assert false ;; -let pp_times fname bench_mode rc big_bang = - if bench_mode then - begin - let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in - let r = Unix.gettimeofday () -. big_bang in - let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in - let cc = - if Str.string_match (Str.regexp ".*opt$") Sys.argv.(0) 0 then - "matitac.opt" - else - "matitac" - in - let rc = if rc then "OK" else "FAIL" in - let times = - let fmt t = - let seconds = int_of_float t in - let cents = int_of_float ((t -. floor t) *. 100.0) in - let minutes = seconds / 60 in - let seconds = seconds mod 60 in - Printf.sprintf "%dm%02d.%02ds" minutes seconds cents - in - Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s) +let pp_times fname rc big_bang = + if not (Helm_registry.get_bool "matita.verbose") then + let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in + let r = Unix.gettimeofday () -. big_bang in + let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in + let rc = if rc then "OK" else "FAIL" in + let times = + let fmt t = + let seconds = int_of_float t in + let cents = int_of_float ((t -. floor t) *. 100.0) in + let minutes = seconds / 60 in + let seconds = seconds mod 60 in + Printf.sprintf "%dm%02d.%02ds" minutes seconds cents in - let fname = - match MatitamakeLib.development_for_dir (Filename.dirname fname) with - | None -> fname - | Some d -> - let rootlen = String.length(MatitamakeLib.root_for_development d)in - let fnamelen = String.length fname in - assert (fnamelen > rootlen); - String.sub fname rootlen (fnamelen - rootlen) - in - let fname = - if fname.[0] = '/' then - String.sub fname 1 (String.length fname - 1) - else - fname - in - let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in - print_endline s; - flush stdout - end + Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s) + in + let s = Printf.sprintf "%-4s %s %s" rc times extra in + print_endline s; + flush stdout +;; + +let cut prefix s = + let lenp = String.length prefix in + let lens = String.length s in + assert (lens > lenp); + assert (String.sub s 0 lenp = prefix); + String.sub s lenp (lens-lenp) ;; -let rec compiler_loop fname = +let rec compile fname = + Helm_registry.set_string "matita.filename" 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 root,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 @@ -263,11 +138,27 @@ let rec compiler_loop fname = let big_bang = Unix.gettimeofday () in let time = Unix.time () in HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); + if not (Helm_registry.get_bool "matita.verbose") then + (let cc = + if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt" + else "matitac" + in + let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in + print_string s; flush stdout); let buf = Ulexing.from_utf8_channel (open_in fname) in + let print_cb = + if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) + else pp_ast_statement + in try let grafite_status, lexicon_status = - run_script buf lexicon_status grafite_status - (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths) + match + MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths + lexicon_status grafite_status buf print_cb + with + | [] -> raise End_of_file + | ((grafite,lexicon),None)::_ -> grafite, lexicon + | (s,Some _)::_ -> raise AttemptToInsertAnAlias in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = @@ -277,7 +168,7 @@ let rec compiler_loop fname = 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; + pp_times fname false big_bang; clean_exit baseuri false) else (if Helm_registry.get_bool "matita.moo" then begin @@ -295,108 +186,38 @@ let rec compiler_loop fname = in HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); - pp_times fname bench_mode true big_bang; + pp_times fname 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; + pp_times fname false big_bang; clean_exit baseuri false | GrafiteEngine.Macro (floc, f) -> - ((* THIS CODE IS NOW BROKEN *) HLog.warn "Codice da rivedere"; - match f (get_macro_context (Some grafite_status)) with + (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 + !out str; + compile 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; + pp_times fname 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); - pp_times fname bench_mode false big_bang; + pp_times fname false big_bang; clean_exit baseuri false | exn -> if matita_debug then raise exn; HLog.error (snd (MatitaExcPp.to_string exn)); - pp_times fname bench_mode false big_bang; + pp_times fname false big_bang; clean_exit baseuri false ;; -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 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; - if system_mode then HLog.message "Compiling in system space"; - if bench_mode then MatitaMisc.shutup (); - (* 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 - let module Make = Make.Make(F) in - Make.make deps targets - diff --git a/matita/matitacLib.mli b/matita/matitacLib.mli index 6921ac534..1fd12cbdb 100644 --- a/matita/matitacLib.mli +++ b/matita/matitacLib.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -val main: unit -> unit +val compile: string -> bool (* this callback is called on the expansion of every inline macro *) val set_callback: (string -> unit) -> unit diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml index 5425a2217..8409eb7bc 100644 --- a/matita/matitaclean.ml +++ b/matita/matitaclean.ml @@ -57,7 +57,7 @@ let ask_confirmation _ = let main () = let _ = MatitaInit.initialize_all () in - if Helm_registry.get_bool "matita.bench" then MatitaMisc.shutup (); + if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); match Helm_registry.get_list Helm_registry.string "matita.args" with | [ "all" ] -> if Helm_registry.get_bool "matita.system" then diff --git a/matita/matitatop.ml b/matita/matitatop.ml deleted file mode 100644 index 0aba1e9b5..000000000 --- a/matita/matitatop.ml +++ /dev/null @@ -1,31 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let _ = - let _ = Topdirs.dir_quit in - Toploop.loop Format.std_formatter; - assert false