1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
22
(*************************************************************************)
23
(*s Load path. Mapping from physical to logical paths etc.*)
25
type logical_path = dir_path
27
let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
29
let get_load_paths () = List.map pi1 !load_paths
31
let find_logical_path phys_dir =
32
let phys_dir = System.canonical_path_name phys_dir in
33
match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
35
| [] -> Nameops.default_root_prefix
36
| l -> anomaly ("Two logical paths are associated to "^phys_dir)
38
let is_in_load_paths phys_dir =
39
let dir = System.canonical_path_name phys_dir in
40
let lp = get_load_paths () in
41
let check_p = fun p -> (String.compare dir p) == 0 in
42
List.exists check_p lp
44
let remove_load_path dir =
45
load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
47
let add_load_path isroot (phys_path,coq_path) =
48
let phys_path = System.canonical_path_name phys_path in
49
match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
52
(* If this is not the default -I . to coqtop *)
54
(phys_path = System.canonical_path_name Filename.current_dir_name
55
&& coq_path = Nameops.default_root_prefix)
58
(* Assume the user is concerned by library naming *)
59
if dir <> Nameops.default_root_prefix then
60
Flags.if_warn msg_warning
61
(str phys_path ++ strbrk " was previously bound to " ++
62
pr_dirpath dir ++ strbrk "; it is remapped to " ++
64
remove_load_path phys_path;
65
load_paths := (phys_path,coq_path,isroot) :: !load_paths;
68
load_paths := (phys_path,coq_path,isroot) :: !load_paths;
69
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
71
let physical_paths (dp,lp) = dp
73
let extend_path_with_dirpath p dir =
74
List.fold_left Filename.concat p
75
(List.map string_of_id (List.rev (repr_dirpath dir)))
77
let root_paths_matching_dir_path dir =
78
let rec aux = function
80
| (p,d,true) :: l when is_dirpath_prefix_of d dir ->
81
let suffix = drop_dirpath_prefix d dir in
82
extend_path_with_dirpath p suffix :: aux l
86
(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
87
(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
89
(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
90
(* 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 *)
92
let intersections d1 d2 =
94
if d1 = empty_dirpath then [d2] else
95
let rest = aux (snd (chop_dirpath 1 d1)) in
96
if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
100
let loadpaths_matching_dir_path dir =
101
let rec aux = function
104
let inters = intersections d dir in
105
List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl))
109
(extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in
112
let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
114
(************************************************************************)
115
(*s Modules on disk contain the following informations (after the magic
116
number, and before the digest). *)
118
type compilation_unit_name = dir_path
120
type library_disk = {
121
md_name : compilation_unit_name;
122
md_compiled : compiled_library;
123
md_objects : Declaremods.library_objects;
124
md_deps : (compilation_unit_name * Digest.t) list;
125
md_imports : compilation_unit_name list }
127
(*s Modules loaded in memory contain the following informations. They are
128
kept in the global table [libraries_table]. *)
131
library_name : compilation_unit_name;
132
library_compiled : compiled_library;
133
library_objects : Declaremods.library_objects;
134
library_deps : (compilation_unit_name * Digest.t) list;
135
library_imports : compilation_unit_name list;
136
library_digest : Digest.t }
138
module LibraryOrdered =
143
(List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
146
module LibraryMap = Map.Make(LibraryOrdered)
147
module LibraryFilenameMap = Map.Make(LibraryOrdered)
149
(* This is a map from names to loaded libraries *)
150
let libraries_table = ref LibraryMap.empty
152
(* This is the map of loaded libraries filename *)
153
(* (not synchronized so as not to be caught in the states on disk) *)
154
let libraries_filename_table = ref LibraryFilenameMap.empty
156
(* These are the _ordered_ sets of loaded, imported and exported libraries *)
157
let libraries_loaded_list = ref []
158
let libraries_imports_list = ref []
159
let libraries_exports_list = ref []
163
!libraries_loaded_list,
164
!libraries_imports_list,
165
!libraries_exports_list
167
let unfreeze (mt,mo,mi,me) =
168
libraries_table := mt;
169
libraries_loaded_list := mo;
170
libraries_imports_list := mi;
171
libraries_exports_list := me
174
libraries_table := LibraryMap.empty;
175
libraries_loaded_list := [];
176
libraries_imports_list := [];
177
libraries_exports_list := []
180
Summary.declare_summary "MODULES"
181
{ Summary.freeze_function = freeze;
182
Summary.unfreeze_function = unfreeze;
183
Summary.init_function = init;
184
Summary.survive_module = false;
185
Summary.survive_section = false }
187
(* various requests to the tables *)
189
let find_library dir =
190
LibraryMap.find dir !libraries_table
192
let try_find_library dir =
195
error ("Unknown library " ^ (string_of_dirpath dir))
197
let register_library_filename dir f =
198
(* Not synchronized: overwrite the previous binding if one existed *)
199
(* from a previous play of the session *)
200
libraries_filename_table :=
201
LibraryFilenameMap.add dir f !libraries_filename_table
203
let library_full_filename dir =
204
try LibraryFilenameMap.find dir !libraries_filename_table
205
with Not_found -> "<unavailable filename>"
207
let overwrite_library_filenames f =
209
if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
210
LibraryMap.iter (fun dir _ -> register_library_filename dir f)
213
let library_is_loaded dir =
214
try let _ = find_library dir in true
215
with Not_found -> false
217
let library_is_opened dir =
218
List.exists (fun m -> m.library_name = dir) !libraries_imports_list
220
let library_is_exported dir =
221
List.exists (fun m -> m.library_name = dir) !libraries_exports_list
223
let loaded_libraries () =
224
List.map (fun m -> m.library_name) !libraries_loaded_list
226
let opened_libraries () =
227
List.map (fun m -> m.library_name) !libraries_imports_list
229
(* If a library is loaded several time, then the first occurrence must
230
be performed first, thus the libraries_loaded_list ... *)
232
let register_loaded_library m =
233
let rec aux = function
235
| m'::_ as l when m'.library_name = m.library_name -> l
236
| m'::l' -> m' :: aux l' in
237
libraries_loaded_list := aux !libraries_loaded_list;
238
libraries_table := LibraryMap.add m.library_name m !libraries_table
240
(* ... while if a library is imported/exported several time, then
241
only the last occurrence is really needed - though the imported
242
list may differ from the exported list (consider the sequence
243
Export A; Export B; Import A which results in A;B for exports but
244
in B;A for imports) *)
246
let rec remember_last_of_each l m =
249
| m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m
250
| m'::l' -> m' :: remember_last_of_each l' m
252
let register_open_library export m =
253
libraries_imports_list := remember_last_of_each !libraries_imports_list m;
255
libraries_exports_list := remember_last_of_each !libraries_exports_list m
257
(************************************************************************)
258
(*s Opening libraries *)
260
(* [open_library export explicit m] opens library [m] if not already
261
opened _or_ if explicitly asked to be (re)opened *)
263
let eq_lib_name m1 m2 = m1.library_name = m2.library_name
265
let open_library export explicit_libs m =
267
(* Only libraries indirectly to open are not reopen *)
268
(* Libraries explicitly mentionned by the user are always reopen *)
269
List.exists (eq_lib_name m) explicit_libs
270
or not (library_is_opened m.library_name)
272
register_open_library export m;
273
Declaremods.really_import_module (MPfile m.library_name)
277
libraries_exports_list := remember_last_of_each !libraries_exports_list m
279
(* open_libraries recursively open a list of libraries but opens only once
280
a library that is re-exported many times *)
282
let open_libraries export modl =
288
(fun l m -> remember_last_of_each l (try_find_library m))
290
in remember_last_of_each subimport m)
292
List.iter (open_library export modl) to_open_list
295
(**********************************************************************)
296
(* import and export - synchronous operations*)
298
let open_import i (_,(dir,export)) =
300
(* even if the library is already imported, we re-import it *)
301
(* if not (library_is_opened dir) then *)
302
open_libraries export [try_find_library dir]
304
let cache_import obj =
307
let subst_import (_,_,o) = o
309
let export_import o = Some o
311
let classify_import (_,(_,export as obj)) =
312
if export then Substitute obj else Dispose
315
let (in_import, out_import) =
316
declare_object {(default_object "IMPORT LIBRARY") with
317
cache_function = cache_import;
318
open_function = open_import;
319
subst_function = subst_import;
320
classify_function = classify_import }
323
(************************************************************************)
324
(*s Low-level interning/externing of libraries to files *)
326
(*s Loading from disk to cache (preparation phase) *)
328
let (raw_extern_library, raw_intern_library) =
329
System.raw_extern_intern Coq_config.vo_magic_number ".vo"
331
let with_magic_number_check f a =
333
with System.Bad_magic_number fname ->
334
errorlabstrm "with_magic_number_check"
335
(str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++
336
spc () ++ str"It is corrupted" ++ spc () ++
337
str"or was compiled with another version of Coq.")
339
(************************************************************************)
340
(*s Locate absolute or partially qualified library names in the path *)
342
exception LibUnmappedDir
343
exception LibNotFound
344
type library_location = LibLoaded | LibInPath
346
let locate_absolute_library dir =
347
(* Search in loadpath *)
348
let pref, base = split_dirpath dir in
349
let loadpath = root_paths_matching_dir_path pref in
350
if loadpath = [] then raise LibUnmappedDir;
352
let name = (string_of_id base)^".vo" in
353
let _, file = System.where_in_path ~warn:false loadpath name in
356
(* Last chance, removed from the file system but still in memory *)
357
if library_is_loaded dir then
358
(dir, library_full_filename dir)
362
let locate_qualified_library warn qid =
364
(* Search library in loadpath *)
365
let dir, base = repr_qualid qid in
366
let loadpath = loadpaths_matching_dir_path dir in
367
if loadpath = [] then raise LibUnmappedDir;
368
let name = string_of_id base ^ ".vo" in
369
let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
370
let dir = extend_dirpath (List.assoc lpath loadpath) base in
372
if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
373
(* Otherwise, look for it in the file system *)
374
else (LibInPath, dir, file)
375
with Not_found -> raise LibNotFound
377
let explain_locate_library_error qid = function
379
let prefix, _ = repr_qualid qid in
380
errorlabstrm "load_absolute_library_from"
381
(str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
382
str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
384
errorlabstrm "load_absolute_library_from"
385
(str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
388
let try_locate_absolute_library dir =
390
locate_absolute_library dir
392
explain_locate_library_error (qualid_of_dirpath dir) e
394
let try_locate_qualified_library (loc,qid) =
396
let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
399
explain_locate_library_error qid e
402
(************************************************************************)
403
(* Internalise libraries *)
405
let lighten_library m =
406
if !Flags.dont_load_proofs then lighten_library m else m
408
let mk_library md digest = {
409
library_name = md.md_name;
410
library_compiled = lighten_library md.md_compiled;
411
library_objects = md.md_objects;
412
library_deps = md.md_deps;
413
library_imports = md.md_imports;
414
library_digest = digest }
416
let intern_from_file f =
417
let ch = with_magic_number_check raw_intern_library f in
418
let md = System.marshal_in ch in
419
let digest = System.marshal_in ch in
421
register_library_filename md.md_name f;
424
let rec intern_library needed (dir, f) =
425
(* Look if in the current logical environment *)
426
try find_library dir, needed
428
(* Look if already listed and consequently its dependencies too *)
429
try List.assoc dir needed, needed
431
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
432
let m = intern_from_file f in
433
if dir <> m.library_name then
434
errorlabstrm "load_physical_library"
435
(str ("The file " ^ f ^ " contains library") ++ spc () ++
436
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
437
spc() ++ pr_dirpath dir);
438
m, intern_library_deps needed dir m
440
and intern_library_deps needed dir m =
441
(dir,m)::List.fold_left (intern_mandatory_library dir) needed m.library_deps
443
and intern_mandatory_library caller needed (dir,d) =
444
let m,needed = intern_library needed (try_locate_absolute_library dir) in
445
if d <> m.library_digest then
446
errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^
447
".vo makes inconsistent assumptions over library "
448
^(string_of_dirpath dir)));
451
let rec_intern_library needed mref =
452
let _,needed = intern_library needed mref in needed
454
let check_library_short_name f dir = function
455
| Some id when id <> snd (split_dirpath dir) ->
456
errorlabstrm "check_library_short_name"
457
(str ("The file " ^ f ^ " contains library") ++ spc () ++
458
pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
462
let rec_intern_by_filename_only id f =
463
let m = try intern_from_file f with Sys_error s -> error s in
464
(* Only the base name is expected to match *)
465
check_library_short_name f m.library_name id;
466
(* We check no other file containing same library is loaded *)
467
if library_is_loaded m.library_name then
469
Flags.if_verbose warning
470
((string_of_dirpath m.library_name)^" is already loaded from file "^
471
library_full_filename m.library_name);
475
let needed = intern_library_deps [] m.library_name m in
476
m.library_name, needed
478
let rec_intern_library_from_file idopt f =
479
(* A name is specified, we have to check it contains library id *)
480
let paths = get_load_paths () in
482
System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
483
rec_intern_by_filename_only idopt f
485
(**********************************************************************)
486
(*s [require_library] loads and possibly opens a library. This is a
487
synchronized operation. It is performed as follows:
489
preparation phase: (functions require_library* ) the library and its
490
dependencies are read from to disk (using intern_* )
491
[they are read from disk to ensure that at section/module
492
discharging time, the physical library referred to outside the
493
section/module is the one that was used at type-checking time in
496
execution phase: (through add_leaf and cache_require)
497
the library is loaded in the environment and Nametab, the objects are
498
registered etc, using functions from Declaremods (via load_library,
499
which recursively loads its dependencies)
502
type library_reference = dir_path list * bool option
504
let register_library (dir,m) =
505
Declaremods.register_library
510
register_loaded_library m
512
(* Follow the semantics of Anticipate object:
513
- called at module or module type closing when a Require occurs in
514
the module or module type
515
- not called from a library (i.e. a module identified with a file) *)
516
let load_require _ (_,(needed,modl,_)) =
517
List.iter register_library needed
519
let open_require i (_,(_,modl,export)) =
520
Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
523
(* [needed] is the ordered list of libraries not already loaded *)
524
let cache_require o =
528
(* keeps the require marker for closed section replay but removes
529
OS dependent fields from .vo files for cross-platform compatibility *)
530
let export_require (_,l,e) = Some ([],l,e)
532
let discharge_require (_,o) = Some o
534
(* open_function is never called from here because an Anticipate object *)
536
let (in_require, out_require) =
537
declare_object {(default_object "REQUIRE") with
538
cache_function = cache_require;
539
load_function = load_require;
540
open_function = (fun _ _ -> assert false);
541
export_function = export_require;
542
discharge_function = discharge_require;
543
classify_function = (fun (_,o) -> Anticipate o) }
545
(* Require libraries, import them if [export <> None], mark them for export
546
if [export = Some true] *)
548
let xml_require = ref (fun d -> ())
549
let set_xml_require f = xml_require := f
551
let require_library qidl export =
552
let modrefl = List.map try_locate_qualified_library qidl in
553
let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
554
let modrefl = List.map fst modrefl in
555
if Lib.is_modtype () || Lib.is_module () then
557
add_anonymous_leaf (in_require (needed,modrefl,None));
558
Option.iter (fun exp ->
559
List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
563
add_anonymous_leaf (in_require (needed,modrefl,export));
564
if !Flags.xml_export then List.iter !xml_require modrefl;
567
let require_library_from_file idopt file export =
568
let modref,needed = rec_intern_library_from_file idopt file in
569
let needed = List.rev needed in
570
if Lib.is_modtype () || Lib.is_module () then begin
571
add_anonymous_leaf (in_require (needed,[modref],None));
572
Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
576
add_anonymous_leaf (in_require (needed,[modref],export));
577
if !Flags.xml_export then !xml_require modref;
580
(* the function called by Vernacentries.vernac_import *)
582
let import_module export (loc,qid) =
584
match Nametab.locate_module qid with
586
if Lib.is_modtype () || Lib.is_module () || not export then
587
add_anonymous_leaf (in_import (dir, export))
589
add_anonymous_leaf (in_import (dir, export))
591
Declaremods.import_module export mp
595
(loc,"import_library",
596
str ((string_of_qualid qid)^" is not a module"))
598
(************************************************************************)
599
(*s Initializing the compilation of a library. *)
601
let check_coq_overwriting p =
602
let l = repr_dirpath p in
603
if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
604
errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
606
let start_library f =
607
let paths = get_load_paths () in
609
System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
610
let ldir0 = find_logical_path (Filename.dirname longf) in
611
check_coq_overwriting ldir0;
612
let id = id_of_string (Filename.basename f) in
613
let ldir = extend_dirpath ldir0 id in
614
Declaremods.start_library ldir;
617
(************************************************************************)
618
(*s [save_library dir] ends library [dir] and save it to the disk. *)
620
let current_deps () =
621
List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
623
let current_reexports () =
624
List.map (fun m -> m.library_name) !libraries_exports_list
626
let error_recursively_dependent_library dir =
628
(strbrk "Unable to use logical name " ++ pr_dirpath dir ++
629
strbrk " to save current library because" ++
630
strbrk " it already depends on a library of this name.")
632
(* Security weakness: file might have been changed on disk between
633
writing the content and computing the checksum... *)
634
let save_library_to dir f =
635
let cenv, seg = Declaremods.end_library dir in
640
md_deps = current_deps ();
641
md_imports = current_reexports () } in
642
if List.mem_assoc dir md.md_deps then
643
error_recursively_dependent_library dir;
644
let (f',ch) = raw_extern_library f in
646
System.marshal_out ch md;
648
let di = Digest.file f' in
649
System.marshal_out ch di;
651
with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
653
(************************************************************************)
654
(*s Display the memory use of a library. *)
659
let m = try_find_library s in
660
h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
661
(size_kb m) (size_kb m.library_compiled)
662
(size_kb m.library_objects)))
added
removed
library/library.ml
