let out = ref ignore
let set_callback f = out := f
+
let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
;;
+let dump f =
+ let module G = GrafiteAst in
+ let module L = LexiconAst in
+ let module H = HExtlib in
+ Helm_registry.set_bool "matita.moo" false;
+ let floc = H.dummy_floc in
+ let nl_ast = G.Comment (floc, G.Note (floc, "")) in
+ let pp_statement stm =
+ GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ ~lazy_term_pp:CicNotationPp.pp_term
+ ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
+ in
+ let pp_lexicon = LexiconAstPp.pp_command in
+ let och = open_out f in
+ let nl () = output_string och (pp_statement nl_ast) in
+ MatitaMisc.out_preamble och;
+ let grafite_parser_cb status = function
+ | G.Executable (_, G.Macro (_, G.Inline _)) -> ()
+ | stm ->
+ output_string och (pp_statement stm); nl (); nl ()
+ in
+ let lexicon_parser_cb status cmd =
+ output_string och (pp_lexicon cmd); nl (); nl ()
+ in
+(*
+ let matita_engine_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline _))
+ | G.Executable (_, G.Command (_, G.Include _)) -> ()
+ | ast ->
+*)
+ let matitac_lib_cb = output_string och in
+ begin fun () ->
+ GrafiteParser.set_grafite_callback grafite_parser_cb;
+ GrafiteParser.set_lexicon_callback lexicon_parser_cb;
+(*
+ MatitaEngine.set_callback matita_engine_cb;
+*)
+ set_callback matitac_lib_cb
+ end,
+ begin fun x ->
+ close_out och;
+ GrafiteParser.set_grafite_callback (fun _ _ -> ());
+ GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+ set_callback ignore; x
+ end
+;;
+
let get_macro_context = function
| Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
| Some status ->
| None -> assert false
;;
-let pp_times fname rc big_bang =
+let pp_times fname rc big_bang big_bang_u big_bang_s =
if not (Helm_registry.get_bool "matita.verbose") then
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
+ let u = u -. big_bang_u in
+ let s = s -. big_bang_s in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
let rc,rcascii =
if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
include_paths
;;
-let compile options fname =
+let activate_extraction baseuri fname =
+ if Helm_registry.get_bool "matita.extract" then
+ let mangled_baseuri =
+ let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+ let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+ String.uncapitalize baseuri in
+ let f =
+ open_out
+ (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
+ LibrarySync.add_object_declaration_hook
+ (fun ~add_obj ~add_coercion _ obj ->
+ output_string f (CicExportation.ppobj baseuri obj);
+ flush f; []);
+;;
+
+let compile atstart options fname =
let matita_debug = Helm_registry.get_bool "matita.debug" in
let include_paths = get_include_paths options in
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
- let grafite_status = GrafiteSync.init baseuri in
+ if Http_getter_storage.is_read_only baseuri then assert false;
+ activate_extraction baseuri fname ;
let lexicon_status =
CicNotation2.load_notation ~include_paths:[]
BuildTimeConf.core_notation_script
in
- let initial_lexicon_status = lexicon_status in
+ atstart (); (* FG: do not invoke before loading the core notation script *)
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
let big_bang = Unix.gettimeofday () in
+ let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
+ Unix.times ()
+ in
let time = Unix.time () in
try
(* sanity checks *)
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- if Http_getter_storage.is_read_only baseuri then
- HLog.error
- (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
LibraryClean.db_uris_of_baseuri baseuri <> [])
HLog.message ("baseuri " ^ baseuri ^ " is not empty");
HLog.message ("cleaning baseuri " ^ baseuri);
LibraryClean.clean_baseuris [baseuri];
- assert (Http_getter_storage.is_empty ~local:true baseuri);
end;
- (* create dir for XML files *)
- if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
- ~default:false)
- then
- HExtlib.mkdir
- (Filename.dirname
- (Http_getter.filename ~local:true ~writable:true (baseuri ^
- "foo.con")));
HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
if not (Helm_registry.get_bool "matita.verbose") then
(let cc =
in
let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
print_string s; flush stdout);
+ (* we dalay this error check until we print 'matitac file ' *)
+ assert (Http_getter_storage.is_empty ~local:true baseuri);
+ (* create dir for XML files *)
+ if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+ ~default:false)
+ then
+ HExtlib.mkdir
+ (Filename.dirname
+ (Http_getter.filename ~local:true ~writable:true (baseuri ^
+ "foo.con")));
let buf = Ulexing.from_utf8_channel (open_in fname) in
let print_cb =
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
else pp_ast_statement
in
- let grafite_status, lexicon_status =
- let rec aux_for_dump x =
+ let lexicon_status, grafite_status =
+ let rec aux_for_dump x lexicon_status grafite_status =
try
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
lexicon_status grafite_status buf x
with
- | [] -> grafite_status, lexicon_status
- | ((grafite,lexicon),None)::_ -> grafite, lexicon
+ | [] -> lexicon_status, grafite_status
+ | ((grafite,lexicon),None)::_ -> lexicon, grafite
| ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
- with MatitaEngine.EnrichedWithLexiconStatus
- (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
- match f (get_macro_context (Some grafite_status)) with
- | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+ with MatitaEngine.EnrichedWithStatus
+ (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
+ match f (get_macro_context (Some grafite)) with
+ | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
let str =
- ApplyTransformation.txt_of_inline_macro style suri prefix
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex") in
+ ApplyTransformation.txt_of_inline_macro style prefix suri
+ ?flavour
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ in
!out str;
- aux_for_dump x
+ aux_for_dump x lexicon grafite
|_-> raise exn
in
- aux_for_dump print_cb
+ aux_for_dump print_cb lexicon_status grafite_status
in
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
"there are still incomplete proofs at the end of the script";
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
+(*
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
+*)
clean_exit baseuri false)
else
(if not (Helm_registry.get_bool "matita.moo" &&
in
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
- pp_times fname true big_bang;
+ pp_times fname true big_bang big_bang_u big_bang_s;
+(*
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
+*)
true)
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| AttemptToInsertAnAlias lexicon_status ->
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
+(*
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
+*)
clean_exit baseuri false
- | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) ->
+ | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' ->
(match exn with
| Sys.Break -> HLog.error "user break!"
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
let (x, y) = HExtlib.loc_of_floc floc in
HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
- | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
- LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
- pp_times fname false big_bang;
+ | exn when matita_debug -> raise exn'
+ | exn -> HLog.error (snd (MatitaExcPp.to_string exn))
+ );
+(* LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
+ * *)
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
- | Sys.Break as exn ->
- if matita_debug then raise exn;
+ | Sys.Break when not matita_debug ->
HLog.error "user break!";
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
- | exn ->
- if matita_debug then raise exn;
+ | exn when not matita_debug ->
HLog.error
("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
- pp_times fname false big_bang;
+ pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
-;;
module F =
struct
let string_of_source_object s = s;;
let string_of_target_object s = s;;
+ let is_readonly_buri_of opts file =
+ let buri = List.assoc "baseuri" opts in
+ Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)
+ ;;
+
let root_and_target_of opts mafile =
try
let include_paths = get_include_paths opts in
let root,baseuri,_,_ =
Librarian.baseuri_of_script ~include_paths mafile
in
- Some root, LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- with Librarian.NoRootFor x -> None, ""
+ let obj_writeable, obj_read_only =
+ if Filename.check_suffix mafile ".mma" then
+ Filename.chop_suffix mafile ".mma" ^ ".ma",
+ Filename.chop_suffix mafile ".mma" ^ ".ma"
+ else
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ Some root, obj_writeable, obj_read_only
+ with Librarian.NoRootFor x -> None, "", ""
;;
let mtime_of_source_object s =
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
;;
- let build = compile;;
+(* FG: a problem was noticed in relising memory between subsequent *)
+(* invocations of the compiler. The following might help *)
+ let compact r = Gc.compact (); r
+
+ let build options fname =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let compile atstart opts fname =
+ try
+ GrafiteSync.push ();
+ GrafiteParser.push ();
+ let rc = compile atstart opts fname in
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ rc
+ with
+ | Sys.Break ->
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ false
+ | exn when not matita_debug ->
+ HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
+ assert false
+ in
+ if Filename.check_suffix fname ".mma" then
+ let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
+ let atstart, atexit = dump generated in
+ let res = compile atstart options fname in
+ let r = compact (atexit res) in
+ if r then r else begin
+(* Sys.remove generated; *)
+ Printf.printf "rm %s\n" generated; flush stdout; r
+ end
+ else
+ compile ignore options fname
+ ;;
let load_deps_file = Librarian.load_deps_file;;
projects / helm.git / blobdiff