Merge PR #10246: Investigations in the initialization of coq binaries and command line (part 1)

Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin

24 files changed, 540 insertions, 445 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 92c24b3b85..889cc3be36 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -102,7 +102,7 @@ let display_coqtop_answer cmd lines =
 
 let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+  let cmd = Filename.quote (coqtop_path ()) ^" -nois -batch " ^ argstr in
   let cmd = requote cmd in
   let filtered_args = ref [] in
   let errlines = ref [] in
diff --git a/ide/idetop.ml b/ide/idetop.ml
index c6a8fdaa55..02682e2ee9 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -496,7 +496,10 @@ let msg_format = ref (fun () ->
 
 (* The loop ignores the command line arguments as the current model delegates
    its handing to the toplevel container. *)
-let loop ~opts:_ ~state =
+let loop run_mode ~opts:_ state =
+  match run_mode with
+  | Coqtop.Batch -> exit 0
+  | Coqtop.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
   init_signal_handler ();
@@ -549,16 +552,42 @@ let rec parse = function
        x :: parse rest
   | [] -> []
 
-let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
+let coqidetop_specific_usage = Usage.{
+  executable_name = "coqidetop";
+  extra_args = "";
+  extra_options = "\n\
+coqidetop specific options:\n\
+\n  --xml_formatinclude dir           (idem)\
+\n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
+}
 
-let islave_init ~opts extra_args =
-  let args = parse extra_args in
-  CoqworkmgrApi.(init High);
-  opts, args
+let islave_parse ~opts extra_args =
+  let open Coqtop in
+  let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in
+  let extra_args = parse extra_args in
+  (* One of the role of coqidetop is to find the name of buffers to open *)
+  (* in the command line; Coqide is waiting these names on stdout *)
+  (* (see filter_coq_opts in coq.ml), so we send them now *)
+  print_string (String.concat "\n" extra_args);
+  run_mode, []
+
+let islave_init run_mode ~opts =
+  if run_mode = Coqtop.Batch then Flags.quiet := true;
+  Coqtop.init_toploop opts
+
+let islave_default_opts =
+  Coqargs.{ default with
+    config = { default.config with
+      stm_flags = { default.config.stm_flags with
+         Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}}
 
 let () =
   let open Coqtop in
-  let custom = { init = islave_init; run = loop; opts = Coqargs.default } in
+  let custom = {
+      parse_extra = islave_parse ;
+      help = coqidetop_specific_usage;
+      init = islave_init;
+      run = loop;
+      opts = islave_default_opts } in
   start_coq custom
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 044ac29e92..909804d0c9 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -115,7 +115,7 @@ module Make(T : Task) () = struct
   type process = Worker.process
   type extra = (T.task * cancel_switch) TQueue.t
 
-  let spawn id =
+  let spawn id priority =
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       (* Filter arguments for slaves. *)
@@ -123,9 +123,9 @@ module Make(T : Task) () = struct
         | [] -> !async_proofs_flags_for_workers @
                 ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                 CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+                 CoqworkmgrApi.(string_of_priority priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs"|"-batch")::tl ->
+        | "-emacs"::tl ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
@@ -155,8 +155,8 @@ module Make(T : Task) () = struct
       let args =
         Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
       let env = Array.append (T.extra_env ()) (Unix.environment ()) in
-    let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
-    Worker.spawn ~env worker_name args in
+      let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+      Worker.spawn ~env worker_name args in
     name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
 
   let manager cpanel (id, proc, ic, oc) =
@@ -262,7 +262,7 @@ module Make(T : Task) () = struct
     cleaner : Thread.t option;
   }
 
-  let create size =
+  let create size priority =
     let cleaner queue =
       while true do
         try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue)
@@ -270,7 +270,7 @@ module Make(T : Task) () = struct
       done in
     let queue = TQueue.create () in
     {
-      active = Pool.create queue ~size;
+      active = Pool.create queue ~size priority;
       queue;
       cleaner = if size > 0 then Some (CThread.create cleaner queue) else None;
     }
@@ -369,8 +369,8 @@ module Make(T : Task) () = struct
      (TQueue.wait_until_n_are_waiting_then_snapshot
        (Pool.n_workers active) queue)
 
-  let with_n_workers n f =
-    let q = create n in
+  let with_n_workers n priority f =
+    let q = create n priority in
     try let rc = f q in destroy q; rc
     with e -> let e = CErrors.push e in destroy q; iraise e
 
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a9a215acc8..e6cf6343c8 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -68,10 +68,10 @@ module type Task = sig
   type request
   type response
 
-  (** UID of the task kind, for -toploop *)
+  (** UID of the task kind *)
   val name : string ref
 
-  (** Extra arguments of the task kind, for -toploop *)
+  (** Extra arguments of the task kind *)
   val extra_env : unit -> string array
 
   (** {5 Master API, it is run by the master, on a thread} *)
@@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig
   (** [queue] is the abstract queue type. *)
   type queue
 
-  (** [create n] will initialize the queue with [n] workers. If [n] is
-      0, the queue won't spawn any process, working in a lazy local
-      manner. [not imposed by the this API] *)
-  val create : int -> queue
+  (** [create n pri] will initialize the queue with [n] workers having
+      priority [pri]. If [n] is 0, the queue won't spawn any process,
+      working in a lazy local manner. [not imposed by the this API] *)
+  val create : int -> CoqworkmgrApi.priority -> queue
 
   (** [destroy q] Deallocates [q], cancelling all pending tasks. *)
   val destroy : queue -> unit
@@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig
   (** [clear q] Clears [q], only if the worker prool is empty *)
   val clear : queue -> unit
 
-  (** [with_n_workers n f] create a queue, run the function, destroy
+  (** [with_n_workers n pri f] creates a queue, runs the function, destroys
       the queue. The user should call join *)
-  val with_n_workers : int -> (queue -> 'a) -> 'a
+  val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a
 
 end
 
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index c21f057742..92dc77172f 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -13,7 +13,8 @@ let debug = false
 type priority = Low | High
 
 (* Default priority *)
-let async_proofs_worker_priority = ref Low
+
+let default_async_proofs_worker_priority = Low
 
 let string_of_priority = function Low -> "low" | High -> "high"
 let priority_of_string = function
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index d53af84071..29eba5bc91 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -15,7 +15,7 @@ val string_of_priority : priority -> string
 val priority_of_string : string -> priority
 
 (* Default priority *)
-val async_proofs_worker_priority : priority ref
+val default_async_proofs_worker_priority : priority
 
 (* Connects to a work manager if any. If no worker manager, then
    -async-proofs-j and -async-proofs-tac-j are used *)
diff --git a/stm/stm.ml b/stm/stm.ml
index ceb62582cd..4db4579e38 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,6 +51,8 @@ module AsyncOpts = struct
     async_proofs_tac_error_resilience : tac_error_filter;
     async_proofs_cmd_error_resilience : bool;
     async_proofs_delegation_threshold : float;
+
+    async_proofs_worker_priority : CoqworkmgrApi.priority;
   }
 
   let default_opts = {
@@ -67,6 +69,8 @@ module AsyncOpts = struct
     async_proofs_tac_error_resilience = `Only [ "curly" ];
     async_proofs_cmd_error_resilience = true;
     async_proofs_delegation_threshold = 0.03;
+
+    async_proofs_worker_priority = CoqworkmgrApi.Low;
   }
 
   let cur_opt = ref default_opts
@@ -1636,7 +1640,7 @@ and Slaves : sig
   val wait_all_done : unit -> unit
 
   (* initialize the whole machinery (optional) *)
-  val init : unit -> unit
+  val init : CoqworkmgrApi.priority -> unit
 
   type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list
   val dump_snapshot : unit -> Future.UUID.t tasks
@@ -1658,11 +1662,11 @@ end = struct (* {{{ *)
   module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
 
   let queue = ref None
-  let init () =
+  let init priority =
     if async_proofs_is_master !cur_opt then
-      queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers)
+      queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers priority)
     else
-      queue := Some (TaskQueue.create 0)
+      queue := Some (TaskQueue.create 0 priority)
 
   let check_task_aux extra name l i =
     let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
@@ -1978,7 +1982,7 @@ and Partac : sig
 
   val vernac_interp :
     solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch ->
-    int -> Stateid.t -> Stateid.t -> aast -> unit
+    int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit
 
 end = struct (* {{{ *)
 
@@ -1990,7 +1994,7 @@ end = struct (* {{{ *)
     else
       f ()
 
-  let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
+  let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
     { indentation; verbose; expr = e; strlen } : unit
   =
     let e, time, batch, fail =
@@ -2003,7 +2007,7 @@ end = struct (* {{{ *)
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
-    TaskQueue.with_n_workers nworkers (fun queue ->
+    TaskQueue.with_n_workers nworkers priority (fun queue ->
     PG_compat.map_proof (fun p ->
       let Proof.{goals} = Proof.data p in
       let open TacTask in
@@ -2118,7 +2122,7 @@ end (* }}} *)
 
 and Query : sig
 
-  val init : unit -> unit
+  val init : CoqworkmgrApi.priority -> unit
   val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t ->  Stateid.t -> aast -> unit
 
 end = struct (* {{{ *)
@@ -2132,7 +2136,7 @@ end = struct (* {{{ *)
     TaskQueue.enqueue_task (Option.get !queue)
       QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
 
-  let init () = queue := Some (TaskQueue.create 0)
+  let init priority = queue := Some (TaskQueue.create 0 priority)
 
 end (* }}} *)
 
@@ -2410,7 +2414,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
             resilient_tactic id cblock (fun () ->
               reach ~cache:true view.next;
               Partac.vernac_interp ~solve ~abstract ~cancel_switch
-                !cur_opt.async_proofs_n_tacworkers view.next id x)
+                !cur_opt.async_proofs_n_tacworkers
+                !cur_opt.async_proofs_worker_priority view.next id x)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
         when async_proofs_is_master !cur_opt -> (fun () ->
@@ -2679,10 +2684,10 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
-  Slaves.init ();
+  Slaves.init stm_options.async_proofs_worker_priority;
   if async_proofs_is_master !cur_opt then begin
     stm_prerr_endline (fun () -> "Initializing workers");
-    Query.init ();
+    Query.init stm_options.async_proofs_worker_priority;
     let opts = match !cur_opt.async_proofs_private_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
diff --git a/stm/stm.mli b/stm/stm.mli
index 92a782d965..29e4b02e3f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -34,6 +34,8 @@ module AsyncOpts : sig
     async_proofs_tac_error_resilience : tac_error_filter;
     async_proofs_cmd_error_resilience : bool;
     async_proofs_delegation_threshold : float;
+
+    async_proofs_worker_priority : CoqworkmgrApi.priority;
   }
 
   val default_opts : stm_opt
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 15c6510f7c..f77ced2f3a 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -19,7 +19,7 @@ type 'a cpanel = {
 module type PoolModel = sig
   (* this shall come from a Spawn.* model *)
   type process
-  val spawn : int -> worker_id * process * CThread.thread_ic * out_channel
+  val spawn : int -> CoqworkmgrApi.priority -> worker_id * process * CThread.thread_ic * out_channel
 
   (* this defines the main loop of the manager *)
   type extra
@@ -79,20 +79,20 @@ let locking { lock; pool = p } f =
     x
   with e -> Mutex.unlock lock; raise e
 
-let rec create_worker extra pool id =
+let rec create_worker extra pool priority id =
   let cancel = ref false in
-  let name, process, ic, oc as worker = Model.spawn id in
+  let name, process, ic, oc as worker = Model.spawn id priority in
   master_handshake name ic oc;
-  let exit () = cancel := true; cleanup pool; Thread.exit () in
+  let exit () = cancel := true; cleanup pool priority; Thread.exit () in
   let cancelled () = !cancel in
   let cpanel = { exit; cancelled; extra } in
   let manager = CThread.create (Model.manager cpanel) worker in
   { name; cancel; manager; process }
   
-and cleanup x = locking x begin fun { workers; count; extra_arg } ->
+and cleanup x priority = locking x begin fun { workers; count; extra_arg } ->
   workers := List.map (function
     | { cancel } as w when !cancel = false -> w
-    | _ -> let n = !count in incr count; create_worker extra_arg x n)
+    | _ -> let n = !count in incr count; create_worker extra_arg x priority n)
   !workers
 end
 
@@ -102,7 +102,7 @@ end
 
 let is_empty x = locking x begin fun { workers } -> !workers = [] end
 
-let create extra_arg ~size = let x = {
+let create extra_arg ~size priority = let x = {
     lock = Mutex.create ();
     pool = {
       extra_arg;
@@ -110,7 +110,7 @@ let create extra_arg ~size = let x = {
       count = ref size;
   }} in
   locking x begin fun { workers } ->
-     workers := CList.init size (create_worker extra_arg x)
+     workers := CList.init size (create_worker extra_arg x priority)
   end;
   x
 
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index 5a6c968993..5468a24959 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -19,7 +19,8 @@ type 'a cpanel = {
 module type PoolModel = sig
   (* this shall come from a Spawn.* model *)
   type process
-  val spawn : int -> worker_id * process * CThread.thread_ic * out_channel
+  val spawn : int -> CoqworkmgrApi.priority ->
+    worker_id * process * CThread.thread_ic * out_channel
 
   (* this defines the main loop of the manager *)
   type extra
@@ -31,7 +32,7 @@ module Make(Model : PoolModel) : sig
 
   type pool
   
-  val create : Model.extra -> size:int -> pool
+  val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool
 
   val is_empty : pool -> bool
   val n_workers : pool -> int
diff --git a/topbin/coqproofworker_bin.ml b/topbin/coqproofworker_bin.ml
index baf76582ac..2715406b13 100644
--- a/topbin/coqproofworker_bin.ml
+++ b/topbin/coqproofworker_bin.ml
@@ -11,4 +11,4 @@
 module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
 
 let () =
-  WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+  WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqproofworker"
diff --git a/topbin/coqqueryworker_bin.ml b/topbin/coqqueryworker_bin.ml
index 0f7005e422..225158e064 100644
--- a/topbin/coqqueryworker_bin.ml
+++ b/topbin/coqqueryworker_bin.ml
@@ -10,4 +10,4 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 
-let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqqueryworker"
diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml
index 19a8cde88a..962028e0e7 100644
--- a/topbin/coqtacticworker_bin.ml
+++ b/topbin/coqtacticworker_bin.ml
@@ -10,4 +10,4 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
 
-let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker"
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index e6255a947e..d8a3dbb4bb 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -20,6 +20,16 @@ let fatal_error msg =
 (******************************************************************************)
 (* Interactive Load File Simulation                                           *)
 (******************************************************************************)
+
+let load_init_file opts ~state =
+  if opts.pre.load_rcfile then
+    Topfmt.(in_phase ~phase:LoadingRcFile) (fun () ->
+        Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
+  else begin
+    Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
+    state
+  end
+
 let load_vernacular opts ~state =
   List.fold_left
     (fun state (f_in, echo) ->
@@ -29,19 +39,12 @@ let load_vernacular opts ~state =
       if !Flags.beautify
       then Flags.with_option Flags.beautify_file load_vernac f_in
       else load_vernac s
-    ) state (List.rev opts.load_vernacular_list)
+    ) state (List.rev opts.pre.load_vernacular_list)
 
 let load_init_vernaculars opts ~state =
-  let state =
-    if opts.load_rcfile then
-      Topfmt.(in_phase ~phase:LoadingRcFile) (fun () ->
-          Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) ()
-    else begin
-      Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
-      state
-    end in
-
-  load_vernacular opts ~state
+  let state = load_init_file opts ~state in
+  let state = load_vernacular opts ~state in
+  state
 
 (******************************************************************************)
 (* File Compilation                                                           *)
@@ -99,8 +102,8 @@ let compile opts copts ~echo ~f_in ~f_out =
   in
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
-  let stm_options = opts.stm_flags in
-  let output_native_objects = match opts.native_compiler with
+  let stm_options = opts.config.stm_flags in
+  let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
   in
   match copts.compilation_mode with
@@ -115,7 +118,7 @@ let compile opts copts ~echo ~f_in ~f_out =
           Stm.{ doc_type = VoDoc long_f_dot_vo;
                 iload_path; require_libs; stm_options;
               } in
-      let state = { doc; sid; proof = None; time = opts.time } in
+      let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
@@ -161,7 +164,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                 iload_path; require_libs; stm_options;
               } in
 
-      let state = { doc; sid; proof = None; time = opts.time } in
+      let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 7e3759f177..eb0331d95e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -40,52 +40,63 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type option_command = OptionSet of string option | OptionUnset
 
-type t = {
+type coqargs_logic_config = {
+  impredicative_set : Declarations.set_predicativity;
+  indices_matter    : bool;
+  toplevel_name     : Stm.interactive_top;
+  allow_sprop       : bool;
+  cumulative_sprop  : bool;
+}
 
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  diffs_set   : bool;
+  time        : bool;
+  glob_opt    : bool;
+  print_emacs : bool;
+  set_options : (Goptions.option_name * option_command) list;
+}
+
+type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
-  rcfile      : string option;
 
   ml_includes : Loadpath.coq_path list;
   vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
-  toplevel_name : Stm.interactive_top;
-
   load_vernacular_list : (string * bool) list;
-  batch : bool;
-
-  color : color;
-
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter : bool;
-  enable_VM : bool;
-  native_compiler : native_compiler;
-  allow_sprop : bool;
-  cumulative_sprop : bool;
-
-  set_options : (Goptions.option_name * option_command) list;
 
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  diffs_set   : bool;
-  time        : bool;
+  inputstate  : string option;
+}
 
-  filter_opts : bool;
+type coqargs_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of Usage.specific_usage
 
-  glob_opt    : bool;
+type coqargs_main =
+  | Queries of coqargs_query list
+  | Run
 
+type coqargs_post = {
   memory_stat : bool;
-  print_tags  : bool;
-  print_where : bool;
-  print_config: bool;
   output_context : bool;
+}
 
-  print_emacs : bool;
-
-  inputstate  : string option;
-
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
 }
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
@@ -95,69 +106,71 @@ let default_native =
   then NativeOn {ondemand=true}
   else NativeOff
 
-let default = {
-
-  load_init   = true;
-  load_rcfile = true;
-  rcfile      = None;
-
-  ml_includes = [];
-  vo_includes = [];
-  vo_requires = [];
-
-  toplevel_name = Stm.TopLogical default_toplevel;
-
-  load_vernacular_list = [];
-  batch = false;
-
-  color = `AUTO;
-
+let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
-  enable_VM = true;
-  native_compiler = default_native;
+  toplevel_name = Stm.TopLogical default_toplevel;
   allow_sprop = false;
   cumulative_sprop = false;
+}
 
-  set_options = [];
-
+let default_config = {
+  logic        = default_logic_config;
+  rcfile       = None;
+  coqlib       = None;
+  color        = `AUTO;
+  enable_VM    = true;
+  native_compiler = default_native;
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
   time         = false;
+  glob_opt     = false;
+  print_emacs  = false;
+  set_options  = [];
 
-  filter_opts  = false;
+  (* Quiet / verbosity options should be here *)
+}
 
-  glob_opt     = false;
+let default_pre = {
+  load_init    = true;
+  load_rcfile  = true;
+  ml_includes  = [];
+  vo_includes  = [];
+  vo_requires  = [];
+  load_vernacular_list = [];
+  inputstate   = None;
+}
+
+let default_queries = []
 
+let default_post = {
   memory_stat  = false;
-  print_tags   = false;
-  print_where  = false;
-  print_config = false;
   output_context = false;
+}
 
-  print_emacs = false;
-
-  (* Quiet / verbosity options should be here *)
-
-  inputstate  = None;
+let default = {
+  config = default_config;
+  pre    = default_pre;
+  main   = Run;
+  post   = default_post;
 }
 
 (******************************************************************************)
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
+  Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }}
 
 let add_vo_include opts unix_path coq_path implicit =
   let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
-  { opts with vo_includes = {
+  { opts with pre = { opts.pre with vo_includes = {
         recursive = true;
-        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.vo_includes }
+        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
-  { opts with vo_requires = (d, p, export) :: opts.vo_requires }
+  { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
 
 let add_compat_require opts v =
   match v with
@@ -166,19 +179,28 @@ let add_compat_require opts v =
   | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
 
 let add_load_vernacular opts verb s =
-  { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list }
+  { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
 
 (** Options for proof general *)
 let set_emacs opts =
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `EMACS; print_emacs = true }
+  { opts with config = { opts.config with color = `OFF; print_emacs = true }}
+
+let set_logic f oval =
+  { oval with config = { oval.config with logic = f oval.config.logic }}
 
 let set_color opts = function
-| "yes" | "on" -> { opts with color = `ON }
-| "no" | "off" -> { opts with color = `OFF }
-| "auto" -> { opts with color = `AUTO }
-| _ ->
-  error_wrong_arg ("Error: on/off/auto expected after option color")
+  | "yes" | "on" -> { opts with config = { opts.config with color = `ON }}
+  | "no" | "off" -> { opts with config = { opts.config with color = `OFF }}
+  | "auto" -> { opts with config = { opts.config with color = `AUTO }}
+  | _ ->
+    error_wrong_arg ("Error: on/off/auto expected after option color")
+
+let set_query opts q =
+  { opts with main = match opts.main with
+  | Run -> Queries (default_queries@[q])
+  | Queries queries -> Queries (queries@[q])
+  }
 
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
@@ -190,9 +212,7 @@ let warn_deprecated_simple_require =
 
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
-  { opts with inputstate = Some s }
-
-let exitcode opts = if opts.filter_opts then 2 else 0
+  { opts with pre = { opts.pre with inputstate = Some s }}
 
 (******************************************************************************)
 (* Parsing helpers                                                            *)
@@ -261,26 +281,9 @@ let parse_option_set opt =
     let v = String.sub opt (eqi+1) (len - eqi - 1) in
     to_opt_key (String.sub opt 0 eqi), Some v
 
-(*s Parsing of the command line.
-    We no longer use [Arg.parse], in order to use share [Usage.print_usage]
-    between coqtop and coqc. *)
-
-let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
-    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
-
-exception NoCoqLib
-
-let usage help =
-  begin
-    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
-    with NoCoqLib -> usage_no_coqlib ()
-  end;
-  let lp = Coqinit.toplevel_init_load_path () in
-  (* Necessary for finding the toplevels below *)
-  List.iter Loadpath.add_coq_path lp;
-  help ()
-
 (* Main parsing routine *)
+(*s Parsing of the command line *)
+
 let parse_args ~help ~init arglist : t * string list =
   let args = ref arglist in
   let extras = ref [] in
@@ -320,54 +323,55 @@ let parse_args ~help ~init arglist : t * string list =
 
     (* Options with one arg *)
     |"-coqlib" ->
-      Envars.set_user_coqlib (next ());
-      oval
+      { oval with config = { oval.config with coqlib = Some (next ())
+      }}
 
     |"-async-proofs" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
-      }}
+      }}}
     |"-async-proofs-j" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
-      }}
+      }}}
     |"-async-proofs-cache" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-tac-j" ->
       let j = get_int opt (next ()) in
       if j <= 0 then begin
         error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
       end;
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_n_tacworkers = j
-      }}
+      }}}
 
     |"-async-proofs-worker-priority" ->
-      CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ());
-      oval
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
+        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
+      }}}
 
     |"-async-proofs-private-flags" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
-      }}
+      }}}
 
     |"-async-proofs-tactic-error-resilience" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-command-error-resilience" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
-      }}
+      }}}
 
     |"-async-proofs-delegation-threshold" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
-      }}
+      }}}
 
     |"-worker-id" -> set_worker_id opt (next ()); oval
 
@@ -378,7 +382,7 @@ let parse_args ~help ~init arglist : t * string list =
 
     |"-dump-glob" ->
       Dumpglob.dump_into_file (next ());
-      { oval with glob_opt = true }
+      { oval with config = { oval.config with glob_opt = true }}
 
     |"-feedback-glob" ->
       Dumpglob.feedback_glob (); oval
@@ -387,7 +391,7 @@ let parse_args ~help ~init arglist : t * string list =
       System.exclude_directory (next ()); oval
 
     |"-init-file" ->
-      { oval with rcfile = Some (next ()); }
+      { oval with config = { oval.config with rcfile = Some (next ()); }}
 
     |"-inputstate"|"-is" ->
       set_inputstate oval (next ())
@@ -441,10 +445,10 @@ let parse_args ~help ~init arglist : t * string list =
       let topname = Libnames.dirpath_of_string (next ()) in
       if Names.DirPath.is_empty topname then
         CErrors.user_err Pp.(str "Need a non empty toplevel module name");
-      { oval with toplevel_name = Stm.TopLogical topname }
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}}
 
     |"-topfile" ->
-      { oval with toplevel_name = Stm.TopPhysical (next()) }
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}}
 
     |"-main-channel" ->
       Spawned.main_channel := get_host_port opt (next()); oval
@@ -462,7 +466,7 @@ let parse_args ~help ~init arglist : t * string list =
         oval
 
     |"-bytecode-compiler" ->
-      { oval with enable_VM = get_bool opt (next ()) }
+      { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }}
 
     |"-native-compiler" ->
 
@@ -479,68 +483,63 @@ let parse_args ~help ~init arglist : t * string list =
         | _ ->
           error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler")
       in
-      { oval with native_compiler }
+      { oval with config = { oval.config with native_compiler }}
 
     | "-set" ->
       let opt = next() in
       let opt, v = parse_option_set opt in
-      { oval with set_options = (opt, OptionSet v) :: oval.set_options }
+      { oval with config = { oval.config with set_options = (opt, OptionSet v) :: oval.config.set_options }}
 
     | "-unset" ->
       let opt = next() in
       let opt = to_opt_key opt in
-      { oval with set_options = (opt, OptionUnset) :: oval.set_options }
+      { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }}
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
     |"-async-proofs-never-reopen-branch" ->
-      { oval with stm_flags = { oval.stm_flags with
+      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_never_reopen_branch = true
-      }}
-    |"-batch" ->
-      Flags.quiet := true;
-      { oval with batch = true }
+      }}}
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
-    |"-config"|"--config" -> { oval with print_config = true }
+    |"-config"|"--config" -> set_query oval PrintConfig
     |"-debug" -> Coqinit.set_debug (); oval
     |"-diffs" -> let opt = next () in
                   if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
                     Proof_diffs.write_diffs_option opt
                   else
                     error_wrong_arg "Error: on|off|removed expected after -diffs";
-                  { oval with diffs_set = true }
+                  { oval with config = { oval.config with diffs_set = true }}
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
-    |"-filteropts" -> { oval with filter_opts = true }
     |"-impredicative-set" ->
-      { oval with impredicative_set = Declarations.ImpredicativeSet }
-    |"-allow-sprop" -> { oval with allow_sprop = true }
-    |"-disallow-sprop" -> { oval with allow_sprop = false }
-    |"-sprop-cumulative" -> { oval with cumulative_sprop = true }
-    |"-indices-matter" -> { oval with indices_matter = true }
-    |"-m"|"--memory" -> { oval with memory_stat = true }
-    |"-noinit"|"-nois" -> { oval with load_init = false }
-    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true }
-    |"-output-context" -> { oval with output_context = true }
+      set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
+    |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval
+    |"-disallow-sprop" -> set_logic (fun o -> { o with allow_sprop = false }) oval
+    |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval
+    |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
+    |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
+    |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }}
+    |"-output-context" -> { oval with post = { oval.post with output_context = true }}
     |"-profile-ltac" -> Flags.profile_ltac := true; oval
-    |"-q" -> { oval with load_rcfile = false; }
+    |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
     |"-quiet"|"-silent" ->
       Flags.quiet := true;
       Flags.make_warn false;
       oval
-    |"-list-tags" -> { oval with print_tags = true }
-    |"-time" -> { oval with time = true }
+    |"-list-tags" -> set_query oval PrintTags
+    |"-time" -> { oval with config = { oval.config with time = true }}
     |"-type-in-type" -> set_type_in_type (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
-    |"-where" -> { oval with print_where = true }
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval
-    |"-v"|"--version" -> Usage.version (exitcode oval)
-    |"-print-version"|"--print-version" ->
-      Usage.machine_readable_version (exitcode oval)
+    |"-where" -> set_query oval PrintWhere
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
+    |"-v"|"--version" -> set_query oval PrintVersion
+    |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
 
     (* Unknown option *)
     | s ->
@@ -560,11 +559,11 @@ let parse_args ~help ~init arglist : t * string list =
 let prelude_data = "Prelude", Some "Coq", Some false
 
 let require_libs opts =
-  if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
+  if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
 let cmdline_load_path opts =
-  List.rev opts.vo_includes @ List.(rev opts.ml_includes)
+  List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes)
 
 let build_load_path opts =
-  Coqinit.libs_init_load_path ~load_init:opts.load_init @
+  Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
   cmdline_load_path opts
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 81f8983e98..e414888861 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -16,57 +16,69 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type option_command = OptionSet of string option | OptionUnset
 
-type t = {
+type coqargs_logic_config = {
+  impredicative_set : Declarations.set_predicativity;
+  indices_matter    : bool;
+  toplevel_name     : Stm.interactive_top;
+  allow_sprop       : bool;
+  cumulative_sprop  : bool;
+}
+
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  diffs_set   : bool;
+  time        : bool;
+  glob_opt    : bool;
+  print_emacs : bool;
+  set_options : (Goptions.option_name * option_command) list;
+}
 
+type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
-  rcfile      : string option;
 
   ml_includes : Loadpath.coq_path list;
   vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
-
-  toplevel_name : Stm.interactive_top;
+  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
-  batch : bool;
-
-  color : color;
-
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter : bool;
-  enable_VM : bool;
-  native_compiler : native_compiler;
-  allow_sprop : bool;
-  cumulative_sprop : bool;
-
-  set_options : (Goptions.option_name * option_command) list;
-
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  diffs_set   : bool;
-  time        : bool;
+  inputstate  : string option;
+}
 
-  filter_opts : bool;
+type coqargs_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of Usage.specific_usage
 
-  glob_opt    : bool;
+type coqargs_main =
+  | Queries of coqargs_query list
+  | Run
 
+type coqargs_post = {
   memory_stat : bool;
-  print_tags  : bool;
-  print_where : bool;
-  print_config: bool;
   output_context : bool;
+}
 
-  print_emacs : bool;
-
-  inputstate  : string option;
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
 }
 
 (* Default options *)
 val default : t
 
-val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
-val exitcode : t -> int
+val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
+val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
 val build_load_path : t -> Loadpath.coq_path list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index a04552e8db..5678acb2b1 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -8,32 +8,37 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let set_noninteractive_mode () =
-  Flags.quiet := true;
-  System.trust_file_cache := true
-
 let outputstate opts =
   Option.iter (fun ostate_file ->
     let fname = CUnix.make_suffix ostate_file ".coq" in
     States.extern_state fname) opts.Coqcargs.outputstate
 
-let coqc_main () =
-  (* Careful because init_toplevel will call Summary.init_summaries,
-     thus options such as `quiet` have to be set after the main
-     initialisation is run. *)
-  let coqc_init ~opts args =
-    set_noninteractive_mode ();
-    let opts, args = Coqtop.(coqtop_toplevel.init) ~opts args in
-    opts, args
-  in
-  let opts, extras =
-    Topfmt.(in_phase ~phase:Initialization)
-      Coqtop.(init_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in
-
-  let copts = Coqcargs.parse extras in
+let coqc_init _copts ~opts =
+  Flags.quiet := true;
+  System.trust_file_cache := true;
+  Coqtop.init_color opts.Coqargs.config;
+  if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ()
 
-  if not opts.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
+let coqc_specific_usage = Usage.{
+  executable_name = "coqc";
+  extra_args = "file...";
+  extra_options = "\n\
+coqc specific options:\
+\n  -o f.vo                use f.vo as the output file name\
+\n  -verbose               compile and output the input file\
+\n  -quick                 quickly compile .v files to .vio files (skip proofs)\
+\n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
+\n                         into fi.vo\
+\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
+\n                         proofs in each fi.vio\
+\n\
+\nUndocumented:\
+\n  -vio2vo                [see manual]\
+\n  -check-vio-tasks       [see manual]\
+\n"
+}
 
+let coqc_main copts ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
     Ccompile.compile_files opts copts;
 
@@ -47,16 +52,16 @@ let coqc_main () =
 
   flush_all();
 
-  if opts.Coqargs.output_context then begin
+  if opts.Coqargs.post.Coqargs.output_context then begin
     let sigma, env = let e = Global.env () in Evd.from_env e, e in
     Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
   end;
   CProfile.print_profile ()
 
-let main () =
+let coqc_run copts ~opts () =
   let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   try
-    coqc_main ();
+    coqc_main ~opts copts;
     exit 0
   with exn ->
     flush_all();
@@ -64,3 +69,14 @@ let main () =
     flush_all();
     let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
     exit exit_code
+
+let custom_coqc = Coqtop.{
+  parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
+  help = coqc_specific_usage;
+  init = coqc_init;
+  run = coqc_run;
+  opts = Coqargs.default;
+}
+
+let main () =
+  Coqtop.start_coq custom_coqc
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4bcde566e3..f6211102e6 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -444,7 +444,7 @@ let drop_args = ref None
 let loop ~opts ~state =
   drop_args := Some opts;
   let open Coqargs in
-  print_emacs := opts.print_emacs;
+  print_emacs := opts.config.print_emacs;
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder coqloop_feed in
   if Dumpglob.dump () then begin
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e43e6a8da4..f09d202edf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -11,6 +11,9 @@
 open Pp
 open Coqargs
 
+(** This file provides generic support for Coq executables + specific
+    support for the coqtop executable *)
+
 let () = at_exit flush_all
 
 let ( / ) = Filename.concat
@@ -30,25 +33,18 @@ let print_header () =
   Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
-let memory_stat = ref false
 let print_memory_stat () =
-  begin (* -m|--memory from the command-line *)
-    if !memory_stat then
-    Feedback.msg_notice
-      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
-  end;
-  begin
-    (* operf-macro interface:
-       https://github.com/OCamlPro/operf-macro *)
-    try
-      let fn = Sys.getenv "OCAML_GC_STATS" in
-      let oc = open_out fn in
-      Gc.print_stat oc;
-      close_out oc
-    with _ -> ()
-  end
-
-let _ = at_exit print_memory_stat
+  (* -m|--memory from the command-line *)
+  Feedback.msg_notice
+    (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
+  (* operf-macro interface:
+     https://github.com/OCamlPro/operf-macro *)
+  try
+    let fn = Sys.getenv "OCAML_GC_STATS" in
+    let oc = open_out fn in
+    Gc.print_stat oc;
+    close_out oc
+  with _ -> ()
 
 let interp_set_option opt v old =
   let open Goptions in
@@ -159,6 +155,14 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
+let print_query opts = function
+  | PrintVersion -> Usage.version ()
+  | PrintMachineReadableVersion -> Usage.machine_readable_version ()
+  | PrintWhere -> print_endline (Envars.coqlib ())
+  | PrintHelp h -> Usage.print_usage stderr h
+  | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
+  | PrintTags -> print_style_tags opts.config
+
 (** GC tweaking *)
 
 (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
@@ -184,123 +188,155 @@ let init_gc () =
              Gc.minor_heap_size = 33554432; (* 4M *)
              Gc.space_overhead = 120}
 
-(** Main init routine *)
-let init_toplevel ~help ~init custom_init arglist =
+let init_setup = function
+  | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+  | Some s -> Envars.set_user_coqlib s
+
+let init_process () =
   (* Coq's init process, phase 1:
      OCaml parameters, basic structures, and IO
    *)
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-
-  Lib.init();
-
+  Lib.init ()
+
+let init_parse parse_extra help init_opts =
+  let opts, extras =
+    parse_args ~help:help ~init:init_opts
+      (List.tl (Array.to_list Sys.argv)) in
+  let customopts, extras = parse_extra ~opts extras in
+  if not (CList.is_empty extras) then begin
+    prerr_endline ("Don't know what to do with "^String.concat " " extras);
+    prerr_endline "See -help for the list of supported options";
+    exit 1
+    end;
+  opts, customopts
+
+let init_execution opts custom_init =
   (* Coq's init process, phase 2:
      Basic Coq environment, load-path, plugins.
    *)
-  let opts, extras = parse_args ~help ~init arglist in
-  memory_stat := opts.memory_stat;
-
   (* If we have been spawned by the Spawn module, this has to be done
    * early since the master waits us to connect back *)
   Spawned.init_channels ();
-  Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-  if opts.print_where then begin
-    print_endline (Envars.coqlib ());
-    exit (exitcode opts)
-  end;
-  if opts.print_config then begin
-    Envars.print_config stdout Coq_config.all_src_dirs;
-    exit (exitcode opts)
-  end;
-  if opts.print_tags then begin
-    print_style_tags opts;
-    exit (exitcode opts)
-  end;
-  if opts.filter_opts then begin
-    print_string (String.concat "\n" extras);
-    exit 0;
-  end;
+  if opts.post.memory_stat then at_exit print_memory_stat;
   let top_lp = Coqinit.toplevel_init_load_path () in
   List.iter Loadpath.add_coq_path top_lp;
-  let opts, extras = custom_init ~opts extras in
+  CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
+  (* Configuration *)
+  Global.set_engagement opts.config.logic.impredicative_set;
+  Global.set_indices_matter opts.config.logic.indices_matter;
+  Global.set_VM opts.config.enable_VM;
+  Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
+  Global.set_allow_sprop opts.config.logic.allow_sprop;
+  if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative ();
 
-  Global.set_engagement opts.impredicative_set;
-  Global.set_indices_matter opts.indices_matter;
-  Global.set_VM opts.enable_VM;
-  Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
-  Global.set_allow_sprop opts.allow_sprop;
-  if opts.cumulative_sprop then Global.make_sprop_cumulative ();
-
-  set_options opts.set_options;
+  set_options opts.config.set_options;
 
   (* Allow the user to load an arbitrary state here *)
-  inputstate opts;
+  inputstate opts.pre;
 
   (* This state will be shared by all the documents *)
   Stm.init_core ();
+  custom_init ~opts
+
+type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
+
+type ('a,'b) custom_toplevel =
+  { parse_extra : 'a extra_args_fn
+  ; help : Usage.specific_usage
+  ; init : 'a -> opts:Coqargs.t -> 'b
+  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
+  ; opts : Coqargs.t
+  }
 
+(** Main init routine *)
+let init_toplevel custom =
+  let () = init_process () in
+  let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in
+  let () = init_setup opts.config.coqlib in
+  (* Querying or running? *)
+  match opts.main with
+  | Queries q -> List.iter (print_query opts) q; exit 0
+  | Run ->
+    let customstate = init_execution opts (custom.init customopts) in
+    opts, customopts, customstate
+
+let init_document opts =
   (* Coq init process, phase 3: Stm initialization, backtracking state.
 
      It is essential that the module system is in a consistent
      state before we take the first snapshot. This was not
      guaranteed in the past, but now is thanks to the STM API.
   *)
-  opts, extras
-
-type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
-
-type custom_toplevel =
-  { init : init_fn
-  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
-  ; opts : Coqargs.t
-  }
-
-
-let init_toploop opts =
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
-  let stm_options = opts.stm_flags in
+  let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
-           { doc_type = Interactive opts.toplevel_name;
+           { doc_type = Interactive opts.config.logic.toplevel_name;
              iload_path; require_libs; stm_options;
            }) in
-  let state = { doc; sid; proof = None; time = opts.time } in
-  Ccompile.load_init_vernaculars opts ~state, opts
-
-let coqtop_init ~opts extra =
-  init_color opts;
-  CoqworkmgrApi.(init !async_proofs_worker_priority);
-  Flags.if_verbose print_header ();
-  opts, extra
-
-let coqtop_toplevel =
-  { init = coqtop_init
-  ; run = Coqloop.loop
-  ; opts = Coqargs.default
-  }
+  { doc; sid; proof = None; time = opts.config.time }
 
 let start_coq custom =
   let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   (* Init phase *)
-  let state, opts =
-    try
-      let opts, extras =
-        init_toplevel
-          ~help:Usage.print_usage_coqtop ~init:default custom.init
-          (List.tl (Array.to_list Sys.argv)) in
-      if not (CList.is_empty extras) then begin
-        prerr_endline ("Don't know what to do with "^String.concat " " extras);
-        prerr_endline "See -help for the list of supported options";
-        exit 1
-      end;
-      init_toploop opts
+  let opts, custom_opts, state =
+    try init_toplevel custom
     with any ->
       flush_all();
       fatal_error_exn any in
   Feedback.del_feeder init_feeder;
-  if not opts.batch then custom.run ~opts ~state;
-  exit 0
+  (* Run phase *)
+  custom.run ~opts custom_opts state
+
+(** ****************************************)
+(** Specific support for coqtop executable *)
+
+type run_mode = Interactive | Batch
+
+let init_toploop opts =
+  let state = init_document opts in
+  let state = Ccompile.load_init_vernaculars opts ~state in
+  state
+
+let coqtop_init run_mode ~opts =
+  if run_mode = Batch then Flags.quiet := true;
+  init_color opts.config;
+  Flags.if_verbose print_header ();
+  init_toploop opts
+
+let coqtop_parse_extra ~opts extras =
+  let rec parse_extra run_mode = function
+  | "-batch" :: rest -> parse_extra Batch rest
+  | x :: rest ->
+    let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest
+  | [] -> run_mode, [] in
+  let run_mode, extras = parse_extra Interactive extras in
+  run_mode, extras
+
+let coqtop_run run_mode ~opts state =
+  match run_mode with
+  | Interactive -> Coqloop.loop ~opts ~state;
+  | Batch -> exit 0
+
+let coqtop_specific_usage = Usage.{
+  executable_name = "coqtop";
+  extra_args = "";
+  extra_options = "\n\
+coqtop specific options:\n\
+\n  -batch                 batch mode (exits after interpretation of command line)\
+\n"
+}
+
+let coqtop_toplevel =
+  { parse_extra = coqtop_parse_extra
+  ; help = coqtop_specific_usage
+  ; init = coqtop_init
+  ; run = coqtop_run
+  ; opts = Coqargs.default
+  }
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 40f569a1c8..4fe7d538a8 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -13,29 +13,33 @@
     [run] launches a custom toplevel.
 *)
 
-type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
+type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
-type custom_toplevel =
-  { init : init_fn
-  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+type ('a,'b) custom_toplevel =
+  { parse_extra : 'a extra_args_fn
+  ; help : Usage.specific_usage
+  ; init : 'a -> opts:Coqargs.t -> 'b
+  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
   ; opts : Coqargs.t
   }
 
-(** [init_toplevel ~help ~init custom_init arg_list]
-    Common Coq initialization and argument parsing *)
-val init_toplevel
-  :  help:(unit -> unit)
-  -> init:Coqargs.t
-  -> init_fn
-  -> string list
-  -> Coqargs.t * string list
-
-val coqtop_toplevel : custom_toplevel
-
-(** The Coq main module. [start custom] will parse the command line,
+(** The generic Coq main module. [start custom] will parse the command line,
    print the banner, initialize the load path, load the input state,
    load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch
    [custom.run]. *)
+val start_coq : ('a,'b) custom_toplevel -> unit
+
+(** Initializer color for output *)
+
+val init_color : Coqargs.coqargs_config -> unit
+
+(** Prepare state for interactive loop *)
+
+val init_toploop : Coqargs.t -> Vernac.State.t
+
+(** The specific characterization of the coqtop_toplevel *)
+
+type run_mode = Interactive | Batch
 
-val start_coq : custom_toplevel -> unit
+val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 91b3c32126..cdb2e36fbd 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -8,21 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let version ret =
+let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
     Coq_config.version Coq_config.date;
-  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version;
-  exit ret
-let machine_readable_version ret =
+  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
+
+let machine_readable_version () =
   Printf.printf "%s %s\n"
-    Coq_config.version Coq_config.caml_version;
-  exit ret
+    Coq_config.version Coq_config.caml_version
 
 (* print the usage of coqtop (or coqc) on channel co *)
 
-let extra_usage = ref []
-let add_to_usage name text = extra_usage := (name,text) :: !extra_usage
-
 let print_usage_common co command =
   output_string co command;
   output_string co "Coq options are:\n";
@@ -99,42 +95,16 @@ let print_usage_common co command =
 \n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
 \n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
 \n  -h, -help, --help      print this list of options\
-\n";
-  List.iter (fun (name, text) ->
-    output_string co
-     ("\nWith the flag '-toploop "^name^
-        "' these extra option are also available:\n"^
-      text^"\n"))
-    !extra_usage
+\n"
 
-(* print the usage on standard error *)
+(* print the usage *)
 
-let print_usage_coqtop () =
-  print_usage_common stderr "Usage: coqtop <options>\n\n";
-  output_string stderr "\n\
-coqtop specific options:\
-\n\
-\n  -batch                 batch mode (exits just after argument parsing)\
-\n";
-  flush stderr ;
-  exit 1
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
 
-let print_usage_coqc () =
-  print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
-  output_string stderr "\n\
-coqc specific options:\
-\n\
-\n  -o f.vo                use f.vo as the output file name\
-\n  -verbose               compile and output the input file\
-\n  -quick                 quickly compile .v files to .vio files (skip proofs)\
-\n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
-\n                         into fi.vo\
-\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
-\n                         proofs in each fi.vio\
-\n\
-\nUndocumented:\
-\n  -vio2vo                [see manual]\
-\n  -check-vio-tasks       [see manual]\
-\n";
-  flush stderr ;
-  exit 1
+let print_usage co { executable_name; extra_args; extra_options } =
+  print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
+  output_string co extra_options
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 1f257a5896..536cbdc6b2 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -8,15 +8,22 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** {6 Prints the version number on the standard output and exits (with 0). } *)
+(** {6 Prints the version number on the standard output. } *)
 
-val version : int -> 'a
-val machine_readable_version : int -> 'a
+val version : unit -> unit
+val machine_readable_version : unit -> unit
 
-(** {6 Enable toploop plugins to insert some text in the usage message. } *)
-val add_to_usage : string -> string -> unit
+(** {6 extra arguments or options to print when asking usage for a
+     given executable. } *)
 
-(** {6 Prints the usage on the error output. } *)
-val print_usage_coqtop : unit -> unit
-val print_usage_coqc : unit -> unit
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
+
+(** {6 Prints the generic part and specific part of usage for a
+       given executable. } *)
+
+val print_usage : out_channel -> specific_usage -> unit
 
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index d362f9db22..5f80ac475c 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -13,18 +13,28 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let arg_init init ~opts extra_args =
-  let extra_args = parse extra_args in
+let worker_parse_extra ~opts extra_args =
+  (), parse extra_args
+
+let worker_init init () ~opts =
   Flags.quiet := true;
   init ();
-  CoqworkmgrApi.(init !async_proofs_worker_priority);
-  opts, extra_args
+  Coqtop.init_toploop opts
+
+let worker_specific_usage name = Usage.{
+  executable_name = name;
+  extra_args = "";
+  extra_options = ("\n" ^ name ^ " specific options:\
+\n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\n");
+}
 
-let start ~init ~loop =
+let start ~init ~loop name =
   let open Coqtop in
   let custom = {
+    parse_extra = worker_parse_extra;
+    help = worker_specific_usage name;
     opts = Coqargs.default;
-    init = arg_init init;
-    run = (fun ~opts:_ ~state:_ -> loop ());
+    init = worker_init init;
+    run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
   } in
   start_coq custom
diff --git a/toplevel/workerLoop.mli b/toplevel/workerLoop.mli
index 685a10f6f3..8d6f0b1988 100644
--- a/toplevel/workerLoop.mli
+++ b/toplevel/workerLoop.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Register a STM worker *)
+(* Register a STM worker of a given executable name *)
 val start :
   init:(unit -> unit) ->
-  loop:(unit -> unit) -> unit
+  loop:(unit -> unit) -> string -> unit