package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file coqcargs.ml

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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
(************************************************************************)
(*         *   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)         *)
(************************************************************************)

type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok

type t =
  { compilation_mode : compilation_mode

  ; compile_file: (string * bool) option  (* bool is verbosity  *)
  ; compilation_output_name : string option

  ; vio_checking : bool
  ; vio_tasks    : (int list * string) list
  ; vio_files    : string list
  ; vio_files_j  : int

  ; echo : bool

  ; glob_out    : Dumpglob.glob_output

  ; output_context : bool
  }

let default =
  { compilation_mode = BuildVo

  ; compile_file = None
  ; compilation_output_name = None

  ; vio_checking = false
  ; vio_tasks    = []
  ; vio_files    = []
  ; vio_files_j  = 0

  ; echo = false

  ; glob_out = Dumpglob.MultFiles

  ; output_context = false
  }

let depr opt =
  Feedback.msg_warning Pp.(seq[str "Option "; str opt; str " is a noop and deprecated"])

(* XXX Remove this duplication with Coqargs *)
let fatal_error exn =
  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
  exit exit_code

let error_missing_arg s =
  prerr_endline ("Error: extra argument expected after option "^s);
  prerr_endline "See -help for the syntax of supported options";
  exit 1

let arg_error msg = CErrors.user_err msg

let is_dash_argument s = String.length s > 0 && s.[0] = '-'

let add_compile ?echo copts s =
  if is_dash_argument s then
    arg_error Pp.(str "Unknown option " ++ str s);
  (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
  let echo = Option.default copts.echo echo in
  let s =
    let open Filename in
    if is_implicit s
    then concat current_dir_name s
    else s
  in
  { copts with compile_file = Some (s,echo) }

let add_compile ?echo copts v_file =
  match copts.compile_file with
  | Some _ ->
    arg_error Pp.(str "More than one file to compile: " ++ str v_file)
  | None ->
    add_compile ?echo copts v_file

let add_vio_task opts f =
  { opts with vio_tasks = f :: opts.vio_tasks }

let add_vio_file opts f =
  { opts with vio_files = f :: opts.vio_files }

let set_vio_checking_j opts opt j =
  try { opts with vio_files_j = int_of_string j }
  with Failure _ ->
    prerr_endline ("The first argument of " ^ opt ^ " must the number");
    prerr_endline "of concurrent workers to be used (a positive integer).";
    prerr_endline "Makefiles generated by coq_makefile should be called";
    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
    exit 1

let set_compilation_mode opts mode =
  match opts.compilation_mode with
  | BuildVo -> { opts with compilation_mode = mode }
  | mode' when mode <> mode' ->
    prerr_endline "Options -vio and -vio2vo are exclusive";
    exit 1
  | _ -> opts

let get_task_list s =
  List.map (fun s ->
      try int_of_string s
      with Failure _ ->
        prerr_endline "Option -check-vio-tasks expects a comma-separated list";
        prerr_endline "of integers followed by a list of files";
        exit 1)
    (Str.split (Str.regexp ",") s)

let is_not_dash_option = function
  | Some f when String.length f > 0 && f.[0] <> '-' -> true
  | _ -> false

let rec add_vio_args peek next oval =
  if is_not_dash_option (peek ()) then
    let oval = add_vio_file oval (next ()) in
    add_vio_args peek next oval
  else oval

let warn_deprecated_quick =
  CWarnings.create ~name:"deprecated-quick" ~category:Deprecation.Version.v8_11
         (fun () ->
          Pp.strbrk "The -quick option is renamed -vio. Please consider using the -vos feature instead.")

let parse arglist : t =
  let echo = ref false in
  let args = ref arglist in
  let extras = ref [] in
  let rec parse (oval : t) = match !args with
    | [] ->
      (oval, List.rev !extras)
    | opt :: rem ->
      args := rem;
      let next () = match !args with
        | x::rem -> args := rem; x
        | [] -> error_missing_arg opt
      in
      let peek_next () = match !args with
        | x::_ -> Some x
        | [] -> None
      in
      let noval : t = begin match opt with
        (* Deprecated options *)
        | "-opt"
        | "-byte" as opt ->
          depr opt;
          oval
        | "-image" as opt ->
          depr opt;
          let _ = next () in
          oval

        (* Non deprecated options *)
        | "-output-context" ->
          { oval with output_context = true }
        (* Verbose == echo mode *)
        | "-verbose" ->
          echo := true;
          oval
        (* Output filename *)
        | "-o" ->
          { oval with compilation_output_name = Some (next ()) }
        | "-quick" ->
          warn_deprecated_quick();
          set_compilation_mode oval BuildVio
        | "-vio" ->
          set_compilation_mode oval BuildVio
        |"-vos" ->
          Flags.load_vos_libraries := true;
          { oval with compilation_mode = BuildVos }
        |"-vok" ->
          Flags.load_vos_libraries := true;
          { oval with compilation_mode = BuildVok }

        | "-check-vio-tasks" ->
          let tno = get_task_list (next ()) in
          let tfile = next () in
          add_vio_task oval (tno,tfile)

        | "-schedule-vio-checking" ->
          let oval = { oval with vio_checking = true } in
          let oval = set_vio_checking_j oval opt (next ()) in
          let oval = add_vio_file oval (next ()) in
          add_vio_args peek_next next oval

        | "-schedule-vio2vo" ->
          let oval = set_vio_checking_j oval opt (next ()) in
          let oval = add_vio_file oval (next ()) in
          add_vio_args peek_next next oval

        | "-vio2vo" ->
          let oval = add_compile ~echo:false oval (next ()) in
          set_compilation_mode oval Vio2Vo

        (* Glob options *)
        |"-no-glob" | "-noglob" ->
          { oval with glob_out = Dumpglob.NoGlob }

        |"-dump-glob" ->
          let file = next () in
          { oval with glob_out = Dumpglob.File file }

        (* Rest *)
        | s ->
          extras := s :: !extras;
          oval
      end in
      parse noval
  in
  try
    let opts, extra = parse default in
    let args = List.fold_left add_compile opts extra in
    args
  with any -> fatal_error any

let parse args =
  let opts = parse args in
  { opts with
    vio_tasks = List.rev opts.vio_tasks
  ; vio_files = List.rev opts.vio_files
  }
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct