[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, 2 insertions, 14 deletions

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d48c6d0af..47bd2493f 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -297,19 +297,7 @@ let main =
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
   let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
-  let coqtop_name = (* from ide/ideutils.ml *)
-    let prog_name = "fake_ide" in
-    let len_prog_name = String.length prog_name in
-    let fake_ide_path = Sys.executable_name in
-    let fake_ide_path_len = String.length fake_ide_path in
-    let pos = fake_ide_path_len - len_prog_name in
-    let rex = Str.regexp_string prog_name in
-    try
-      let i = Str.search_backward rex fake_ide_path pos in
-      String.sub fake_ide_path 0 i ^ "coqtop" ^
-      String.sub fake_ide_path (i + len_prog_name)
-        (fake_ide_path_len - i - len_prog_name) 
-    with Not_found -> assert false in
+  let idetop_name = System.get_toplevel_path "coqidetop" in
   let coqtop_args, input_file = match Sys.argv with
     | [| _; f |] -> Array.of_list def_args, f
     | [| _; f; ct |] ->
@@ -318,7 +306,7 @@ let main =
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =
-    let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in
+    let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
     let ip = Xml_parser.make (Xml_parser.SChannel cin) in
     let op = Xml_printer.make (Xml_printer.TChannel cout) in
     Xml_parser.check_eof ip false;