Some bugs fixed (and some still open) in recursive compilation of files:

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 1efaeff24834ce7b09cdbd3f1eb619d0ece0a270..c6f4359759d4818baf48e51b0c86827c83aa9042 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -162,19 +162,23 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
   (new_status,None)::intermediate_states
 ;;
 
+let baseuri_of_script ~include_paths fname =
+ try Librarian.baseuri_of_script ~include_paths fname
+ with
+   Librarian.NoRootFor _ -> 
+    HLog.error ("The included file '"^fname^"' has no root file,");
+    HLog.error "please create it.";
+    raise (Failure ("No root file for "^fname))
+  | Librarian.FileNotFound _ -> 
+    raise (Failure ("File not found: "^fname))
+;;
+
 let rec get_ast status ~compiling ~include_paths strm = 
   match GrafiteParser.parse_statement status strm 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
-       ignore (assert_ng ~compiling ~include_paths ~root tgt);
+       ignore (assert_ng ~compiling ~include_paths mafilename);
        cmd
    | cmd -> cmd
 
@@ -249,7 +253,10 @@ and compile ~compiling ~include_paths fname =
         (Filename.dirname 
           (Http_getter.filename ~local:true ~writable:true (baseuri ^
           "foo.con")));
-    let buf = Ulexing.from_utf8_channel (open_in fname) in
+    let buf =
+     GrafiteParser.parsable_statement grafite_status
+      (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
@@ -285,27 +292,34 @@ and compile ~compiling ~include_paths fname =
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-(* 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,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
- assert (root=root');
+and assert_ng ~compiling ~include_paths mapath =
+ let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  let baseuri = NUri.uri_of_string baseuri in
- let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
- let ngtime =
+ 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 mapath).Unix.st_mtime
-  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false
+  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 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
+       List.exists
+        (fun mapath ->
+             assert_ng ~compiling ~include_paths mapath
+          || let _,baseuri,_,_ =
+               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)
+        ) preamble
       in
        children_bad || matime > ngtime
    | None -> true
@@ -317,7 +331,7 @@ and assert_ng ~compiling ~include_paths ~root mapath =
      (* maybe recompiling it I would get the same... *)
      raise (AlreadyLoaded (lazy mapath))
    else
-    (compile ~compiling ~include_paths mapath; true)
+    (compile ~compiling ~include_paths fullmapath; true)
 ;;
 
 let assert_ng = assert_ng ~compiling:[]