package rocq-runtime

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

Source file stmargs.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
(************************************************************************)
(*         *      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)         *)
(************************************************************************)

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 set_worker_id opt s =
  assert (s <> "master");
  Flags.async_proofs_worker_id := s

let get_host_port opt s =
  match String.split_on_char ':' s with
  | [host; portr; portw] ->
    Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
  | ["stdfds"] -> Some Spawned.AnonPipe
  | _ ->
    Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)

let get_error_resilience opt = function
  | "on" | "all" | "yes" -> Stm.AsyncOpts.FAll
  | "off" | "no" -> Stm.AsyncOpts.FNone
  | s -> Stm.AsyncOpts.FOnly (String.split_on_char ',' s)

let get_priority opt s =
  try CoqworkmgrApi.priority_of_string s
  with Invalid_argument _ ->
    Coqargs.error_wrong_arg ("Error: low/high expected after "^opt)

let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
  | "no" | "off" -> APoff
  | "yes" | "on" -> APon
  | "lazy" -> APonLazy
  | _ ->
    Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt)

let get_cache opt = function
  | "force" -> Some Stm.AsyncOpts.Force
  | _ ->
    Coqargs.error_wrong_arg ("Error: force expected after "^opt)

let spawn_args (opts:Coqargs.t) =
  (* Coqargs whose effect is not in the summary and matters for workers:

     Flags.output_directory
     Flags.test_mode
     native output dir, native includes

     Coqargs whose effect is used before the summary is installed and matter for workers:

     -I, -boot

     and we force -q -noinit otherwise the worker will try to require the
     rcfile and prelude before receiving the summary

     AFAICT that's all *)
  let output_dir = match opts.config.output_directory with
    | None -> []
    | Some dir -> ["-output-directory";dir]
  in
  let test_mode = if opts.config.test_mode then ["-test-mode"] else [] in
  let native_output = ["-native-output-dir"; opts.config.native_output_dir] in
  let native_include ni = ["-nI";ni] in
  let native_includes = CList.concat_map native_include opts.config.native_include_dirs in
  let ml_include i = ["-I"; i] in
  let ml_includes = CList.concat_map ml_include opts.pre.ml_includes in
  let boot = if opts.pre.boot then ["-boot"] else [] in
  List.concat [
    output_dir;
    test_mode;
    native_output;
    native_includes;
    ml_includes;
    boot;
    ["-q"; "-noinit"]
  ]


let parse_args opts arglist : Stm.AsyncOpts.stm_opt * string list =
  let init = Stm.AsyncOpts.default_opts ~spawn_args:(spawn_args opts) in
  let args = ref arglist in
  let extras = ref [] in
  let rec parse oval = match !args with
  | [] ->
    (oval, List.rev !extras)
  | opt :: rem ->
    args := rem;
    let next () = match !args with
      | x::rem -> args := rem; x
      | [] -> Coqargs.error_missing_arg opt
    in
    let noval = begin match opt with

    |"-async-proofs" ->
      { oval with
        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
      }
    |"-async-proofs-j" ->
      { oval with
        Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ()))
      }
    |"-async-proofs-cache" ->
      { oval with
        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
      }

    |"-async-proofs-tac-j" ->
      let j = Coqargs.get_int ~opt (next ()) in
      if j < 0 then begin
        Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 0")
      end;
      { oval with
        Stm.AsyncOpts.async_proofs_n_tacworkers = j
      }

    |"-async-proofs-worker-priority" ->
      { oval with
        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
      }

    |"-async-proofs-private-flags" ->
      { oval with
        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
      }

    |"-async-proofs-tactic-error-resilience" ->
      { oval with
        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
      }

    |"-async-proofs-command-error-resilience" ->
      { oval with
        Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ())
      }

    |"-async-proofs-delegation-threshold" ->
      { oval with
        Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ())
      }

    |"-worker-id" -> set_worker_id opt (next ()); oval

    |"-main-channel" ->
      let ch = next () in
      Spawned.main_channel := get_host_port opt ch;
      { oval with spawn_args = opt :: ch :: oval.spawn_args }

    |"-control-channel" ->
      let ch = next () in
      Spawned.control_channel := get_host_port opt ch;
      { oval with spawn_args = opt :: ch :: oval.spawn_args }

    (* Options with zero arg *)
    |"-async-queries-always-delegate"
    |"-async-proofs-always-delegate"
    |"-async-proofs-never-reopen-branch" ->
      { oval with
        Stm.AsyncOpts.async_proofs_never_reopen_branch = true;
        spawn_args = opt :: oval.spawn_args;
      }
    |"-stm-debug" -> Stm.stm_debug := true; { oval with spawn_args = opt :: oval.spawn_args }
    (* Unknown option *)
    | s ->
      extras := s :: !extras;
      oval
    end in
    parse noval
  in
  try
    parse init
  with any -> fatal_error any

let usage = "\
\n  -stm-debug             STM debug mode (will trace every transaction)\
"
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