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
(************************************************************************)
(*         *      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 compilation_mode = BuildVo | BuildVos | BuildVok

type t =
  { compilation_mode : compilation_mode

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

  ; echo : bool

  ; glob_out    : Dumpglob.glob_output

  ; output_context : bool
  }

let default =
  { compilation_mode = BuildVo

  ; compile_file = None
  ; compilation_output_name = None

  ; 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 Rocq 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 (first,_) ->
    arg_error Pp.(str "More than one file to compile: " ++ str first ++ spc() ++
                  str "and " ++ str v_file)
  | None ->
    add_compile ?echo copts v_file

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 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 ()) }
        |"-vos" ->
          Flags.load_vos_libraries := true;
          { oval with compilation_mode = BuildVos }
        |"-vok" ->
          Flags.load_vos_libraries := true;
          { oval with compilation_mode = BuildVok }

        (* 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