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
114
115
116
117
|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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) *)
(************************************************************************)
type native_compiler = Coq_config.native_compiler =
NativeOff | NativeOn of { ondemand : bool }
type top = TopLogical of string | TopPhysical of string
type option_command =
| OptionSet of string option
| OptionUnset
type export_flag = Export | Import
type require_injection = { lib: string; prefix: string option; export: export_flag option; allow_failure: bool }
(** Parameters follow [Library], that is to say, [lib,prefix,export]
means require library [lib] from optional [prefix] and import or
export if [export] is [Some Lib.Import]/[Some Lib.Export]. *)
type injection_command =
| OptionInjection of (string list * option_command)
(** Set flags or options before the initial state is ready. *)
| RequireInjection of require_injection
(** Require libraries before the initial state is
ready. *)
| WarnNoNative of string
(** Used so that "-w -native-compiler-disabled -native-compiler yes"
does not cause a warning. The native option must be processed
before injections (because it affects require), so the
instruction to emit a message is separated. *)
| WarnNativeDeprecated
(** Used so that "-w -native-compiler-deprecated-option -native-compiler FLAG"
does not cause a warning, similarly to above. *)
type coqargs_logic_config = {
impredicative_set : bool;
indices_matter : bool;
type_in_type : bool;
rewrite_rules : bool;
toplevel_name : top;
}
type time_config = ToFeedback | ToFile of string
type coqargs_config = {
logic : coqargs_logic_config;
rcfile : string option;
coqlib : string option;
enable_VM : bool;
native_compiler : native_compiler;
native_output_dir : CUnix.physical_path;
native_include_dirs : CUnix.physical_path list;
output_directory : CUnix.physical_path option;
exclude_dirs : CUnix.physical_path list;
beautify : bool;
quiet : bool;
time : time_config option;
test_mode : bool;
profile : string option;
print_emacs : bool;
}
type vo_path = {
implicit : bool; (** true if -R, otherwise -Q *)
unix_path : string;
rocq_path : string;
}
type coqargs_pre = {
boot : bool;
load_init : bool;
load_rcfile : bool;
ml_includes : CUnix.physical_path list;
vo_includes : vo_path list;
load_vernacular_list : (string * bool) list;
injections : injection_command list;
}
type coqargs_main =
| Queries of Boot.Usage.query list
| Run
type coqargs_post = {
memory_stat : bool;
}
type t = {
config : coqargs_config;
pre : coqargs_pre;
main : coqargs_main;
post : coqargs_post;
}
(* Default options *)
val default : t
val parse_args : init:t -> string list -> t * string list
val injection_commands : t -> injection_command list
(* Common utilities *)
val get_int : opt:string -> string -> int
val get_int_opt : opt:string -> string -> int option
val get_bool : opt:string -> string -> bool
val get_float : opt:string -> string -> float
val error_missing_arg : string -> 'a
val error_wrong_arg : string -> 'a
|
