Some common points between coqc and other coq binaries.

- Binding coqc execution to the generic support for Coq binaries
  (i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
  can avoid to call it. By the way, it is unclear what workerloop
  should do with it. Also, it is unclear how much the -l option should
  be considered an coqidetop or coq*worker option. In any case, it
  should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
  phase. Seems ok, despites the few involved side effects.

4 files changed, 71 insertions, 64 deletions

diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 603d4118b5..fd275fdb1b 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -8,34 +8,18 @@
 (*         *     (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 =
-    set_noninteractive_mode ();
-    Coqtop.(coqtop_toplevel.init) ~opts in
-  let custom_coqc = Coqtop.{
-      coqtop_toplevel with
-      help = Usage.print_usage_coqc;
-      init = coqc_init;
-      parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
-    } in
-  let opts, copts =
-    Topfmt.(in_phase ~phase:Initialization)
-      Coqtop.init_toplevel custom_coqc in
-
-  if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
+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 ()
 
+let coqc_main copts ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
     Ccompile.compile_files opts copts;
 
@@ -55,10 +39,10 @@ let coqc_main () =
   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();
@@ -66,3 +50,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 = Usage.print_usage_coqc;
+  init = coqc_init;
+  run = coqc_run;
+  opts = Coqargs.default;
+}
+
+let main () =
+  Coqtop.start_coq custom_coqc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 560ba35a42..770698bee8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -232,7 +232,6 @@ let init_execution opts custom_init =
   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;
-  custom_init ~opts;
   CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
@@ -249,15 +248,16 @@ let init_execution opts custom_init =
   inputstate opts.pre;
 
   (* This state will be shared by all the documents *)
-  Stm.init_core ()
+  Stm.init_core ();
+  custom_init ~opts
 
 type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
-type 'a custom_toplevel =
+type ('a,'b) custom_toplevel =
   { parse_extra : 'a extra_args_fn
   ; help : unit -> unit
-  ; init : opts:Coqargs.t -> unit
-  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+  ; init : 'a -> opts:Coqargs.t -> 'b
+  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
   ; opts : Coqargs.t
   }
 
@@ -270,8 +270,8 @@ let init_toplevel custom =
   match opts.main with
   | Queries q -> print_queries opts q; exit 0
   | Run ->
-    let () = init_execution opts custom.init in
-    opts, customopts
+    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.
@@ -291,32 +291,33 @@ let init_document opts =
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
-let init_toploop opts =
-  let state = init_document opts in
-  let state = Ccompile.load_init_vernaculars opts ~state in
-  state
-
-type run_mode = Interactive | Batch
-
 let start_coq custom =
   let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   (* Init phase *)
-  let run_mode, state, opts =
-    try
-      let opts, run_mode = init_toplevel custom in
-      let state = init_toploop opts in
-      run_mode, state, opts
+  let opts, custom_opts, state =
+    try init_toplevel custom
     with any ->
       flush_all();
       fatal_error_exn any in
   Feedback.del_feeder init_feeder;
-  match run_mode with
-  | Interactive -> custom.run ~opts ~state;
-  | Batch -> exit 0
+  (* Run phase *)
+  custom.run ~opts custom_opts state
+
+(** ****************************************)
+(** Specific support for coqtop executable *)
 
-let coqtop_init ~opts =
+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 ()
+  Flags.if_verbose print_header ();
+  init_toploop opts
 
 let coqtop_parse_extra ~opts extras =
   let rec parse_extra run_mode = function
@@ -327,10 +328,15 @@ let coqtop_parse_extra ~opts extras =
   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_toplevel =
   { parse_extra = coqtop_parse_extra
   ; help = Usage.print_usage_coqtop
   ; init = coqtop_init
-  ; run = Coqloop.loop
+  ; run = coqtop_run
   ; opts = Coqargs.default
   }
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 4a86dc1b5a..e2339afbde 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,26 +15,31 @@
 
 type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
-type 'a custom_toplevel =
+type ('a,'b) custom_toplevel =
   { parse_extra : 'a extra_args_fn
   ; help : unit -> unit
-  ; init : opts:Coqargs.t -> unit
-  ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
+  ; init : 'a -> opts:Coqargs.t -> 'b
+  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
   ; opts : Coqargs.t
   }
 
-(** [init_toplevel custom]
-    Customized Coq initialization and argument parsing *)
-val init_toplevel : 'a custom_toplevel -> Coqargs.t * 'a
-
-type run_mode = Interactive | Batch
-
 (** 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 : run_mode custom_toplevel -> unit
+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 *)
-val coqtop_toplevel : run_mode custom_toplevel
+
+type run_mode = Interactive | Batch
+
+val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index c2bd8213b0..0087e4833c 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -14,11 +14,12 @@ let rec parse = function
   | [] -> []
 
 let worker_parse_extra ~opts extra_args =
-  Coqtop.Interactive, parse extra_args
+  (), parse extra_args
 
-let worker_init init ~opts =
+let worker_init init () ~opts =
   Flags.quiet := true;
-  init ()
+  init ();
+  Coqtop.init_toploop opts
 
 let start ~init ~loop =
   let open Coqtop in
@@ -27,6 +28,6 @@ let start ~init ~loop =
     help = (fun _ -> output_string stderr "Same options as coqtop");
     opts = Coqargs.default;
     init = worker_init init;
-    run = (fun ~opts:_ ~state:_ -> loop ());
+    run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
   } in
   start_coq custom