aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
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