]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matitacLib.ml
dama, tests, legacy ported
[helm.git] / matita / matitacLib.ml
index 3cb8ae4196ecdc0f648e3ebe2c4e6984f2affe23..51834f6e74f86511f385e182c02c721bc5abd22e 100644 (file)
@@ -29,101 +29,31 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias
+exception AttemptToInsertAnAlias of LexiconEngine.status
 
 let out = ref ignore 
-
 let set_callback f = out := f
 
-let pp_ast_statement st =
-  GrafiteAstPp.pp_statement
-    ~map_unicode_to_tex:(Helm_registry.get_bool
-      "matita.paste_unicode_as_tex")
-    ~term_pp:CicNotationPp.pp_term
-    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
-
-(** {2 Initialization} *)
+let slash_n_RE = Pcre.regexp "\\n" ;;
 
-let grafite_status = (ref None : GrafiteTypes.status option ref)
-let lexicon_status = (ref None : LexiconEngine.status option ref)
-
-let run_script is eval_function  =
-  let lexicon_status',grafite_status' = 
-    match !lexicon_status,!grafite_status with
-    | Some ss, Some s -> ss,s
-    | _,_ -> assert false
-  in
-  let slash_n_RE = Pcre.regexp "\\n" in
-  let cb = 
-    if Helm_registry.get_int "matita.verbosity" < 1 then 
-      (fun _ _ -> ())
-    else 
-      (fun grafite_status stm ->
-        (* dump_status grafite_status; *)
-        let stm = pp_ast_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
-        HLog.debug ("Executing: ``" ^ stm ^ "''"))
+let pp_ast_statement grafite_status stm =
+  let stm = GrafiteAstPp.pp_statement
+    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+    ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj
+    CicNotationPp.pp_term) stm
   in
-  let matita_debug = Helm_registry.get_bool "matita.debug" in
-  try
-   match eval_function lexicon_status' grafite_status' is cb with
-      [] -> raise End_of_file
-    | ((grafite_status'',lexicon_status''),None)::_ ->
-       lexicon_status := Some lexicon_status'';
-       grafite_status := Some grafite_status''
-    | (s,Some _)::_ -> raise AttemptToInsertAnAlias
-  with
-  | GrafiteEngine.Drop  
-  | End_of_file
-  | CicNotationParser.Parse_error _ 
-  | GrafiteEngine.Macro _ as exn -> raise exn
-  | exn -> 
-      if not matita_debug then
-       HLog.error (snd (MatitaExcPp.to_string exn)) ;
-      raise exn
-
-let fname () =
-  let rec aux = function
-  | ""::tl -> aux tl
-  | [x] -> x
-  | [] -> MatitaInit.die_usage ()
-  | l -> 
-      prerr_endline 
-        ("Wrong commands: " ^ 
-          String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
-      MatitaInit.die_usage ()
+  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
-  aux (Helm_registry.get_list Helm_registry.string "matita.args")
+    HLog.debug ("Executing: ``" ^ stm ^ "''")
+;;
 
-let pp_ocaml_mode () = 
-  HLog.message "";
-  HLog.message "                      ** Entering Ocaml mode ** ";
-  HLog.message "";
-  HLog.message "Type 'go ();;' to enter an interactive matitac";
-  HLog.message ""
-  
-let clean_exit n =
- let opt_exit =
-  function
-     None -> ()
-   | Some n -> exit n
- in
-  match !grafite_status with
-     None -> opt_exit n
-   | Some grafite_status ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
-       LibraryClean.clean_baseuris ~verbose:false [baseuri];
-       opt_exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       opt_exit n
+let clean_exit baseuri rc =
+  LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
+;;
 
 let get_macro_context = function
    | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
@@ -132,312 +62,228 @@ let get_macro_context = function
       let goal = Continuationals.Stack.find_goal stack in
       GrafiteTypes.get_proof_context status goal
    | None                       -> assert false
+;;
    
-let rec interactive_loop () = 
-  let str = Ulexing.from_utf8_channel stdin in
-  try
-    run_script str 
-      (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true
-      ~include_paths:(Helm_registry.get_list Helm_registry.string
-        "matita.includes"))
-  with 
-  | GrafiteEngine.Drop -> pp_ocaml_mode ()
-  | GrafiteEngine.Macro (floc, f) ->
-      begin match f (get_macro_context !grafite_status) with 
-       | _, GrafiteAst.Inline (_, style, suri, prefix) ->
-         let str =
-          ApplyTransformation.txt_of_inline_macro style suri prefix
-           ~map_unicode_to_tex:(Helm_registry.get_bool
-             "matita.paste_unicode_as_tex")
-         in
-          !out str;
-         interactive_loop ()
-       | _ ->
-         let x, y = HExtlib.loc_of_floc floc in
-         HLog.error (sprintf "A macro has been found in a script at %d-%d" x y);
-         interactive_loop ()
-      end
-  | Sys.Break -> HLog.error "user break!"; interactive_loop ()
-  | GrafiteTypes.Command_error _ -> interactive_loop ()
-  | End_of_file ->
-     print_newline ();
-     clean_exit (Some 0)
-  | 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);
-      interactive_loop ()
-  | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
-
-let go () =
-  Helm_registry.load_from BuildTimeConf.matita_conf;
-  Http_getter.init ();
-  MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-  LibraryDb.create_owner_environment ();
-  CicEnvironment.set_trust (* environment trust *)
-    (let trust =
-      Helm_registry.get_opt_default Helm_registry.get_bool
-        ~default:true "matita.environment_trust" in
-     fun _ -> trust);
-  let include_paths =
-   Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := Some (GrafiteSync.init ());
-  lexicon_status :=
-   Some (CicNotation2.load_notation ~include_paths
-    BuildTimeConf.core_notation_script);
-  Sys.catch_break true;
-  interactive_loop ()
-
-let pp_times fname bench_mode rc big_bang = 
-  if bench_mode then
-    begin
-      let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
-      let r = Unix.gettimeofday () -. big_bang in
-      let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
-      let cc = 
-        if Str.string_match (Str.regexp ".*opt$") Sys.argv.(0) 0 then 
-          "matitac.opt" 
-        else 
-          "matitac" 
-      in
-      let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
-      let times = 
-        let fmt t = 
-          let seconds = int_of_float t in
-          let cents = int_of_float ((t -. floor t) *. 100.0) in
-          let minutes = seconds / 60 in
-          let seconds = seconds mod 60 in
-          Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
-        in
-        Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
+let pp_times fname rc big_bang = 
+  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 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
+    let times = 
+      let fmt t = 
+        let seconds = int_of_float t in
+        let cents = int_of_float ((t -. floor t) *. 100.0) in
+        let minutes = seconds / 60 in
+        let seconds = seconds mod 60 in
+        Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
       in
