File: coqargs.mli

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (117 lines) | stat: -rw-r--r-- 3,813 bytes parent folder | download | duplicates (2)
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