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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** {5 Toplevel management} *)
(** Coq plugins are identified by their OCaml library name (in the
Findlib sense) *)
module PluginSpec : sig
(** A plugin is identified by its canonical library name,
such as [coq-core.plugins.ltac] *)
type t
(** [repr p] returns a pair of [legacy_name, lib_name] where
[lib_name] is the canoncial library name.
[legacy_name] may be [Some pname] for the cases the plugin was
specified in [Declare ML Module] with their legacy name (for
example [ltac_plugin]). This will stop being supported soon and
is only here for compatiblity. Note that the name doesn't include
the ".cmxs" / ".cma" extension *)
val repr : t -> string option * string
val pp : t -> string
end
type toplevel =
{ load_plugin : PluginSpec.t -> unit
(** Load a findlib library, given by public name *)
; load_module : string -> unit
(** Load a cmxs / cmo module, used by the native compiler to load objects *)
; add_dir : string -> unit
(** Adds a dir to the module search path *)
; ml_loop : ?init_file:string -> unit -> unit
(** Run the OCaml toplevel with given addtitional initialisation file *)
}
(** Sets and initializes a toplevel (if any) *)
val set_top : toplevel -> unit
(** Low level module loading, for the native compiler and similar users. *)
val load_module : string -> unit
(** Removes the toplevel (if any) *)
val remove : unit -> unit
(** Tests if an Ocaml toplevel runs under Coq *)
val is_ocaml_top : unit -> bool
(** Starts the Ocaml toplevel loop *)
val ocaml_toploop : ?init_file:string -> unit -> unit
(** {5 ML Dynlink} *)
(** Adds a dir to the plugin search path, this also extends
OCamlfind's search path *)
val add_ml_dir : string -> unit
(** Tests if we can load ML files *)
val has_dynlink : bool
val module_is_known : string -> bool
(** {5 Initialization functions} *)
(** Declare a plugin which has been linked. A plugin is
a findlib library name. Usually, this will be called automatically
when use do [DECLARE PLUGIN "pkg.lib"] in the .mlg file.
The main effect is that dynlink will not be attempted for this
plugin, so eg if it was statically linked Coq will not try and
fail to find the cmxs.
*)
val add_known_module : string -> unit
(* EJGA: Todo, this could take a PluginSpec.t at some point *)
(** Declare a initialization function. The initialization function is
called in Declare ML Module, including reruns after backtracking
over it (either interactive backtrack, module closing backtrack,
Require of a file with Declare ML Module).
*)
val add_init_function : string -> (unit -> unit) -> unit
(** Register a callback that will be called when the module is declared with
the Declare ML Module command. This is useful to define Coq objects at that
time only. Several functions can be defined for one module; they will be
called in the order of declaration, and after the ML module has been
properly initialized.
Unlike the init functions it does not run after closing a module
or Requiring a file which contains the Declare ML Module.
This allows to have effects which depend on the module when
command was run in, eg add a named libobject which will use it for the prefix.
*)
val declare_cache_obj : (unit -> unit) -> string -> unit
(** {5 Declaring modules} *)
(** Implementation of the [Declare ML Module] vernacular command. *)
val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
(** {5 Utilities} *)
val print_ml_path : unit -> Pp.t
val print_ml_modules : unit -> Pp.t
val print_gc : unit -> Pp.t
|