-      let fname = 
-        match MatitamakeLib.development_for_dir (Filename.dirname fname) with
-        | None -> fname
-        | Some d -> 
-            let rootlen = String.length(MatitamakeLib.root_for_development d)in
-            let fnamelen = String.length fname in
-            assert (fnamelen > rootlen); 
-            String.sub fname rootlen (fnamelen - rootlen)           
-      in
-      let fname = 
-        if fname.[0] = '/' then
-          String.sub fname 1 (String.length fname - 1)
-        else
-          fname
-      in
-      let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
-      print_endline s;
-      flush stdout
-    end
+      Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
+    in
+    let s = Printf.sprintf "%-4s %s %s" rc times extra in
+    print_endline s;
+    flush stdout;
+    HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
 ;;
 
-let rec compiler_loop fname big_bang mode buf =
- let include_paths =
-  Helm_registry.get_list Helm_registry.string "matita.includes" in
- let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in    
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let bench_mode =  Helm_registry.get_bool "matita.bench" in
- try
-  run_script buf 
-   (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
-    ~clean_baseuri)
- with 
-  | End_of_file -> ()
-  | Sys.Break as exn ->
-     if matita_debug then raise exn;
-      HLog.error "user break!";
-      pp_times fname bench_mode false big_bang;
-      if mode = `COMPILER then
-        clean_exit (Some ~-1)
-      else
-        pp_ocaml_mode ()
-  | GrafiteEngine.Drop ->
-      if mode = `COMPILER then 
-        begin
-          pp_times fname bench_mode false big_bang;
-          clean_exit (Some 1)
-        end
-      else 
-        pp_ocaml_mode ()
-  | GrafiteEngine.Macro (floc, f) ->
-      begin match f (get_macro_context !grafite_status) with 
-       | _, GrafiteAst.Inline (_, style, suri, prefix) ->
-         let str =
-          ApplyTransformation.txt_of_inline_macro style suri prefix
-           ~map_unicode_to_tex:(Helm_registry.get_bool
-             "matita.paste_unicode_as_tex") in
-         !out str;
-         compiler_loop fname big_bang mode buf
-       | _ ->
-         let x, y = HExtlib.loc_of_floc floc in
-         HLog.error (sprintf "A macro has been found in a script at %d-%d" x y);
-         if mode = `COMPILER then
-           begin 
-              pp_times fname bench_mode false big_bang;
-              clean_exit (Some 1)
-            end 
-        else 
-            pp_ocaml_mode ()
-      end
-  | 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);
-     if mode = `COMPILER then
-       begin
-         pp_times fname bench_mode false big_bang;
-         clean_exit (Some 1)
-       end
-     else
-       pp_ocaml_mode ()
-  | exn ->
-      if matita_debug then raise exn;
-      if mode = `COMPILER then 
-        begin
-          pp_times fname bench_mode false big_bang;
-          clean_exit (Some 3)
-        end
-      else 
-        pp_ocaml_mode ()
+let cut prefix s = 
+  let lenp = String.length prefix in
+  let lens = String.length s in
+  assert (lens > lenp);
+  assert (String.sub s 0 lenp = prefix);
+  String.sub s lenp (lens-lenp)
+;;
 
-exception ReadOnlyUri of string
+let get_include_paths options =
+  let include_paths = 
+    try List.assoc "include_paths" options with Not_found -> "" 
+  in
+  let include_paths = Str.split (Str.regexp " ") include_paths in
+  let include_paths = 
+    include_paths @ 
+    Helm_registry.get_list Helm_registry.string "matita.includes" 
+  in
+    include_paths
+;;
 
-let main ~mode = 
-  let big_bang = Unix.gettimeofday () in
-  MatitaInit.initialize_all ();
-  (* must be called after init since args are set by cmdline parsing *)
-  let fname = fname () in
-  if false then
-   (let baseuri =
-    (* This does not work yet :-(
-       let baseuri =
-        GrafiteTypes.get_string_option
-        (match !grafite_status with None -> assert false | Some s -> s)
-        "baseuri" in*)
-    lazy
-      (let _root, buri, _fname = Librarian.baseuri_of_script ~include_paths:[] fname in
-      buri)
-   in
-   let mangled_baseuri =
-    lazy
-     ( let baseuri = Lazy.force baseuri in
-       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 =
-    lazy
-     (open_out
-       (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in
-    LibrarySync.set_object_declaration_hook
-     (fun _ obj ->
-       output_string (Lazy.force f)
-        (CicExportation.ppobj (Lazy.force baseuri) obj);
-       flush (Lazy.force f)));
-  let system_mode =  Helm_registry.get_bool "matita.system" in
-  let bench_mode =  Helm_registry.get_bool "matita.bench" in
-  if bench_mode then
-    Helm_registry.set_int "matita.verbosity" 0;
-  let include_paths =
-   Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := Some (GrafiteSync.init ());
-  lexicon_status :=
-   Some (CicNotation2.load_notation ~include_paths
-    BuildTimeConf.core_notation_script);
-  Sys.catch_break true;
-  let origcb = HLog.get_log_callback () in
-  let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
-  let newcb tag s =
-    match tag with
-    | `Debug | `Message -> ()
-    | `Warning | `Error -> origcb tag s
+let rec compile 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
+  let lexicon_status = 
+    CicNotation2.load_notation ~include_paths:[]
+      BuildTimeConf.core_notation_script 
   in
-  if Helm_registry.get_int "matita.verbosity" < 1 then
-    HLog.set_log_callback newcb;
-  if bench_mode then MatitaMisc.shutup ();
-  let ich, fname, baseuri = 
-    if fname = "stdin" || fname = "-" then
-      let fname = "/dev/fd/0" in
-      let _,baseuri,fname =
-        Librarian.baseuri_of_script ~include_paths:[] fname
+  let initial_lexicon_status = lexicon_status in
+  let big_bang = Unix.gettimeofday () in
+  let time = Unix.time () in
+  try
+    (* sanity checks *)
+    let moo_fname = 
+     LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
+    in
+    let lexicon_fname= 
+     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 <> []) 
+      then begin
+      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 = 
+        if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt"
+        else "matitac" 
       in
-        stdin, fname, baseuri
+      let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
+      print_string s; flush stdout);
+    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 =
+      match
+       MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
+        lexicon_status grafite_status buf print_cb
+      with
+      | [] -> raise End_of_file
+      | ((grafite,lexicon),None)::_ -> grafite, lexicon
+      | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
+    in
+    let elapsed = Unix.time () -. time in
+    let proof_status,moo_content_rev,lexicon_content_rev = 
+      grafite_status.proof_status, grafite_status.moo_content_rev, 
+       lexicon_status.LexiconEngine.lexicon_content_rev
+    in
+    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;
+     LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
+     clean_exit baseuri false)
     else
-      let _,baseuri,fname = 
-        Librarian.baseuri_of_script ~include_paths fname 
-      in
-        open_in fname, fname, baseuri
-  in
-              (* PUT THIS IN A FUNCTION *)
-        if Http_getter_storage.is_read_only baseuri then begin
-          HLog.error (Printf.sprintf "uri %s belongs to a read-only repository"
-          baseuri);
-          raise (ReadOnlyUri baseuri)
-        end;
-        if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
-            LibraryClean.db_uris_of_baseuri baseuri <> [])
-          then begin
-          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;
-        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")));
-              (* PUT THIS IN A FUNCTION *)
-  let time = Unix.time () in
-  if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then
-    origcb `Message ("compiling " ^ 
-    Filename.basename fname ^ " in " ^ baseuri ^ " ...")
-  else
-    HLog.message (sprintf "execution of %s started in %s:" 
-      (Filename.basename fname) baseuri);
-  let buf = Ulexing.from_utf8_channel ich in
-  compiler_loop fname big_bang mode buf;
-  let elapsed = Unix.time () -. time in
-  let tm = Unix.gmtime elapsed in
-  let sec = string_of_int tm.Unix.tm_sec ^ "''" 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,lexicon_content_rev = 
-    match !lexicon_status,!grafite_status with
-    | Some ss, Some s ->
-       s.proof_status, s.moo_content_rev, 
-        ss.LexiconEngine.lexicon_content_rev
-    | _,_ -> assert false
-  in
-  if proof_status <> GrafiteTypes.No_proof then
-   begin
-    HLog.error
-     "there are still incomplete proofs at the end of the script";
-    pp_times fname bench_mode true big_bang;
-    clean_exit (Some 2)
-   end
-  else
-   begin
-     let moo_fname = 
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true 
-     in
-     let lexicon_fname= 
-       LibraryMisc.lexicon_file_of_baseuri 
-        ~must_exist:false ~baseuri ~writable:true 
-     in
-     (* FG: we do not generate .moo when dumping .mma files *)
-     if Helm_registry.get_bool "matita.moo" then begin
+     (if Helm_registry.get_bool "matita.moo" then begin
+        (* FG: we do not generate .moo when dumping .mma files *)
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
      end;
+     let tm = Unix.gmtime elapsed in
+     let sec = string_of_int tm.Unix.tm_sec ^ "''" 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
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
-     pp_times fname bench_mode true big_bang;
-     exit 0
-   end
+     pp_times fname true big_bang;
+     LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
+     true)
+  with 
+  | End_of_file -> 
+      HLog.error "End_of_file"; 
+      pp_times fname false big_bang;
+      clean_exit baseuri false
+  | AttemptToInsertAnAlias lexicon_status -> 
+      pp_times fname false big_bang;
+      LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
+      clean_exit baseuri false
+  | Sys.Break as exn ->
+     if matita_debug then raise exn; 
+     HLog.error "user break!";
+     pp_times fname false big_bang;
+     clean_exit baseuri false
+  | GrafiteEngine.Macro (floc, f) ->
+      (try
+        match f (get_macro_context (Some grafite_status)) with 
+        | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+          let str =
+           ApplyTransformation.txt_of_inline_macro style suri prefix
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex") in
+          !out str;
+          compile options fname 
+        | _ ->
+          let x, y = HExtlib.loc_of_floc floc in
+          HLog.error (sprintf "A macro has been found at %d-%d" x y);
+          pp_times fname false big_bang;
+          clean_exit baseuri false
+      with exn -> 
+        HLog.error (snd (MatitaExcPp.to_string exn)); 
+        pp_times fname false big_bang;
+        clean_exit baseuri false)
+  | 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);
+      pp_times fname false big_bang;
+      clean_exit baseuri false
+  | exn ->
+       if matita_debug then raise exn; 
+       HLog.error (snd (MatitaExcPp.to_string exn));
+       pp_times fname false big_bang;
+       clean_exit baseuri false
+;;
+
+module F = 
+  struct 
+    type source_object = string
+    type target_object = string
+    let string_of_source_object s = s;;
+    let string_of_target_object s = s;;
+
+    let root_of opts s = 
+      try
+        let include_paths = get_include_paths opts in
+        let root,_,_,_ = Librarian.baseuri_of_script ~include_paths s in
+        Some root
+      with Librarian.NoRootFor x -> None
+    ;;
+
+    let target_of opts mafile = 
+      let include_paths = get_include_paths opts in
+      let _,baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mafile in
+      LibraryMisc.obj_file_of_baseuri 
+        ~must_exist:false ~baseuri ~writable:true 
+    ;;
+
+    let mtime_of_source_object s =
+      try Some (Unix.stat s).Unix.st_mtime
+      with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> 
+              None
+(*         max_float *)
+(*         raise (Failure ("Unable to stat a source file: " ^ s))  *)
+    ;;
+
+    let mtime_of_target_object s =
+      try Some (Unix.stat s).Unix.st_mtime
+      with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+    ;;
+
+    let build = compile;;
+
+    let load_deps_file = Librarian.load_deps_file;;
+
+  end 
+
+module Make = Librarian.Make(F) 
+