From c9bb60cf6fc39876e2dc7bf40fd650080d0d218f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Dec 2010 12:11:57 +0000 Subject: [PATCH] 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 --- .../grafite_engine/grafiteEngine.ml | 5 +- matita/components/ng_library/nCicLibrary.ml | 36 +++-- matita/components/ng_library/nCicLibrary.mli | 2 +- matita/matita/matitaEngine.ml | 132 ++++++++++-------- 4 files changed, 102 insertions(+), 73 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 2acf844b0..4ccf56653 100644 --- 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 65e0cd60e..edfb7db66 100644 --- 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 14a0685b4..c65ee1df1 100644 --- 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 6c8a033e4..64b3cc1eb 100644 --- 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) -- 2.39.2