Imported Upstream version 8.5~beta1+dfsg

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