1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: library.mli,v 1.23.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
(*i*)
open Util
open Names
open Libnames
open Libobject
(*i*)
(*s This module is the heart of the library. It provides low level
functions to load, open and save libraries. Libraries are saved
onto the disk with checksums (obtained with the [Digest] module),
which are checked at loading time to prevent inconsistencies
between files written at various dates. It also provides a high
level function [require] which corresponds to the vernacular
command [Require]. *)
val read_library : qualid located -> unit
val read_library_from_file : System.physical_path -> unit
(* [import_library true qid] = [export qid] *)
val import_library : bool -> qualid located -> unit
val library_is_loaded : dir_path -> bool
val library_is_opened : dir_path -> bool
val loaded_libraries : unit -> dir_path list
val opened_libraries : unit -> dir_path list
val fmt_libraries_state : unit -> Pp.std_ppcmds
(*s Require. The command [require_library spec m file export] loads and opens
a library [m]. [file] specifies the filename, if not [None]. [spec]
specifies to look for a specification ([true]) or for an implementation
([false]), if not [None]. And [export] specifies if the library must be
exported. *)
val require_library :
bool option -> qualid located list -> bool -> unit
val require_library_from_file :
bool option -> identifier option -> System.physical_path -> bool -> unit
val set_xml_require : (dir_path -> unit) -> unit
(*s [save_library_to s f] saves the current environment as a library [s]
in the file [f]. *)
val start_library : string -> dir_path * string
val save_library_to : dir_path -> string -> unit
(* [library_full_filename] returns the full filename of a loaded library. *)
val library_full_filename : dir_path -> string
(*s Global load path *)
type logical_path = dir_path
val get_load_path : unit -> System.physical_path list
val get_full_load_path : unit -> (System.physical_path * logical_path) list
val add_load_path_entry : System.physical_path * logical_path -> unit
val remove_path : System.physical_path -> unit
val find_logical_path : System.physical_path -> logical_path
val load_path_of_logical_path : dir_path -> System.physical_path list
exception LibUnmappedDir
exception LibNotFound
type library_location = LibLoaded | LibInPath
val locate_qualified_library :
qualid -> library_location * dir_path * System.physical_path
val check_required_library : string list -> unit
(*s Displays the memory use of a library. *)
val mem : dir_path -> Pp.std_ppcmds
(* For discharge *)
type library_reference
val out_require : Libobject.obj -> library_reference
val reload_library : library_reference -> unit
|
