X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=ebf1e455bff5d62f4cd9d28f0e0be43441811603;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=1baa34910c3a1356d5c08b0b3133a9e28a1e7f30;hpb=d9394782ed9580f3565eb9b4682d8348aae6349e;p=helm.git diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 1baa34910..ebf1e455b 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -29,41 +29,55 @@ open MatitaTypes (** {2 Initialization} *) +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 set_b b = fun () -> b := true;; + let arg_spec = [ -(* "-opt", Arg...., "set bla bla bla"; *) + "-I", Arg.String (add_l paths_to_search_in), + " Adds path to the list of searched paths for the include command"; + "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation"; + "-preserve", Arg.Unit (set_b dont_delete_baseuri), + "Turns off automatic baseuri cleaning" ] let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" BuildTimeConf.version -let _ = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment () - -let status = ref (Lazy.force MatitaEngine.initial_status) ;; +let status = ref None let run_script is eval_function = + let status = + match !status with + | None -> assert false + | Some s -> s + in let slash_n_RE = Pcre.regexp "\\n" in - let cb status stm = - (* dump_status status; *) - let stm = TacticAstPp.pp_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 - MatitaLog.debug ("Executing: ``" ^ stm ^ "''") + let cb = + if !quiet_compilation then + fun _ _ -> () + else + fun status stm -> + (* dump_status status; *) + let stm = GrafiteAstPp.pp_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 + MatitaLog.debug ("Executing: ``" ^ stm ^ "''") in try eval_function status is cb with | MatitaEngine.Drop - | CicTextualParser2.Parse_error _ as exn -> raise exn + | End_of_file + | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> MatitaLog.error (MatitaExcPp.to_string exn); raise exn @@ -83,41 +97,89 @@ let pp_ocaml_mode () = MatitaLog.message "Type 'go ();;' to enter an interactive matitac"; MatitaLog.message "" -let rec go () = +let clean_exit n = + let opt_exit = + function + None -> () + | Some n -> exit n + in + match !status with + None -> opt_exit n + | Some status -> + try + let baseuri = MatitaTypes.get_string_option !status "baseuri" in + MatitacleanLib.clean_baseuris ~verbose:false [baseuri]; + opt_exit n + with MatitaTypes.Option_error("baseuri", "not found") -> + (* no baseuri ==> nothing to clean yet *) + opt_exit n + +let rec interactive_loop () = let str = Stream.of_channel stdin in try - run_script str MatitaEngine.eval_from_stream_greedy + run_script str + (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in) with | MatitaEngine.Drop -> pp_ocaml_mode () - | Sys.Break -> MatitaLog.error "user break!"; go () - | MatitaTypes.Command_error _ -> go () - | CicTextualParser2.Parse_error (floc,err) -> - (* check for EOI *) - if Stream.peek str = None then - exit 0 - else - let (x, y) = CicAst.loc_of_floc floc in - MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); - | exn -> MatitaLog.error (Printexc.to_string exn); go () + | Sys.Break -> MatitaLog.error "user break!"; interactive_loop () + | MatitaTypes.Command_error _ -> interactive_loop () + | End_of_file -> + print_newline (); + clean_exit (Some 0) + | CicNotationParser.Parse_error (floc,err) -> + let (x, y) = CicNotationPt.loc_of_floc floc in + MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); + interactive_loop () + | exn -> MatitaLog.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"); + status := Some (ref (Lazy.force MatitaEngine.initial_status)); + Sys.catch_break true; + interactive_loop () + +let dump_moo_to_file file moo = + let os = open_out (MatitaMisc.obj_file_of_script file) in + let output s = output_string os s in + output "(* GENERATED FILE: DO NOT EDIT! *)\n\n"; + List.iter output (List.rev moo); + close_out os let main ~mode = - at_exit - (fun () -> - Http_getter_logger.log "Sync map tree to disk..."; - Http_getter.sync_dump_file (); - print_endline "\nThanks for using Matita!\n"); + Helm_registry.load_from BuildTimeConf.matita_conf; + CicNotation.load_notation BuildTimeConf.core_notation_script; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.create_owner_environment (); + status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; + let origcb = MatitaLog.get_log_callback () in + let newcb tag s = + match tag with + | `Debug | `Message -> () + | `Warning | `Error -> origcb tag s + in let fname = fname () in + if !quiet_compilation then + MatitaLog.set_log_callback newcb; try let time = Unix.time () in - MatitaLog.message (sprintf "execution of %s started:" fname); + if !quiet_compilation then + origcb `Message ("compiling " ^ Filename.basename fname ^ "...") + else + MatitaLog.message (sprintf "execution of %s started:" fname); let is = Stream.of_channel (match fname with | "stdin" -> stdin | fname -> open_in fname) in - run_script is MatitaEngine.eval_from_stream; + run_script is + (MatitaEngine.eval_from_stream + ~include_paths:!paths_to_search_in + ~clean_baseuri:(not !dont_delete_baseuri)); let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = @@ -129,29 +191,45 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status = !status.proof_status in + let proof_status,moo_content_rev = + match !status with + | Some s -> !s.proof_status, !s.moo_content_rev + | None -> assert false + in if proof_status <> MatitaTypes.No_proof then begin MatitaLog.error "there are still incomplete proofs at the end of the script"; - exit 2 + clean_exit (Some 2) end else begin + dump_moo_to_file fname moo_content_rev; MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); exit 0 end with - | Sys.Break -> MatitaLog.error "user break!"; exit ~-1 + | Sys.Break -> + MatitaLog.error "user break!"; + if mode = `COMPILER then + clean_exit (Some ~-1) + else + pp_ocaml_mode () | MatitaEngine.Drop -> if mode = `COMPILER then - exit 1 + clean_exit (Some 1) else pp_ocaml_mode () - | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in + | CicNotationParser.Parse_error (floc,err) -> + let (x, y) = CicNotationPt.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); - Http_getter.sync_dump_file (); - exit 1 - + if mode = `COMPILER then + clean_exit (Some 1) + else + pp_ocaml_mode () + | _ -> + if mode = `COMPILER then + clean_exit (Some 3) + else + pp_ocaml_mode ()