- bug fixed: circular dependencies are now detected correctly

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index b04a0667232f5bf80dd94ca4ffce09e018d2b9a1..1efaeff24834ce7b09cdbd3f1eb619d0ece0a270 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -33,6 +33,7 @@ exception TryingToAdd of string Lazy.t
 exception EnrichedWithStatus of exn * GrafiteTypes.status
 exception AlreadyLoaded of string Lazy.t
 exception FailureCompiling of string * exn
+exception CircularDependency of string
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -89,11 +90,6 @@ let cut prefix s =
   String.sub s lenp (lens-lenp)
 ;;
 
-(*MATITA 1.0 assert false;; (* chiamare enrich_include_paths *)*)
-let enrich_include_paths ~include_paths =
- include_paths @ Helm_registry.get_list Helm_registry.string "matita.includes" 
-;;
-
 let activate_extraction baseuri fname =
   ()
   (* MATITA 1.0
@@ -166,7 +162,7 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
   (new_status,None)::intermediate_states
 ;;
 
-let rec get_ast status ~include_paths strm = 
+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
@@ -178,17 +174,17 @@ let rec get_ast status ~include_paths strm =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-       ignore (assert_ng ~include_paths ~root tgt);
+       ignore (assert_ng ~compiling ~include_paths ~root tgt);
        cmd
    | cmd -> cmd
 
-and eval_from_stream ~include_paths ?do_heavy_checks status str cb =
+and eval_from_stream ~compiling ~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 = 
    try
      let cont =
-       try Some (get_ast status ~include_paths str)
+       try Some (get_ast status ~compiling ~include_paths str)
        with End_of_file -> None in
      match cont with
      | None -> true, status
@@ -211,7 +207,9 @@ and eval_from_stream ~include_paths ?do_heavy_checks status str cb =
  in
   loop status
 
-and compile ~include_paths fname =
+and compile ~compiling ~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
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
@@ -257,7 +255,7 @@ and compile ~include_paths fname =
       else pp_ast_statement
     in
     let grafite_status =
-     eval_from_stream ~include_paths grafite_status buf print_cb in
+     eval_from_stream ~compiling ~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)
@@ -289,7 +287,7 @@ and compile ~include_paths fname =
 
 (* BIG BUG: if a file recursively includes itself, anything can happen,
  * from divergence to inclusion of an old copy of itself *)
-and assert_ng ~include_paths ~root mapath =
+and assert_ng ~compiling ~include_paths ~root mapath =
  let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
  assert (root=root');
  let baseuri = NUri.uri_of_string baseuri in
@@ -306,7 +304,9 @@ and assert_ng ~include_paths ~root mapath =
   match ngtime with
      Some ngtime ->
       let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
-      let children_bad= List.exists (assert_ng ~include_paths ~root) preamble in
+      let children_bad =
+       List.exists (assert_ng ~compiling ~include_paths ~root) preamble
+      in
        children_bad || matime > ngtime
    | None -> true
  in
@@ -317,4 +317,8 @@ and assert_ng ~include_paths ~root mapath =
      (* maybe recompiling it I would get the same... *)
      raise (AlreadyLoaded (lazy mapath))
    else
-    (compile ~include_paths mapath; true)
+    (compile ~compiling ~include_paths mapath; true)
+;;
+
+let assert_ng = assert_ng ~compiling:[]
+let get_ast = get_ast ~compiling:[]

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 6af367614abf9a6a383a2d3ac2da50a5de5046c9..768ff7080ee323f50a5f8cdb977fe92579e9995e 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -27,6 +27,7 @@ exception TryingToAdd of string Lazy.t
 exception EnrichedWithStatus of exn * GrafiteTypes.status
 exception AlreadyLoaded of string Lazy.t
 exception FailureCompiling of string * exn
+exception CircularDependency of string
 
 val get_ast:
   GrafiteTypes.status -> include_paths:string list -> Ulexing.lexbuf ->

diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml
index ac1c23997b4b6166b908467a0ddf7a9a20d2ec08..5ecea5dc85af80a7058da057170fc92f53f01c47 100644 (file)
--- a/matita/matita/matitaExcPp.ml
+++ b/matita/matita/matitaExcPp.ml
@@ -147,13 +147,15 @@ let rec to_string =
      None, "NCicEnvironment object not found: " ^ Lazy.force msg
   | NCicEnvironment.AlreadyDefined msg ->
      None, "NCicEnvironment already defined: " ^ Lazy.force msg
+  | MatitaEngine.CircularDependency fname ->
+      None, "Circular dependency including " ^ fname
   | MatitaEngine.TryingToAdd msg ->
      None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg
   | MatitaEngine.AlreadyLoaded msg ->
      None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is
      already loaded; undo the inclusion and try again."
   | MatitaEngine.FailureCompiling (filename,exn) ->
-     None, "Compiling " ^ filename ^ ": " ^ snd (to_string exn)
+     None, "Compiling " ^ filename ^ ":\n" ^ snd (to_string exn)
   | NCicRefiner.AssertFailure msg ->
      None, "NRefiner assert failure: " ^ Lazy.force msg
   | NCicEnvironment.BadDependency (msg,e) ->
@@ -168,7 +170,7 @@ let rec to_string =
   | DisambiguateChoices.Choice_not_found msg ->
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
   | MatitaEngine.EnrichedWithStatus (exn,_) ->
-     None, "EnrichedWithStatus "^snd(to_string exn)
+     None, snd(to_string exn)
   | NTacStatus.Error (msg,None) ->
      None, "NTactic error: " ^ Lazy.force msg 
   | NTacStatus.Error (msg,Some exn) ->