- Some root, relpath, obj_writeable, obj_read_only
- with Librarian.NoRootFor x -> None, "", "", ""
- ;;
-
- 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
- ;;
-
- 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
- ;;
-
-(* 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 opts fname =
- try
- (* MATITA 1.0: c'erano le push/pop per il parser; ma per
- * l'environment nuovo? *)
- compile opts fname
- with
- | Sys.Break -> false
- | exn when not matita_debug ->
- HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
- assert false
- in
- compact (compile options fname)
- ;;
-
- let load_deps_file = Librarian.load_deps_file;;
-
- end
-
-module Make = Librarian.Make(F)
-
-(* FINE EX MATITACLIB *)
-
-
-
-(* this function calls the parser in a way that it does not perform inclusions,
- * so that we can ensure the inclusion is performed after the included file
- * is compiled (if needed). matitac does not need that, since it compiles files
- * in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths f x =
- match f x with
- (GrafiteAst.Executable
- (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
- ->
- let root, buri, _, tgt =
- try Librarian.baseuri_of_script ~include_paths mafilename
- with Librarian.NoRootFor _ ->
- HLog.error ("The included file '"^mafilename^"' has no root file,");
- HLog.error "please create it.";
- raise (Failure ("No root file for "^mafilename))
- in
- if Make.make root [tgt] then
- cmd
- else raise (Failure ("Compiling: " ^ tgt))
- | cmd -> cmd
+ asserted, children_bad || matime > ngtime
+ | None -> asserted,true
+ in
+ if not to_be_compiled then fullmapath::asserted,false
+ else
+ if List.mem baseuri already_included then
+ (* maybe recompiling it I would get the same... *)
+ raise (AlreadyLoaded (lazy mapath))
+ else
+ let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+ fullmapath::asserted,true
+ end