diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /library/library.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 646 |
1 files changed, 372 insertions, 274 deletions
diff --git a/library/library.ml b/library/library.ml index 681c55c7..b078e2c4 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,182 +1,62 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names open Libnames open Nameops -open Safe_typing open Libobject open Lib -open Nametab - -(*************************************************************************) -(*s Load path. Mapping from physical to logical paths etc.*) - -type logical_path = dir_path - -let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) - -let get_load_paths () = List.map pi1 !load_paths - -let find_logical_path phys_dir = - let phys_dir = System.canonical_path_name phys_dir in - match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with - | [_,dir,_] -> dir - | [] -> Nameops.default_root_prefix - | l -> anomaly ("Two logical paths are associated to "^phys_dir) - -let is_in_load_paths phys_dir = - let dir = System.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p = fun p -> (String.compare dir p) == 0 in - List.exists check_p lp - -let remove_load_path dir = - load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths - -let add_load_path isroot (phys_path,coq_path) = - let phys_path = System.canonical_path_name phys_path in - match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with - | [_,dir,_] -> - if coq_path <> dir - (* If this is not the default -I . to coqtop *) - && not - (phys_path = System.canonical_path_name Filename.current_dir_name - && coq_path = Nameops.default_root_prefix) - then - begin - (* Assume the user is concerned by library naming *) - if dir <> Nameops.default_root_prefix then - Flags.if_warn msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); - remove_load_path phys_path; - load_paths := (phys_path,coq_path,isroot) :: !load_paths; - end - | [] -> - load_paths := (phys_path,coq_path,isroot) :: !load_paths; - | _ -> anomaly ("Two logical paths are associated to "^phys_path) - -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.map string_of_id (List.rev (repr_dirpath dir))) - -let root_paths_matching_dir_path dir = - let rec aux = function - | [] -> [] - | (p,d,true) :: l when is_dirpath_prefix_of d dir -> - let suffix = drop_dirpath_prefix d dir in - extend_path_with_dirpath p suffix :: aux l - | _ :: l -> aux l in - aux !load_paths - -(* Root p is bound to A.B.C.D and we require file C.D.E.F *) -(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) - -(* Root p is bound to A.B.C.C and we require file C.C.E.F *) -(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) - -let intersections d1 d2 = - let rec aux d1 = - if d1 = empty_dirpath then [d2] else - let rest = aux (snd (chop_dirpath 1 d1)) in - if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest - else rest in - aux d1 - -let loadpaths_matching_dir_path dir = - let rec aux = function - | [] -> [] - | (p,d,true) :: l -> - let inters = intersections d dir in - List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl)) - inters @ - aux l - | (p,d,_) :: l -> - (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in - aux !load_paths - -let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) -type compilation_unit_name = dir_path +type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; - md_compiled : LightenLibrary.lightened_compiled_library; + md_compiled : Safe_typing.compiled_library; md_objects : Declaremods.library_objects; - md_deps : (compilation_unit_name * Digest.t) list; - md_imports : compilation_unit_name list } + md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_imports : compilation_unit_name array } (*s Modules loaded in memory contain the following informations. They are kept in the global table [libraries_table]. *) type library_t = { library_name : compilation_unit_name; - library_compiled : compiled_library; + library_compiled : Safe_typing.compiled_library; library_objects : Declaremods.library_objects; - library_deps : (compilation_unit_name * Digest.t) list; - library_imports : compilation_unit_name list; - library_digest : Digest.t } - -module LibraryOrdered = - struct - type t = dir_path - let compare d1 d2 = - Pervasives.compare - (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) - end + library_deps : (compilation_unit_name * Safe_typing.vodigest) array; + library_imports : compilation_unit_name array; + library_digests : Safe_typing.vodigest; + library_extra_univs : Univ.universe_context_set; +} +module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) -let libraries_table = ref LibraryMap.empty +let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) let libraries_filename_table = ref LibraryFilenameMap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) -let libraries_loaded_list = ref [] -let libraries_imports_list = ref [] -let libraries_exports_list = ref [] - -let freeze () = - !libraries_table, - !libraries_loaded_list, - !libraries_imports_list, - !libraries_exports_list - -let unfreeze (mt,mo,mi,me) = - libraries_table := mt; - libraries_loaded_list := mo; - libraries_imports_list := mi; - libraries_exports_list := me - -let init () = - libraries_table := LibraryMap.empty; - libraries_loaded_list := []; - libraries_imports_list := []; - libraries_exports_list := [] - -let _ = - Summary.declare_summary "MODULES" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" (* various requests to the tables *) @@ -186,7 +66,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (string_of_dirpath dir)) + error ("Unknown library " ^ (DirPath.to_string dir)) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -209,7 +89,7 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> m.library_name = dir) !libraries_imports_list + List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list @@ -221,9 +101,17 @@ let opened_libraries () = be performed first, thus the libraries_loaded_list ... *) let register_loaded_library m = + let link m = + let dirname = Filename.dirname (library_full_filename m.library_name) in + let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in + let f = prefix ^ "cmo" in + let f = Dynlink.adapt_filename f in + if not !Flags.no_native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f + in let rec aux = function - | [] -> [m] - | m'::_ as l when m'.library_name = m.library_name -> l + | [] -> link m; [m] + | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; libraries_table := LibraryMap.add m.library_name m !libraries_table @@ -237,7 +125,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m + | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m let register_open_library export m = @@ -251,14 +139,14 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = m1.library_name = m2.library_name +let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) List.exists (eq_lib_name m) explicit_libs - or not (library_is_opened m.library_name) + || not (library_is_opened m.library_name) then begin register_open_library export m; Declaremods.really_import_module (MPfile m.library_name) @@ -275,7 +163,7 @@ let open_libraries export modl = List.fold_left (fun l m -> let subimport = - List.fold_left + Array.fold_left (fun l m -> remember_last_of_each l (try_find_library m)) l m.library_imports in remember_last_of_each subimport m) @@ -287,7 +175,7 @@ let open_libraries export modl = (* import and export - synchronous operations*) let open_import i (_,(dir,export)) = - if i=1 then + if Int.equal i 1 then (* even if the library is already imported, we re-import it *) (* if not (library_is_opened dir) then *) open_libraries export [try_find_library dir] @@ -300,7 +188,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let in_import : dir_path * bool -> obj = +let in_import : DirPath.t * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -314,7 +202,7 @@ let in_import : dir_path * bool -> obj = (*s Loading from disk to cache (preparation phase) *) let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number ".vo" + System.raw_extern_intern Coq_config.vo_magic_number (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -326,130 +214,233 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = root_paths_matching_dir_path pref in - if loadpath = [] then raise LibUnmappedDir; - try - let name = (string_of_id base)^".vo" in - let _, file = System.where_in_path ~warn:false loadpath name in - (dir, file) - with Not_found -> - (* Last chance, removed from the file system but still in memory *) - if library_is_loaded dir then - (dir, library_full_filename dir) - else - raise LibNotFound + let loadpath = Loadpath.expand_root_path pref in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let find ext = + try + let name = Id.to_string base ^ ext in + let _, file = System.where_in_path ~warn:false loadpath name in + [file] + with Not_found -> [] in + match find ".vo" @ find ".vio" with + | [] -> raise LibNotFound + | [file] -> dir, file + | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + str vo ++ str " because it is more recent"); + dir, vi + | [vo;vi] -> dir, vo + | _ -> assert false let locate_qualified_library warn qid = - try - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = loadpaths_matching_dir_path dir in - if loadpath = [] then raise LibUnmappedDir; - let name = string_of_id base ^ ".vo" in - let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in - (* Look if loaded *) - if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) - (* Otherwise, look for it in the file system *) - else (LibInPath, dir, file) - with Not_found -> raise LibNotFound - -let explain_locate_library_error qid = function - | LibUnmappedDir -> - let prefix, _ = repr_qualid qid in - errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) - | LibNotFound -> - errorlabstrm "load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - | e -> raise e + (* Search library in loadpath *) + let dir, base = repr_qualid qid in + let loadpath = Loadpath.expand_path dir in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let find ext = + try + let name = Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn (List.map fst loadpath) name in + [lpath, file] + with Not_found -> [] in + let lpath, file = + match find ".vo" @ find ".vio" with + | [] -> raise LibNotFound + | [lpath, file] -> lpath, file + | [lpath_vo, vo; lpath_vi, vi] + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + str vo ++ str " because it is more recent"); + lpath_vi, vi + | [lpath_vo, vo; _ ] -> lpath_vo, vo + | _ -> assert false + in + let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in + (* Look if loaded *) + if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir) + (* Otherwise, look for it in the file system *) + else (LibInPath, dir, file) + +let error_unmapped_dir qid = + let prefix, _ = repr_qualid qid in + errorlabstrm "load_absolute_library_from" + (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ + str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) + +let error_lib_not_found qid = + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = try locate_absolute_library dir - with e when Errors.noncritical e -> - explain_locate_library_error (qualid_of_dirpath dir) e + with + | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) + | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) let try_locate_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f + with + | LibUnmappedDir -> error_unmapped_dir qid + | LibNotFound -> error_lib_not_found qid + +(************************************************************************) +(** {6 Tables of opaque proof terms} *) + +(** We now store opaque proof terms apart from the rest of the environment. + See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + we can quickly load a first half of a .vo file without these opaque + terms, and access them only when a specific command (e.g. Print or + Print Assumptions) needs it. *) + +exception Faulty + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) + +let fetch_table what dp (f,pos,digest) = + let dir_path = Names.DirPath.to_string dp in + try + msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let ch = System.with_magic_number_check raw_intern_library f in + let () = seek_in ch pos in + if not (String.equal (System.digest_in f ch) digest) then raise Faulty; + let table, pos', digest' = System.marshal_in_segment f ch in + let () = close_in ch in + let ch' = open_in f in + if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; + let () = close_in ch' in + table with e when Errors.noncritical e -> - explain_locate_library_error qid e + error + ("The file "^f^" (bound to " ^ dir_path ^ + ") is inaccessible or corrupted,\n" ^ + "cannot load some "^what^" in it.\n") + +(** Delayed / available tables of opaque terms *) + +type 'a table_status = + | ToFetch of string * int * Digest.t + | Fetched of 'a Future.computation array + +let opaque_tables = + ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t) +let univ_tables = + ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t) + +let add_opaque_table dp st = + opaque_tables := LibraryMap.add dp st !opaque_tables +let add_univ_table dp st = + univ_tables := LibraryMap.add dp st !univ_tables + +let access_table fetch_table add_table tables dp i = + let t = match LibraryMap.find dp tables with + | Fetched t -> t + | ToFetch (f,pos,digest) -> + let t = fetch_table dp (f,pos,digest) in + add_table dp (Fetched t); + t + in + assert (i < Array.length t); t.(i) + +let access_opaque_table dp i = + access_table + (fetch_table "opaque proofs") + add_opaque_table !opaque_tables dp i +let access_univ_table dp i = + try + Some (access_table + (fetch_table "universe contexts of opaque proofs") + add_univ_table !univ_tables dp i) + with Not_found -> None +let () = + Opaqueproof.set_indirect_opaque_accessor access_opaque_table; + Opaqueproof.set_indirect_univ_accessor access_univ_table (************************************************************************) (* Internalise libraries *) -let mk_library md table digest = - let md_compiled = - LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled - in { +type seg_lib = library_disk +type seg_univ = (* true = vivo, false = vi *) + Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool +type seg_discharge = Opaqueproof.cooking_info list array +type seg_proofs = Term.constr Future.computation array + +let mk_library md digests univs = + { library_name = md.md_name; - library_compiled = md_compiled; + library_compiled = md.md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; library_imports = md.md_imports; - library_digest = digest + library_digests = digests; + library_extra_univs = univs; } -let fetch_opaque_table (f,pos,digest) = - try - let ch = System.with_magic_number_check raw_intern_library f in - seek_in ch pos; - if System.marshal_in f ch <> digest then failwith "File changed!"; - let table = (System.marshal_in f ch : LightenLibrary.table) in - close_in ch; - table - with e when Errors.noncritical e -> - error - ("The file "^f^" is inaccessible or has changed,\n" ^ - "cannot load some opaque constant bodies in it.\n") - let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in - let lmd = System.marshal_in f ch in - let pos = pos_in ch in - let digest = System.marshal_in f ch in - let table = lazy (fetch_opaque_table (f,pos,digest)) in - register_library_filename lmd.md_name f; - let library = mk_library lmd table digest in + let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in + let _ = System.skip_in_segment f ch in + let pos, digest = System.skip_in_segment f ch in close_in ch; - library - -let rec intern_library needed (dir, f) = + register_library_filename lmd.md_name f; + add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); + let open Safe_typing in + match univs with + | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + | Some (utab,uall,true) -> + add_univ_table lmd.md_name (Fetched utab); + mk_library lmd (Dvivo (digest_lmd,digest_u)) uall + | Some (utab,_,false) -> + add_univ_table lmd.md_name (Fetched utab); + mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + +module DPMap = Map.Make(DirPath) + +let deps_to_string deps = + Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps + +let rec intern_library (needed, contents) (dir, f) from = + Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) - try find_library dir, needed + try find_library dir, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) - try List.assoc dir needed, needed + try DPMap.find dir contents, (needed, contents) with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in - if dir <> m.library_name then + if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - m, intern_library_deps needed dir m + Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); + m, intern_library_deps (needed, contents) dir m (Some f) -and intern_library_deps needed dir m = - (dir,m)::List.fold_left (intern_mandatory_library dir) needed m.library_deps +and intern_library_deps libs dir m from = + let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in + (dir :: needed, DPMap.add dir m contents ) -and intern_mandatory_library caller needed (dir,d) = - let m,needed = intern_library needed (try_locate_absolute_library dir) in - if d <> m.library_digest then - errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^ - ".vo makes inconsistent assumptions over library " - ^(string_of_dirpath dir))); - needed +and intern_mandatory_library caller from libs (dir,d) = + let m, libs = intern_library libs (try_locate_absolute_library dir) from in + if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then + errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ + ".vo makes inconsistent assumptions over library " ^ + DirPath.to_string dir)); + libs -let rec_intern_library needed mref = - let _,needed = intern_library needed mref in needed +let rec_intern_library libs mref = + let _, libs = intern_library libs mref None in + libs let check_library_short_name f dir = function - | Some id when id <> snd (split_dirpath dir) -> + | Some id when not (Id.equal id (snd (split_dirpath dir))) -> errorlabstrm "check_library_short_name" (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ @@ -463,18 +454,24 @@ let rec_intern_by_filename_only id f = (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin - Flags.if_warn msg_warning + msg_warning (pr_dirpath m.library_name ++ str " is already loaded from file " ++ str (library_full_filename m.library_name)); m.library_name, [] end else - let needed = intern_library_deps [] m.library_name m in + let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in + let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in m.library_name, needed +let native_name_from_filename f = + let ch = System.with_magic_number_check raw_intern_library f in + let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + Nativecode.mod_uid_of_dirpath lmd.md_name + let rec_intern_library_from_file idopt f = (* A name is specified, we have to check it contains library id *) - let paths = get_load_paths () in + let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in rec_intern_by_filename_only idopt f @@ -496,14 +493,13 @@ let rec_intern_library_from_file idopt f = which recursively loads its dependencies) *) -type library_reference = dir_path list * bool option - let register_library m = Declaremods.register_library m.library_name m.library_compiled m.library_objects - m.library_digest; + m.library_digests + m.library_extra_univs; register_loaded_library m (* Follow the semantics of Anticipate object: @@ -526,7 +522,7 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -type require_obj = library_t list * dir_path list * bool option +type require_obj = library_t list * DirPath.t list * bool option let in_require : require_obj -> obj = declare_object {(default_object "REQUIRE") with @@ -539,12 +535,9 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) -let xml_require = ref (fun d -> ()) -let set_xml_require f = xml_require := f - let require_library_from_dirpath modrefl export = - let needed = List.fold_left rec_intern_library [] modrefl in - let needed = List.rev_map snd needed in + let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in + let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin @@ -555,7 +548,6 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () let require_library qidl export = @@ -572,7 +564,6 @@ let require_library_from_file idopt file export = end else add_anonymous_leaf (in_require (needed,[modref],export)); - if !Flags.xml_export then !xml_require modref; add_frozen_state () (* the function called by Vernacentries.vernac_import *) @@ -597,28 +588,73 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let check_coq_overwriting p id = - let l = repr_dirpath p in - if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then + let l = DirPath.repr p in + let is_empty = match l with [] -> true | _ -> false in + if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^ + (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^ ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) +(* Verifies that a string starts by a letter and do not contain + others caracters than letters, digits, or `_` *) + +let check_module_name s = + let msg c = + strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++ + (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ + strbrk " is not allowed in module names\n" + in + let err c = errorlabstrm "" (msg c) in + match String.get s 0 with + | 'a' .. 'z' | 'A' .. 'Z' -> + for i = 1 to (String.length s)-1 do + match String.get s i with + | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> () + | c -> err c + done + | c -> err c + let start_library f = - let paths = get_load_paths () in - let _,longf = + let paths = Loadpath.get_paths () in + let _, longf = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in - let ldir0 = find_logical_path (Filename.dirname longf) in - let id = id_of_string (Filename.basename f) in + let ldir0 = + try + let lp = Loadpath.find_load_path (Filename.dirname longf) in + Loadpath.logical lp + with Not_found -> Nameops.default_root_prefix + in + let file = Filename.basename f in + let id = Id.of_string file in + check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; ldir,longf +let load_library_todo f = + let paths = Loadpath.get_paths () in + let _, longf = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let f = longf^"io" in + let ch = System.with_magic_number_check raw_intern_library f in + let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in + let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in + let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in + let tasks, _, _ = System.marshal_in_segment f ch in + let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in + close_in ch; + if tasks = None then errorlabstrm "restart" (str"not a .vio file"); + if s2 = None then errorlabstrm "restart" (str"not a .vio file"); + if s3 = None then errorlabstrm "restart" (str"not a .vio file"); + if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); + longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) let current_deps () = - List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list + List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list @@ -629,34 +665,85 @@ let error_recursively_dependent_library dir = strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") +(* We now use two different digests in a .vo file. The first one + only covers half of the file, without the opaque table. It is + used for identifying this version of this library : this digest + is the one leading to "inconsistent assumptions" messages. + The other digest comes at the very end, and covers everything + before it. This one is used for integrity check of the whole + file when loading the opaque table. *) + (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to dir f = - let cenv, seg = Declaremods.end_library dir in - let cenv, table = LightenLibrary.save cenv in + +let save_library_to ?todo dir f otab = + let f, except = match todo with + | None -> + assert(!Flags.compilation_mode = Flags.BuildVo); + f ^ "o", Future.UUIDSet.empty + | Some (l,_) -> + f ^ "io", + List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + Future.UUIDSet.empty l in + let cenv, seg, ast = Declaremods.end_library ~except dir in + let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in + let tasks, utab, dtab = + match todo with + | None -> None, None, None + | Some (tasks, rcbackup) -> + let tasks = + List.map Stateid.(fun r -> + { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + Some (tasks,rcbackup), + Some (univ_table,Univ.ContextSet.empty,false), + Some disch_table in + let except = + Future.UUIDSet.fold (fun uuid acc -> + Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc) + except Int.Set.empty in + let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in + Array.iteri (fun i x -> + if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) + opaque_table; let md = { md_name = dir; md_compiled = cenv; md_objects = seg; - md_deps = current_deps (); - md_imports = current_reexports () } in - if List.mem_assoc dir md.md_deps then + md_deps = Array.of_list (current_deps ()); + md_imports = Array.of_list (current_reexports ()) } in + if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then error_recursively_dependent_library dir; + (* Open the vo file and write the magic number *) let (f',ch) = raw_extern_library f in try - System.marshal_out ch md; - flush ch; - (* The loading of the opaque definitions table is optional whereas - the digest is loaded all the time. As a consequence, the digest - must be serialized before the table (if we want to keep the - current simple layout of .vo files). This also entails that the - digest does not take opaque terms into account anymore. *) - let di = Digest.file f' in - System.marshal_out ch di; - System.marshal_out ch table; - close_out ch - with reraise -> - msg_warn ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise + (* Writing vo payload *) + System.marshal_out_segment f' ch (md : seg_lib); + System.marshal_out_segment f' ch (utab : seg_univ option); + System.marshal_out_segment f' ch (dtab : seg_discharge option); + System.marshal_out_segment f' ch (tasks : 'tasks option); + System.marshal_out_segment f' ch (opaque_table : seg_proofs); + close_out ch; + (* Writing native code files *) + if not !Flags.no_native_compiler then + let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in + if not (Nativelib.compile_library dir ast fn) then + msg_error (str"Could not compile the library to native code. Skipping.") + with reraise -> + let reraise = Errors.push reraise in + let () = msg_warning (str ("Removed file "^f')) in + let () = close_out ch in + let () = Sys.remove f' in + iraise reraise + +let save_library_raw f lib univs proofs = + let (f',ch) = raw_extern_library (f^"o") in + System.marshal_out_segment f' ch (lib : seg_lib); + System.marshal_out_segment f' ch (Some univs : seg_univ option); + System.marshal_out_segment f' ch (None : seg_discharge option); + System.marshal_out_segment f' ch (None : 'tasks option); + System.marshal_out_segment f' ch (proofs : seg_proofs); + close_out ch (************************************************************************) (*s Display the memory use of a library. *) @@ -666,5 +753,16 @@ open Printf let mem s = let m = try_find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (size_kb m) (size_kb m.library_compiled) - (size_kb m.library_objects))) + (CObj.size_kb m) (CObj.size_kb m.library_compiled) + (CObj.size_kb m.library_objects))) + +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) + +let get_used_load_paths () = + StringSet.elements + (List.fold_left (fun acc m -> StringSet.add + (Filename.dirname (library_full_filename m.library_name)) acc) + StringSet.empty !libraries_loaded_list) + +let _ = Nativelib.get_load_paths := get_used_load_paths |