]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitacLib.ml
Dama is now in the night benchmarks.
[helm.git] / helm / software / 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