From d6eeb40f4796a582934c3d0b6a4dd5ae6f3b768f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 16:43:25 +0000 Subject: [PATCH] - bug fixed: circular dependencies are now detected correctly --- matita/matita/matitaEngine.ml | 32 ++++++++++++++++++-------------- matita/matita/matitaEngine.mli | 1 + matita/matita/matitaExcPp.ml | 6 ++++-- 3 files changed, 23 insertions(+), 16 deletions(-) diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index b04a06672..1efaeff24 100644 --- 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 6af367614..768ff7080 100644 --- 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 ac1c23997..5ecea5dc8 100644 --- 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) -> -- 2.39.2