-(* BIG BUG: if a file recursively includes itself, anything can happen,
- * from divergence to inclusion of an old copy of itself *)
-and assert_ng ~compiling ~include_paths ~root mapath =
- let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
- assert (root=root');
- let baseuri = NUri.uri_of_string baseuri in
- let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
- let ngtime =
- try
- Some (Unix.stat ngpath).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
- let matime =
- try (Unix.stat fullmapath).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
- in
- let to_be_compiled =
- match ngtime with
- Some ngtime ->
- let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
- let children_bad =
- List.exists (assert_ng ~compiling ~include_paths ~root) preamble
- in
- children_bad || matime > ngtime
- | None -> true
- in
- if not to_be_compiled then false
- else
- (* MATITA 1.0: SHOULD TAKE THIS FROM THE STATUS *)
- if List.mem baseuri (NCicLibrary.get_already_included ()) then
- (* maybe recompiling it I would get the same... *)
- raise (AlreadyLoaded (lazy mapath))
- else
- (compile ~compiling ~include_paths fullmapath; true)
+and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
+ let root,baseuri,fullmapath,_ =
+ Librarian.baseuri_of_script ~include_paths mapath in
+ if List.mem fullmapath asserted then asserted,false
+ else
+ begin
+ let include_paths =
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ root::includes @
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let baseuri = NUri.uri_of_string baseuri in
+ let ngtime_of baseuri =
+ let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ try
+ Some (Unix.stat ngpath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
+ let matime =
+ try (Unix.stat fullmapath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
+ in
+ let ngtime = ngtime_of baseuri in
+ let asserted,to_be_compiled =
+ match ngtime with
+ Some ngtime ->
+ let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let asserted,children_bad =
+ List.fold_left
+ (fun (asserted,b) mapath ->
+ let asserted,b1 =
+ try
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mapath
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ asserted, true
+ in
+ asserted, b || b1
+ || let _,baseuri,_,_ =
+ (*CSC: bug here? include_paths should be empty and
+ mapath should be absolute *)
+ Librarian.baseuri_of_script ~include_paths mapath in
+ let baseuri = NUri.uri_of_string baseuri in
+ (match ngtime_of baseuri with
+ Some child_ngtime -> child_ngtime > ngtime
+ | None -> assert false)
+ ) (asserted,false) preamble
+ in
+ 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