blob: 4c6c654c5842fee65de9c5729d4c647bad441d74 (
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
(** This module provides functions to load, open and save
libraries. Libraries correspond to the subclass of modules that
coincide with a file on disk (the ".vo" files). Libraries on the
disk comes with checksums (obtained with the [Digest] module), which
are checked at loading time to prevent inconsistencies between files
written at various dates.
*)
(** {6 ... }
Require = load in the environment + open (if the optional boolean
is not [None]); mark also for export if the boolean is [Some true] *)
val require_library_from_dirpath
: lib_resolver:(DirPath.t -> CUnix.physical_path)
-> (DirPath.t * string) list
-> bool option
-> unit
(** {6 Start the compilation of a library } *)
(** Segments of a library *)
type seg_sum
type seg_lib
type seg_univ = (* all_cst, finished? *)
Univ.ContextSet.t * bool
type seg_proofs = Opaqueproof.opaque_proofterm array
(** End the compilation of a library and save it to a ".vo" file,
a ".vio" file, or a ".vos" file, depending on the todo_proofs
argument.
[output_native_objects]: when producing vo objects, also compile the native-code version. *)
type 'document todo_proofs =
| ProofsTodoNone (* for .vo *)
| ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
| ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *)
val save_library_to :
'document todo_proofs ->
output_native_objects:bool ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo
: CUnix.physical_path
-> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
(** {6 Interrogate the status of libraries } *)
(** - Tell if a library is loaded *)
val library_is_loaded : DirPath.t -> bool
(** - Tell which libraries are loaded *)
val loaded_libraries : unit -> DirPath.t list
(** - Return the full filename of a loaded library. *)
val library_full_filename : DirPath.t -> string
(** - Overwrite the filename of all libraries (used when restoring a state) *)
val overwrite_library_filenames : string -> unit
(** {6 Native compiler. } *)
val native_name_from_filename : string -> string
(** {6 Opaque accessors} *)
val indirect_accessor : Opaqueproof.indirect_accessor
|
