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

2 files changed, 24 insertions, 14 deletions

diff --git a/lib/system.ml b/lib/system.ml
index dfede29e8..f109c7192 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -116,18 +116,6 @@ let where_in_path ?(warn=true) path filename =
     let f = Filename.concat lpe filename in
     if file_exists_respecting_case lpe filename then [lpe,f] else []))
 
-let where_in_path_rex path rex =
-  search path (fun lpe ->
-    try
-      let files = Sys.readdir lpe in
-      CList.map_filter (fun name ->
-        try
-          ignore(Str.search_forward rex name 0);
-          Some (lpe,Filename.concat lpe name)
-        with Not_found -> None)
-      (Array.to_list files)
-    with Sys_error _ -> [])
-
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
     (* the name is considered to be a physical name and we use the file
@@ -312,3 +300,9 @@ let with_time ~batch f x =
     let msg2 = if batch then "" else " (failure)" in
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
+
+let get_toplevel_path top =
+  let dir = Filename.dirname Sys.argv.(0) in
+  let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
+  let eff = if Dynlink.is_native then ".opt" else ".byte" in
+  dir ^ Filename.dir_sep ^ top ^ eff ^ exe
diff --git a/lib/system.mli b/lib/system.mli
index 3349dfea3..a34280037 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -50,8 +50,6 @@ val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
 val where_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
-val where_in_path_rex :
-  CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
@@ -107,3 +105,21 @@ val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
+
+(** [get_toplevel_path program] builds a complete path to the
+   executable denoted by [program]. This involves:
+
+   - locating the directory: we don't rely on PATH as to make calls to
+   /foo/bin/coqtop chose the right /foo/bin/coqproofworker
+
+   - adding the proper suffixes: .opt/.byte depending on the current
+   mode, + .exe if in windows.
+
+ Note that this function doesn't check that the executable actually
+ exists. This is left back to caller, as well as the choice of
+ fallback strategy. We could add a fallback strategy here but it is
+ better not to as in most cases if this function fails to construct
+ the right name you want you execution to fail rather than fall into
+ choosing some random binary from the system-wide installation of
+ Coq. *)
+val get_toplevel_path : string -> string