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 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) *)
(************************************************************************)
val default_toplevel : Names.DirPath.t
type native_compiler = Coq_config.native_compiler =
NativeOff | NativeOn of { ondemand : bool }
type top = TopLogical of Names.DirPath.t | TopPhysical of string
type option_command =
| OptionSet of string option
| OptionUnset
| OptionAppend of string
type require_injection = { lib: string; prefix: string option; export: Lib.export_flag option; }
(** 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 (Goptions.option_name * 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;
time : time_config option;
profile : string option;
print_emacs : bool;
}
type coqargs_pre = {
boot : bool;
load_init : bool;
load_rcfile : bool;
ml_includes : CUnix.physical_path list;
vo_includes : Loadpath.vo_path list;
load_vernacular_list : (string * bool) list;
injections : injection_command list;
}
type coqargs_query =
| PrintWhere | PrintConfig
| PrintVersion | PrintMachineReadableVersion
| PrintHelp of Boot.Usage.specific_usage
type coqargs_main =
| Queries of coqargs_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 : usage:Boot.Usage.specific_usage -> init:t -> string list -> t * string list
val injection_commands : t -> injection_command list
val dirpath_of_top : top -> Names.DirPath.t
(* 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
val set_option : Goptions.option_name * option_command -> unit
|