1. bug fixed: in the last commit on NCicLibrary we forgot that

   get_already_included must be transitively closed; fixed and changed
   the function name
2. added a cache to assert_ng (called ~asserted) to avoid re-asserting
   the same file twice during a single include command

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 2acf844b0f21a39707d217d939636f8e1130d142..4ccf56653461877e85170d95e2ddb629f9fb1f4e 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -471,12 +471,13 @@ let compute_relevance uri =
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.Include (loc, mode, fname) ->
-          let _root, baseuri, _fullpath, _rrelpath = 
+          let _root, baseuri, fullpath, _rrelpath = 
        Librarian.baseuri_of_script ~include_paths fname in
      let baseuri = NUri.uri_of_string baseuri in
      (* MATITA 1.0: keep WithoutPreferences? *)
      let alias_only = (mode = GrafiteAst.OnlyPreferences) in
-      GrafiteTypes.Serializer.require ~alias_only ~baseuri ~fname status
+      GrafiteTypes.Serializer.require
+       ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
      let status, composites =

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 65e0cd60e0637d13b5f099bc7e466d89692c4963..edfb7db66782001b7efa68b2d2c253bff59e8a8f 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -158,7 +158,7 @@ let time_travel status =
 ;;
 
 type obj = string * Obj.t
-(* CSC: includes & dependencies to be unified! *)
+(* includes are transitively closed; dependencies are only immediate *)
 type dump =
  { objs: obj list ; includes: NUri.uri list; dependencies: string list }
 
@@ -177,7 +177,7 @@ class dumpable_status =
    = fun o -> {< db = o#dump >}
  end
 
-let get_already_included status =
+let get_transitively_included status =
  status#dump.includes
 ;;
 
@@ -253,15 +253,14 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    List.iter (fun u -> add_deps u [baseuri]) status#dump.includes;
    time_travel (new status)
 
-  let require2 ~baseuri ~fname ~alias_only status =
+  let require2 ~baseuri ~alias_only status =
    try
     let s = D.get status in
     let status =
-      D.set status
-       (s#set_dump
-         {s#dump with
-           includes = baseuri::s#dump.includes;
-           dependencies = fname::s#dump.dependencies}) in
+     D.set status
+      (s#set_dump
+        {s#dump with
+        includes = baseuri::s#dump.includes}) in
     let _dependencies,dump = require0 ~baseuri in
      List.fold_right (!require1 ~alias_only) dump status
    with
@@ -274,16 +273,29 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
    ~refresh_uri_in_reference:_ ~alias_only status =
      let alias_only =
-      alias_only || List.mem baseuri (get_already_included (D.get status))
+      alias_only || List.mem baseuri (get_transitively_included (D.get status))
      in
-      require2 ~baseuri ~fname ~alias_only status
+      HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname);
+      let status = require2 ~baseuri ~alias_only status in
+      HLog.warn ("done: include " ^ (if alias_only then "alias " else "") ^ fname);
+      status
    in
     register#run "include" aux
 
   let require ~baseuri ~fname ~alias_only status =
    let alias_only =
-    alias_only || List.mem baseuri (get_already_included (D.get status)) in
-   let status = require2 ~baseuri ~fname ~alias_only status in
+    alias_only || List.mem baseuri (get_transitively_included (D.get status)) in
+   let status =
+    if not alias_only then
+     let s = D.get status in
+      D.set status
+       (s#set_dump
+         {s#dump with
+           includes = baseuri::s#dump.includes;
+           dependencies = fname::s#dump.dependencies})
+    else
+     status in
+   let status = require2 ~baseuri ~alias_only status in
    let s = D.get status in
     D.set status
      (s#set_dump

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index 14a0685b4a6a74633a13e8abc7cb093e89fc8887..c65ee1df1d8b8a831347aedd9558b7b4e85eea9f 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -50,7 +50,7 @@ class dumpable_status :
   method set_dumpable_status: #g_dumpable_status -> 'self
  end
 
-val get_already_included: #dumpable_status -> NUri.uri list
+val get_transitively_included: #dumpable_status -> NUri.uri list
 val dump_obj: #dumpable_status as 'status -> obj -> 'status
 
 module type SerializerType =

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 6c8a033e46f733dceb377f277902713930fc6855..64b3cc1ebbc0d8a19407bcceb5fbce7f6034c60f 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -153,27 +153,30 @@ let baseuri_of_script ~include_paths fname =
     raise (Failure ("File not found: "^fname))
 ;;
 
-let rec get_ast status ~compiling ~include_paths strm = 
+let rec get_ast status ~compiling ~asserted ~include_paths strm = 
   match GrafiteParser.parse_statement status strm with
      (GrafiteAst.Executable
        (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
      ->
-       let already_included = NCicLibrary.get_already_included status in
-       ignore(assert_ng ~already_included ~compiling ~include_paths mafilename);
-       cmd
-   | cmd -> cmd
+       let already_included = NCicLibrary.get_transitively_included status in
+       let asserted,_ =
+        assert_ng ~already_included ~compiling ~asserted ~include_paths
+         mafilename
+       in
+        asserted,cmd
+   | cmd -> asserted,cmd
 
-and eval_from_stream ~compiling ~include_paths ?do_heavy_checks status str cb =
+and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop status =
-  let stop,status = 
+ let rec loop asserted status =
+  let asserted,stop,status = 
    try
      let cont =
-       try Some (get_ast status ~compiling ~include_paths str)
+       try Some (get_ast status ~compiling ~asserted ~include_paths str)
        with End_of_file -> None in
      match cont with
-     | None -> true, status
-     | Some ast ->
+     | None -> asserted, true, status
+     | Some (asserted,ast) ->
         cb status ast;
         let new_statuses =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
@@ -184,15 +187,15 @@ and eval_from_stream ~compiling ~include_paths ?do_heavy_checks status str cb =
                 raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
           | _ -> assert false
         in
-         false, status
+         asserted, false, status
    with exn when not matita_debug ->
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then status else loop status
+  if stop then asserted,status else loop asserted status
  in
-  loop status
+  loop asserted status
 
-and compile ~compiling ~include_paths fname =
+and compile ~compiling ~asserted ~include_paths fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
@@ -242,8 +245,8 @@ and compile ~compiling ~include_paths fname =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement
     in
-    let grafite_status =
-     eval_from_stream ~compiling ~include_paths grafite_status buf print_cb in
+    let asserted, grafite_status =
+     eval_from_stream ~compiling ~asserted ~include_paths grafite_status buf print_cb in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
@@ -259,7 +262,8 @@ and compile ~compiling ~include_paths fname =
      in
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
-     pp_times fname true big_bang big_bang_u big_bang_s
+     pp_times fname true big_bang big_bang_u big_bang_s;
+     asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
@@ -273,46 +277,58 @@ and compile ~compiling ~include_paths fname =
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-and assert_ng ~already_included ~compiling ~include_paths mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
  let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath 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 to_be_compiled =
-  match ngtime with
-     Some ngtime ->
-      let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
-      let children_bad =
-       List.exists
-        (fun mapath ->
-             assert_ng ~already_included ~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
- in
-  if not to_be_compiled then false
-  else
-   if List.mem baseuri already_included then
-     (* maybe recompiling it I would get the same... *)
-     raise (AlreadyLoaded (lazy mapath))
-   else
-    (compile ~compiling ~include_paths fullmapath; true)
+ if List.mem fullmapath asserted then asserted,false
+ else
+  begin
+   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 =
+              assert_ng ~already_included ~compiling ~asserted ~include_paths
+               mapath
+            in
+             asserted, b || b1
+              || 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)
+          ) (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
 ;;
 
-let assert_ng = assert_ng ~already_included:[] ~compiling:[]
-let get_ast = get_ast ~compiling:[]
+let assert_ng ~include_paths mapath =
+ snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
+  mapath)
+let get_ast status ~include_paths strm =
+ snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)