-let arg_spec = [
-(* "-opt", Arg...., "set bla bla bla"; *)
-]
-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 scripts =
- let acc = ref [] in
- let add_script fname = acc := fname :: !acc in
- Arg.parse arg_spec add_script usage;
- List.rev !acc
-
-let run_script fname =
- let is =
- Stream.of_channel
- (match fname with
- | "stdin" -> stdin
- | fname -> open_in fname)
- in
- let status = ref (Lazy.force MatitaEngine.initial_status) 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 ^ "''")
- in
- try
- status := MatitaEngine.eval_from_stream !status is cb ;
- !status
- with
- | CicTextualParser2.Parse_error (floc,err) ->
- let (x, y) = CicAst.loc_of_floc floc in
- MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
- Http_getter.sync_dump_file ();
- exit 1
- | exn ->
- MatitaLog.error (Printexc.to_string exn);
- raise exn
-
-let _ =
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
- Sys.catch_break true;
- try
- List.iter (fun fname ->
- let time = Unix.time () in
- MatitaLog.message (sprintf "execution of %s started:" fname);
- let status = run_script fname in
- 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 = status.proof_status in
- if proof_status <> MatitaTypes.No_proof then
- begin
- MatitaLog.error
- "there are still incomplete proofs at the end of the script";
- exit(-1)
- end
- else
- begin
- MatitaLog.message
- (sprintf "execution of %s completed in %s." fname (hou^min^sec)) ;
- exit(0)
- end
- ) scripts
- with Sys.Break ->
- MatitaLog.error "user break!";
- exit (-1)