matita/matitacLib.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 open GrafiteTypes
  31
  32 exception AttemptToInsertAnAlias
  33
  34 let pp_ast_statement =
  35   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
  36     ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
  37
  38 (** {2 Initialization} *)
  39
  40 let grafite_status = (ref None : GrafiteTypes.status option ref)
  41 let lexicon_status = (ref None : LexiconEngine.status option ref)
  42
  43 let run_script is eval_function  =
  44   let lexicon_status',grafite_status' =
  45     match !lexicon_status,!grafite_status with
  46     | Some ss, Some s -> ss,s
  47     | _,_ -> assert false
  48   in
  49   let slash_n_RE = Pcre.regexp "\\n" in
  50   let cb =
  51     if Helm_registry.get_int "matita.verbosity" < 1 then
  52       (fun _ _ -> ())
  53     else
  54       (fun grafite_status stm ->
  55         (* dump_status grafite_status; *)
  56         let stm = pp_ast_statement stm in
  57         let stm = Pcre.replace ~rex:slash_n_RE stm in
  58         let stm =
  59           if String.length stm > 50 then
  60             String.sub stm 0 50 ^ " ..."
  61           else
  62             stm
  63         in
  64         HLog.debug ("Executing: ``" ^ stm ^ "''"))
  65   in
  66   let matita_debug = Helm_registry.get_bool "matita.debug" in
  67   try
  68    let grafite_status'', lexicon_status'' =
  69     match eval_function lexicon_status' grafite_status' is cb with
  70        [] -> assert false
  71      | (s,None)::_ -> s
  72      | (s,Some _)::_ -> raise AttemptToInsertAnAlias
  73    in
  74     lexicon_status := Some lexicon_status'';
  75     grafite_status := Some grafite_status''
  76   with
  77   | GrafiteEngine.Drop
  78   | End_of_file
  79   | CicNotationParser.Parse_error _ as exn -> raise exn
  80   | exn ->
  81       if not matita_debug then
  82        HLog.error (snd (MatitaExcPp.to_string exn)) ;
  83       raise exn
  84
  85 let fname () =
  86   let rec aux = function
  87   | ""::tl -> aux tl
  88   | [x] -> x
  89   | [] -> MatitaInit.die_usage ()
  90   | l ->
  91       prerr_endline
  92         ("Wrong commands: " ^
  93           String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
  94       MatitaInit.die_usage ()
  95   in
  96   aux (Helm_registry.get_list Helm_registry.string "matita.args")
  97
  98 let pp_ocaml_mode () =
  99   HLog.message "";
 100   HLog.message "                      ** Entering Ocaml mode ** ";
 101   HLog.message "";
 102   HLog.message "Type 'go ();;' to enter an interactive matitac";
 103   HLog.message ""
 104
 105 let clean_exit n =
 106  let opt_exit =
 107   function
 108      None -> ()
 109    | Some n -> exit n
 110  in
 111   match !grafite_status with
 112      None -> opt_exit n
 113    | Some grafite_status ->
 114       try
 115        let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
 116        LibraryClean.clean_baseuris ~verbose:false [baseuri];
 117        opt_exit n
 118       with GrafiteTypes.Option_error("baseuri", "not found") ->
 119        (* no baseuri ==> nothing to clean yet *)
 120        opt_exit n
 121
 122 let rec interactive_loop () =
 123   let str = Ulexing.from_utf8_channel stdin in
 124   try
 125     run_script str
 126       (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true
 127       ~include_paths:(Helm_registry.get_list Helm_registry.string
 128         "matita.includes"))
 129   with
 130   | GrafiteEngine.Drop -> pp_ocaml_mode ()
 131   | GrafiteEngine.Macro (floc,_) ->
 132      let x, y = HExtlib.loc_of_floc floc in
 133       HLog.error
 134        (sprintf "A macro has been found in a script at %d-%d" x y);
 135       interactive_loop ()
 136   | Sys.Break -> HLog.error "user break!"; interactive_loop ()
 137   | GrafiteTypes.Command_error _ -> interactive_loop ()
 138   | End_of_file ->
 139      print_newline ();
 140      clean_exit (Some 0)
 141   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
 142      let x, y = HExtlib.loc_of_floc floc in
 143       HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
 144       interactive_loop ()
 145   | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
 146
 147 let go () =
 148   Helm_registry.load_from BuildTimeConf.matita_conf;
 149   Http_getter.init ();
 150   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
 151   LibraryDb.create_owner_environment ();
 152   CicEnvironment.set_trust (* environment trust *)
 153     (let trust =
 154       Helm_registry.get_opt_default Helm_registry.get_bool
 155         ~default:true "matita.environment_trust" in
 156      fun _ -> trust);
 157   let include_paths =
 158    Helm_registry.get_list Helm_registry.string "matita.includes" in
 159   grafite_status := Some (GrafiteSync.init ());
 160   lexicon_status :=
 161    Some (CicNotation2.load_notation ~include_paths
 162     BuildTimeConf.core_notation_script);
 163   Sys.catch_break true;
 164   interactive_loop ()
 165
 166 let pp_times fname bench_mode rc big_bang =
 167   if bench_mode then
 168     begin
 169       let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
 170       let r = Unix.gettimeofday () -. big_bang in
 171       let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
 172       let cc =
 173         if Str.string_match (Str.regexp ".*opt$") Sys.argv.(0) 0 then
 174           "matitac.opt"
 175         else
 176           "matitac"
 177       in
 178       let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
 179       let times =
 180         let fmt t =
 181           let seconds = int_of_float t in
 182           let cents = int_of_float ((t -. floor t) *. 100.0) in
 183           let minutes = seconds / 60 in
 184           let seconds = seconds mod 60 in
 185           Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
 186         in
 187         Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
 188       in
 189       let fname =
 190         match MatitamakeLib.development_for_dir (Filename.dirname fname) with
 191         | None -> fname
 192         | Some d ->
 193             let rootlen = String.length(MatitamakeLib.root_for_development d)in
 194             let fnamelen = String.length fname in
 195             assert (fnamelen > rootlen);
 196             String.sub fname rootlen (fnamelen - rootlen)
 197       in
 198       let fname =
 199         if fname.[0] = '/' then
 200           String.sub fname 1 (String.length fname - 1)
 201         else
 202           fname
 203       in
 204       let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
 205       print_endline s;
 206       flush stdout
 207     end
 208 ;;
 209
 210 let main ~mode =
 211   let big_bang = Unix.gettimeofday () in
 212   MatitaInit.initialize_all ();
 213   (* must be called after init since args are set by cmdline parsing *)
 214   let fname = fname () in
 215   let system_mode =  Helm_registry.get_bool "matita.system" in
 216   let bench_mode =  Helm_registry.get_bool "matita.bench" in
 217   if bench_mode then
 218     Helm_registry.set_int "matita.verbosity" 0;
 219   let include_paths =
 220    Helm_registry.get_list Helm_registry.string "matita.includes" in
 221   grafite_status := Some (GrafiteSync.init ());
 222   lexicon_status :=
 223    Some (CicNotation2.load_notation ~include_paths
 224     BuildTimeConf.core_notation_script);
 225   Sys.catch_break true;
 226   let origcb = HLog.get_log_callback () in
 227   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
 228   let newcb tag s =
 229     match tag with
 230     | `Debug | `Message -> ()
 231     | `Warning | `Error -> origcb tag s
 232   in
 233   if Helm_registry.get_int "matita.verbosity" < 1 then
 234     HLog.set_log_callback newcb;
 235   if bench_mode then MatitaMisc.shutup ();
 236   let matita_debug = Helm_registry.get_bool "matita.debug" in
 237   try
 238     let time = Unix.time () in
 239     if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then
 240       origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
 241     else
 242       HLog.message (sprintf "execution of %s started:" fname);
 243     let is =
 244       Ulexing.from_utf8_channel
 245         (match fname with
 246         | "stdin" -> stdin
 247         | fname -> open_in fname) in
 248     let include_paths =
 249      Helm_registry.get_list Helm_registry.string "matita.includes" in
 250     (try
 251       run_script is
 252        (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
 253          ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
 254      with End_of_file -> ());
 255     let elapsed = Unix.time () -. time in
 256     let tm = Unix.gmtime elapsed in
 257     let sec = string_of_int tm.Unix.tm_sec ^ "''" in
 258     let min =
 259       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else ""
 260     in
 261     let hou =
 262       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
 263     in
 264     let proof_status,moo_content_rev,metadata,lexicon_content_rev =
 265       match !lexicon_status,!grafite_status with
 266       | Some ss, Some s ->
 267          s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
 268           ss.LexiconEngine.lexicon_content_rev
 269       | _,_ -> assert false
 270     in
 271     if proof_status <> GrafiteTypes.No_proof then
 272      begin
 273       HLog.error
 274        "there are still incomplete proofs at the end of the script";
 275       pp_times fname bench_mode true big_bang;
 276       clean_exit (Some 2)
 277      end
 278     else
 279      begin
 280        let baseuri, _fullpathforfname =
 281         DependenciesParser.baseuri_of_script ~include_paths fname in
 282        let moo_fname =
 283          LibraryMisc.obj_file_of_baseuri
 284            ~must_exist:false ~baseuri ~writable:true
 285        in
 286        let lexicon_fname=
 287          LibraryMisc.lexicon_file_of_baseuri
 288           ~must_exist:false ~baseuri ~writable:true
 289        in
 290        let metadata_fname =
 291         LibraryMisc.metadata_file_of_baseuri
 292           ~must_exist:false ~baseuri ~writable:true
 293        in
 294        GrafiteMarshal.save_moo moo_fname moo_content_rev;
 295        LibraryNoDb.save_metadata metadata_fname metadata;
 296        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
 297        HLog.message
 298          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
 299        pp_times fname bench_mode true big_bang;
 300        exit 0
 301      end
 302   with
 303   | Sys.Break as exn ->
 304      if matita_debug then raise exn;
 305       HLog.error "user break!";
 306       pp_times fname bench_mode false big_bang;
 307       if mode = `COMPILER then
 308         clean_exit (Some ~-1)
 309       else
 310         pp_ocaml_mode ()
 311   | GrafiteEngine.Drop ->
 312       if mode = `COMPILER then
 313         begin
 314           pp_times fname bench_mode false big_bang;
 315           clean_exit (Some 1)
 316         end
 317       else
 318         pp_ocaml_mode ()
 319   | GrafiteEngine.Macro (floc,_) ->
 320      let x, y = HExtlib.loc_of_floc floc in
 321       HLog.error
 322        (sprintf "A macro has been found in a script at %d-%d" x y);
 323       if mode = `COMPILER then
 324         begin
 325           pp_times fname bench_mode false big_bang;
 326           clean_exit (Some 1)
 327         end
 328       else
 329         pp_ocaml_mode ()
 330   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
 331      let (x, y) = HExtlib.loc_of_floc floc in
 332      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
 333      if mode = `COMPILER then
 334        begin
 335          pp_times fname bench_mode false big_bang;
 336          clean_exit (Some 1)
 337        end
 338      else
 339        pp_ocaml_mode ()
 340   | exn ->
 341       if matita_debug then raise exn;
 342       if mode = `COMPILER then
 343         begin
 344           pp_times fname bench_mode false big_bang;
 345           clean_exit (Some 3)
 346         end
 347       else
 348         pp_ocaml_mode ()
 349