summaryrefslogtreecommitdiff
path: root/library/library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml86
1 files changed, 53 insertions, 33 deletions
diff --git a/library/library.ml b/library/library.ml
index 09f92e6a..37622874 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
@@ -68,8 +66,6 @@ let add_load_path isroot (phys_path,coq_path) =
load_paths := (phys_path,coq_path,isroot) :: !load_paths;
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
-let physical_paths (dp,lp) = dp
-
let extend_path_with_dirpath p dir =
List.fold_left Filename.concat p
(List.map string_of_id (List.rev (repr_dirpath dir)))
@@ -119,7 +115,7 @@ type compilation_unit_name = dir_path
type library_disk = {
md_name : compilation_unit_name;
- md_compiled : compiled_library;
+ md_compiled : LightenLibrary.lightened_compiled_library;
md_objects : Declaremods.library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
@@ -215,9 +211,6 @@ let library_is_loaded dir =
let library_is_opened dir =
List.exists (fun m -> m.library_name = dir) !libraries_imports_list
-let library_is_exported dir =
- List.exists (fun m -> m.library_name = dir) !libraries_exports_list
-
let loaded_libraries () =
List.map (fun m -> m.library_name) !libraries_loaded_list
@@ -307,7 +300,7 @@ let subst_import (_,o) = o
let classify_import (_,export as obj) =
if export then Substitute obj else Dispose
-let (in_import, out_import) =
+let in_import : dir_path * bool -> obj =
declare_object {(default_object "IMPORT LIBRARY") with
cache_function = cache_import;
open_function = open_import;
@@ -389,24 +382,41 @@ let try_locate_qualified_library (loc,qid) =
(************************************************************************)
(* Internalise libraries *)
-let lighten_library m =
- if !Flags.dont_load_proofs then lighten_library m else m
-
-let mk_library md digest = {
- library_name = md.md_name;
- library_compiled = lighten_library md.md_compiled;
- library_objects = md.md_objects;
- library_deps = md.md_deps;
- library_imports = md.md_imports;
- library_digest = digest }
+let mk_library md table digest =
+ let md_compiled =
+ LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled
+ in {
+ library_name = md.md_name;
+ library_compiled = md_compiled;
+ library_objects = md.md_objects;
+ library_deps = md.md_deps;
+ library_imports = md.md_imports;
+ library_digest = digest
+ }
+
+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 ch <> digest then failwith "File changed!";
+ let table = (System.marshal_in ch : LightenLibrary.table) in
+ close_in ch;
+ table
+ with _ ->
+ 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 md = System.marshal_in ch in
+ let lmd = System.marshal_in ch in
+ let pos = pos_in ch in
let digest = System.marshal_in 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
close_in ch;
- register_library_filename md.md_name f;
- mk_library md digest
+ library
let rec intern_library needed (dir, f) =
(* Look if in the current logical environment *)
@@ -453,9 +463,9 @@ 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_verbose warning
- ((string_of_dirpath m.library_name)^" is already loaded from file "^
- library_full_filename m.library_name);
+ Flags.if_warn 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
@@ -488,7 +498,7 @@ let rec_intern_library_from_file idopt f =
type library_reference = dir_path list * bool option
-let register_library (dir,m) =
+let register_library m =
Declaremods.register_library
m.library_name
m.library_compiled
@@ -516,7 +526,9 @@ let discharge_require (_,o) = Some o
(* open_function is never called from here because an Anticipate object *)
-let (in_require, out_require) =
+type require_obj = library_t list * dir_path list * bool option
+
+let in_require : require_obj -> obj =
declare_object {(default_object "REQUIRE") with
cache_function = cache_require;
load_function = load_require;
@@ -531,9 +543,10 @@ let xml_require = ref (fun d -> ())
let set_xml_require f = xml_require := f
let require_library_from_dirpath modrefl export =
- let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
+ let needed = List.fold_left rec_intern_library [] modrefl in
+ let needed = List.rev_map snd needed in
let modrefl = List.map fst modrefl in
- if Lib.is_modtype () || Lib.is_module () then
+ if Lib.is_module_or_modtype () then
begin
add_anonymous_leaf (in_require (needed,modrefl,None));
Option.iter (fun exp ->
@@ -551,8 +564,8 @@ let require_library qidl export =
let require_library_from_file idopt file export =
let modref,needed = rec_intern_library_from_file idopt file in
- let needed = List.rev needed in
- if Lib.is_modtype () || Lib.is_module () then begin
+ let needed = List.rev_map snd needed in
+ if Lib.is_module_or_modtype () then begin
add_anonymous_leaf (in_require (needed,[modref],None));
Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
export
@@ -568,7 +581,7 @@ let import_module export (loc,qid) =
try
match Nametab.locate_module qid with
| MPfile dir ->
- if Lib.is_modtype () || Lib.is_module () || not export then
+ if Lib.is_module_or_modtype () || not export then
add_anonymous_leaf (in_import (dir, export))
else
add_anonymous_leaf (in_import (dir, export))
@@ -620,6 +633,7 @@ let error_recursively_dependent_library dir =
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 md = {
md_name = dir;
md_compiled = cenv;
@@ -632,8 +646,14 @@ let save_library_to dir f =
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 e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e