[stm] Make toplevels standalone executables.

We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:

- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.

In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:

- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.

11 files changed, 108 insertions, 120 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 17e848c5a..5c1ffd784 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -52,7 +52,6 @@ type coq_cmdopts = {
   compilation_mode : compilation_mode;
 
   toplevel_name : Names.DirPath.t;
-  toploop : string option;
 
   compile_list: (string * bool) list;  (* bool is verbosity  *)
   compilation_output_name : string option;
@@ -81,6 +80,8 @@ type coq_cmdopts = {
   print_config: bool;
   output_context : bool;
 
+  print_emacs : bool;
+
   inputstate  : string option;
   outputstate : string option;
 
@@ -100,7 +101,6 @@ let init_args = {
   compilation_mode = BuildVo;
 
   toplevel_name = Names.(DirPath.make [Id.of_string "Top"]);
-  toploop = None;
 
   compile_list = [];
   compilation_output_name = None;
@@ -129,6 +129,8 @@ let init_args = {
   print_config = false;
   output_context = false;
 
+  print_emacs = false;
+
   inputstate  = None;
   outputstate = None;
 }
@@ -191,11 +193,8 @@ let set_vio_checking_j opts opt j =
 
 (** Options for proof general *)
 let set_emacs opts =
-  if not (Option.is_empty opts.toploop) then
-    CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop");
-  Coqloop.print_emacs := true;
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `OFF }
+  { opts with color = `OFF; print_emacs = true }
 
 let set_color opts = function
 | "yes" | "on" -> { opts with color = `ON }
@@ -310,12 +309,9 @@ let usage batch =
   let lp = Coqinit.toplevel_init_load_path () in
   (* Necessary for finding the toplevels below *)
   List.iter Mltop.add_coq_path lp;
-  if batch then Usage.print_usage_coqc ()
-  else begin
-    Mltop.load_ml_objects_raw_rex
-      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
-    Usage.print_usage_coqtop ()
-  end
+  if batch
+  then Usage.print_usage_coqc ()
+  else Usage.print_usage_coqtop ()
 
 (* Main parsing routine *)
 let parse_args arglist : coq_cmdopts * string list =
@@ -401,7 +397,7 @@ let parse_args arglist : coq_cmdopts * string list =
       }}
 
     |"-async-proofs-worker-priority" ->
-      WorkerLoop.async_proofs_worker_priority := get_priority opt (next ());
+      CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ());
       oval
 
     |"-async-proofs-private-flags" ->
@@ -500,11 +496,6 @@ let parse_args arglist : coq_cmdopts * string list =
       let oval = add_compile oval false (next ()) in
       { oval with compilation_mode = Vio2Vo }
 
-    |"-toploop" ->
-      if !Coqloop.print_emacs then
-        CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible");
-      { oval with toploop = Some (next ()) }
-
     |"-w" | "-W" ->
       let w = next () in
       if w = "none" then
@@ -538,12 +529,7 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
-    |"-ideslave" ->
-      if !Coqloop.print_emacs then
-        CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
-      Flags.ide_slave := true;
-      { oval with toploop = Some "coqidetop" }
-
+    |"-ideslave" -> Flags.ide_slave := true; oval
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
     |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index de9b6a682..9fb6219a6 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -27,7 +27,6 @@ type coq_cmdopts = {
   compilation_mode : compilation_mode;
 
   toplevel_name : Names.DirPath.t;
-  toploop : string option;
 
   compile_list: (string * bool) list;  (* bool is verbosity  *)
   compilation_output_name : string option;
@@ -56,6 +55,8 @@ type coq_cmdopts = {
   print_config: bool;
   output_context : bool;
 
+  print_emacs : bool;
+
   inputstate  : string option;
   outputstate : string option;
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3e7a83085..e61f830f3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -75,16 +75,12 @@ let ml_path_if c p =
   let f x = { recursive = false; path_spec = MlPath x } in
   if c then List.map f p else []
 
-(* LoadPath for toploop toplevels *)
+(* LoadPath for developers *)
 let toplevel_init_load_path () =
   let coqlib = Envars.coqlib () in
   (* NOTE: These directories are searched from last to first *)
   (* first, developer specific directory to open *)
-  ml_path_if Coq_config.local [coqlib/"dev"] @
-
-  (* main loops *)
-  ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @
-  ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"]
+  ml_path_if Coq_config.local [coqlib/"dev"]
 
 (* LoadPath for Coq user libraries *)
 let libs_init_load_path ~load_init =
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index da9169514..d7ede1c2e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -410,3 +410,25 @@ let rec loop ~state =
                 str (Printexc.to_string any)) ++ spc () ++
          hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."));
       loop ~state
+
+(* Default toplevel loop *)
+let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
+
+let drop_args = ref None
+let loop ~opts ~state =
+  drop_args := Some opts;
+  let open Coqargs in
+  print_emacs := opts.print_emacs;
+  (* We initialize the console only if we run the toploop_run *)
+  let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in
+  if Dumpglob.dump () then begin
+    Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
+    Dumpglob.noglob ()
+  end;
+  let _ = loop ~state in
+  (* Initialise and launch the Ocaml toplevel *)
+  Coqinit.init_ocaml_path();
+  Mltop.ocaml_toploop();
+  (* We delete the feeder after the OCaml toploop has ended so users
+     of Drop can see the feedback. *)
+  Feedback.del_feeder tl_feed
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 6d9867fb9..5c07a8bf3 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -10,9 +10,6 @@
 
 (** The Coq toplevel loop. *)
 
-(** -emacs option: printing includes emacs tags. *)
-val print_emacs : bool ref
-
 (** A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
@@ -32,8 +29,9 @@ val set_prompt : (unit -> string) -> unit
 (** Toplevel feedback printer. *)
 val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit
 
-(** Main entry point of Coq: read and execute vernac commands. *)
-val loop : state:Vernac.State.t -> Vernac.State.t
-
 (** Last document seen after `Drop` *)
 val drop_last_doc : Vernac.State.t option ref
+val drop_args : Coqargs.coq_cmdopts option ref
+
+(** Main entry point of Coq: read and execute vernac commands. *)
+val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 809490166..e979d0e54 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -30,8 +30,6 @@ let print_header () =
   Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
-let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
-
 (* Feedback received in the init stage, this is different as the STM
    will not be generally be initialized, thus stateid, etc... may be
    bogus. For now we just print to the console too *)
@@ -41,23 +39,6 @@ let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude
 
 let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile
 
-(* Default toplevel loop *)
-let console_toploop_run opts ~state =
-  (* We initialize the console only if we run the toploop_run *)
-  let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in
-  if Dumpglob.dump () then begin
-    Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
-    Dumpglob.noglob ()
-  end;
-  let _ = Coqloop.loop ~state in
-  (* Initialise and launch the Ocaml toplevel *)
-  Coqinit.init_ocaml_path();
-  Mltop.ocaml_toploop();
-  (* We let the feeder in place for users of Drop *)
-  Feedback.del_feeder tl_feed
-
-let toploop_run = ref console_toploop_run
-
 let memory_stat = ref false
 let print_memory_stat () =
   begin (* -m|--memory from the command-line *)
@@ -387,12 +368,6 @@ let init_color color_mode =
   else
     Topfmt.init_terminal_output ~color:false
 
-let toploop_init = ref begin fun opts x ->
-  let () = init_color opts.color in
-  let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in
-  opts, x
-  end
-
 let print_style_tags opts =
   let () = init_color opts.color in
   let tags = Topfmt.dump_tags () in
@@ -435,7 +410,7 @@ let init_gc () =
              Gc.space_overhead = 120}
 
 (** Main init routine *)
-let init_toplevel arglist =
+let init_toplevel custom_init arglist =
   (* Coq's init process, phase 1:
      OCaml parameters, basic structures, and IO
    *)
@@ -475,8 +450,7 @@ let init_toplevel arglist =
       end;
       let top_lp = Coqinit.toplevel_init_load_path () in
       List.iter Mltop.add_coq_path top_lp;
-      Option.iter Mltop.load_ml_object_raw opts.toploop;
-      let opts, extras = !toploop_init opts extras in
+      let opts, extras = custom_init ~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";
@@ -540,11 +514,23 @@ let init_toplevel arglist =
   Feedback.del_feeder !init_feeder;
   res
 
-let start () =
-  match init_toplevel (List.tl (Array.to_list Sys.argv)) with
+type custom_toplevel = {
+  init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list;
+  run : opts:coq_cmdopts -> state:Vernac.State.t -> unit;
+}
+
+let coqtop_init ~opts extra =
+  init_color opts.color;
+  CoqworkmgrApi.(init !async_proofs_worker_priority);
+  opts, extra
+
+let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; }
+
+let start_coq custom =
+  match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with
   (* Batch mode *)
   | Some state, opts when not opts.batch_mode ->
-    !toploop_run opts ~state;
+    custom.run ~opts ~state;
     exit 1
   | _ , opts ->
     flush_all();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index fcc569ca0..641448f10 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -8,16 +8,21 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** The Coq main module. The following function [start] 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 [Coqloop.loop]. *)
+(** Definition of custom toplevels.
+    [init] is used to do custom command line argument parsing.
+    [run] launches a custom toplevel.
+*)
+type custom_toplevel = {
+  init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list;
+  run  : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit;
+}
 
-val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts
+val coqtop_toplevel : custom_toplevel
 
-val start : unit -> unit
+(** The 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]. *)
 
-(* For other toploops *)
-val toploop_init :
-  (Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list) ref
-val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref
+val start_coq : custom_toplevel -> unit
diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml
deleted file mode 100644
index 0b65cebbb..000000000
--- a/toplevel/coqtop_byte_bin.ml
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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 drop_setup () =
-  begin try
-    (* Enable rectypes in the toplevel if it has the directive #rectypes *)
-    begin match Hashtbl.find Toploop.directive_table "rectypes" with
-      | Toploop.Directive_none f -> f ()
-      | _ -> ()
-    end
-    with
-    | Not_found -> ()
-  end;
-  let ppf = Format.std_formatter in
-  Mltop.(set_top
-           { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
-                          then CErrors.user_err Pp.(str ("Could not load plugin "^f))
-                        );
-             use_file = Topdirs.dir_use ppf;
-             add_dir  = Topdirs.dir_directory;
-             ml_loop  = (fun () -> Toploop.loop ppf);
-           })
-
-(* Main coqtop initialization *)
-let _ =
-  drop_setup ();
-  Coqtop.start()
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 78b96e5e2..597173e5f 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,7 +1,8 @@
 Vernac
 Usage
-G_toplevel
-Coqloop
 Coqinit
 Coqargs
+G_toplevel
+Coqloop
 Coqtop
+WorkerLoop
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
new file mode 100644
index 000000000..ee6d5e884
--- /dev/null
+++ b/toplevel/workerLoop.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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 rec parse = function
+  | "--xml_format=Ppcmds" :: rest -> parse rest
+  | x :: rest -> x :: parse rest
+  | [] -> []
+
+let arg_init init ~opts extra_args =
+  let extra_args = parse extra_args in
+  Flags.quiet := true;
+  init ();
+  CoqworkmgrApi.(init !async_proofs_worker_priority);
+  opts, extra_args
+
+let start ~init ~loop =
+  let open Coqtop in
+  let custom = {
+    init = arg_init init;
+    run = (fun ~opts:_ ~state:_ -> loop ());
+  } in
+  start_coq custom
diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/workerLoop.mli
index ea4c0ea52..e497dee6d 100644
--- a/toplevel/coqtop_opt_bin.ml
+++ b/toplevel/workerLoop.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let drop_setup () = Mltop.remove ()
-
-(* Main coqtop initialization *)
-let _ =
-  drop_setup ();
-  Coqtop.start()
+(* Register a STM worker *)
+val start :
+  init:(unit -> unit) ->
+  loop:(unit -> unit) -> unit