(* 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/ *) open Printf open MatitaTypes (** {2 Initialization} *) 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 = if Helm_registry.get_bool "matita.quiet" 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 | End_of_file | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> MatitaLog.error (MatitaExcPp.to_string exn); raise exn let fname () = match Helm_registry.get_list Helm_registry.string "matita.args" with | [x] -> x | _ -> MatitaInit.die_usage () let pp_ocaml_mode () = MatitaLog.message ""; MatitaLog.message " ** Entering Ocaml mode ** "; MatitaLog.message ""; MatitaLog.message "Type 'go ();;' to enter an interactive matitac"; MatitaLog.message "" 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 = Ulexing.from_utf8_channel stdin in try run_script str (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 () | 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; CicNotation.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment (); CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in fun _ -> trust); status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; 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 let newcb tag s = match tag with | `Debug | `Message -> () | `Warning | `Error -> origcb tag s in if Helm_registry.get_bool "matita.quiet" then MatitaLog.set_log_callback newcb; let matita_debug = Helm_registry.get_bool "matita.debug" in try let time = Unix.time () in if Helm_registry.get_bool "matita.quiet" then origcb `Message ("compiling " ^ Filename.basename fname ^ "...") else MatitaLog.message (sprintf "execution of %s started:" fname); let is = Ulexing.from_utf8_channel (match fname with | "stdin" -> stdin | fname -> open_in fname) in run_script is (MatitaEngine.eval_from_stream ~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 = if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" 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 = 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"; clean_exit (Some 2) end else begin let moo_fname = MatitacleanLib.obj_file_of_script fname in MatitaMoo.save_moo moo_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!"; if mode = `COMPILER then clean_exit (Some ~-1) else pp_ocaml_mode () | MatitaEngine.Drop -> if mode = `COMPILER then clean_exit (Some 1) else pp_ocaml_mode () | 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); if mode = `COMPILER then clean_exit (Some 1) else pp_ocaml_mode () | exn -> if matita_debug then raise exn; if mode = `COMPILER then clean_exit (Some 3) else pp_ocaml_mode ()