[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.

1 files changed, 22 insertions, 0 deletions

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