blob: d69ecef9e80dd26862fd2c625039e4c69e9d9e0c (
plain)
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ 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. Modules 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
val export_library : 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
(*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
|
