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

42 files changed, 256 insertions, 224 deletions

diff --git a/.merlin b/.merlin
index 40db60950..404a7e793 100644
--- a/.merlin
+++ b/.merlin
@@ -32,6 +32,8 @@ S vernac
 B vernac
 S toplevel
 B toplevel
+S topbin
+B topbin
 S plugins/ltac
 B plugins/ltac
 S API
diff --git a/CHANGES b/CHANGES
index 3030e3311..aea7ec2f6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,18 @@ Tactic language
   called by OCaml-defined tactics.
 - Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
+Coq binaries and process model
+
+- Before 8.9, Coq distributed a single `coqtop` binary and a set of
+  dynamically loadable plugins that used to take over the main loop
+  for tasks such as IDE language server or parallel proof checking.
+
+  These plugins have been turned into full-fledged binaries so each
+  different process has associated a particular binary now, in
+  particular `coqidetop` is the CoqIDE language server, and
+  `coq{proof,tactic,query}worker` are in charge of task-specific and
+  parallel proof checking.
+
 Changes from 8.8.0 to 8.8.1
 ===========================
 
diff --git a/Makefile b/Makefile
index f914de5a6..61b2f5cd9 100644
--- a/Makefile
+++ b/Makefile
@@ -214,7 +214,7 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(CHICKENBYTE)
+	rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE)
 	find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
@@ -245,7 +245,7 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(CHICKEN)
+	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBIN)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
diff --git a/Makefile.build b/Makefile.build
index 179ca28b6..b19841a37 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -383,29 +383,34 @@ grammar/%.cmi: grammar/%.mli
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbyte: $(TOPBYTE) $(CHICKENBYTE)
 
-coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
-
-COQTOP_OPT=toplevel/coqtop_opt_bin.ml
-COQTOP_BYTE=toplevel/coqtop_byte_bin.ml
+# Special rule for coqtop
+$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
+	cp $< $@
 
-ifeq ($(BEST),opt)
-$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT)
+bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
 	                   -I kernel/byterun/ -cclib -lcoqrun \
 			   $(SYSMOD) -package camlp5.gramlib \
-			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $(COQTOP_OPT) -o $@
+			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
-else
-$(COQTOPEXE): $(COQTOPBYTE)
-	cp $< $@
-endif
 
+bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
+	$(SHOW)'COQMKTOP -o $@'
+	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \
+	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
+			 $(SYSMOD) -package camlp5.gramlib \
+			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
+
+COQTOP_BYTE=topbin/coqtop_byte_bin.ml
+
+# Special rule for coqtop.byte
 # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
-$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE)
+$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
@@ -477,7 +482,7 @@ COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -package str,unix,threads)
+	$(HIDE)$(call bestocaml, -package str)
 
 $(COQTEX): $(call bestobj, tools/coq_tex.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
@@ -506,9 +511,9 @@ FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
  ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo	\
  tools/fake_ide.cmo
 
-$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
+$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I ide -package str,unix,threads)
+	$(HIDE)$(call bestocaml, -I ide -package str -package dynlink)
 
 # votour: a small vo explorer (based on the checker)
 
diff --git a/Makefile.common b/Makefile.common
index 9493acd1f..372c31475 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -14,8 +14,11 @@
 # Executables
 ###########################################################################
 
-COQTOPBYTE:=bin/coqtop.byte$(EXE)
+TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
+TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE))
+
 COQTOPEXE:=bin/coqtop$(EXE)
+COQTOPBYTE:=bin/coqtop.byte$(EXE)
 
 COQDEP:=bin/coqdep$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
@@ -107,8 +110,6 @@ CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
         stm/stm.cma toplevel/toplevel.cma
 
-TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
-
 GRAMMARCMA:=grammar/grammar.cma
 
 ###########################################################################
diff --git a/Makefile.ide b/Makefile.ide
index ac4ba75d4..eca0f20d4 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -45,7 +45,9 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
 IDEDEPS:=clib/clib.cma lib/lib.cma
 IDECMA:=ide/ide.cma
-IDETOPLOOPCMA=ide/coqidetop.cma
+IDETOPEXE=bin/coqidetop$(EXE)
+IDETOP=bin/coqidetop.opt$(EXE)
+IDETOPBYTE=bin/coqidetop.byte$(EXE)
 
 LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml
 LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml
@@ -88,15 +90,15 @@ endif
 
 coqide-files: $(IDEFILES)
 
-ide-byteloop: $(IDETOPLOOPCMA)
-ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs)
-ide-toploop: ide-$(BEST)loop
+ide-byteloop: $(IDETOPBYTE)
+ide-optloop: $(IDETOP)
+ide-toploop: $(IDETOPEXE)
 
 ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
-		lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP) $@
 else
 $(COQIDE): $(COQIDEBYTE)
@@ -105,8 +107,8 @@ endif
 
 $(COQIDEBYTE): $(LINKIDE)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
-	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
 ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here
 	$(SHOW)'CAMLP5O   $<'
@@ -135,6 +137,29 @@ ide/ideutils.cmx: ide/ideutils.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $<
 
+IDETOPCMA:=ide/ide_common.cma
+IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa)
+
+# Special rule for coqidetop
+$(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
+	cp $< $@
+
+$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
+	$(SHOW)'COQMKTOP -o $@'
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \
+	                   -I kernel/byterun/ -cclib -lcoqrun \
+			   $(SYSMOD) -package camlp5.gramlib \
+			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
+	$(STRIP) $@
+	$(CODESIGN) $@
+
+$(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
+	$(SHOW)'COQMKTOP -o $@'
+	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide \
+	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
+			 $(SYSMOD) -package camlp5.gramlib \
+			 $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@
+
 ####################
 ## Install targets
 ####################
@@ -164,13 +189,11 @@ install-ide-bin:
 
 install-ide-toploop:
 ifeq ($(BEST),opt)
-	$(MKDIR) $(FULLCOQLIB)/toploop/
-	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+	$(INSTALLBIN) $(IDETOPEXE) $(IDETOP) $(FULLBINDIR)
 endif
 install-ide-toploop-byte:
 ifneq ($(BEST),opt)
-	$(MKDIR) $(FULLCOQLIB)/toploop/
-	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+	$(INSTALLBIN) $(IDETOPEXE) $(IDETOPBYTE) $(FULLBINDIR)
 endif
 
 install-ide-devfiles:
@@ -206,8 +229,7 @@ $(COQIDEAPP)/Contents:
 $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-		unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
-		threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	        -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP) $@
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
diff --git a/Makefile.install b/Makefile.install
index 02695287b..0764b61fc 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -70,17 +70,11 @@ endif
 
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
-	$(MKDIR) $(FULLCOQLIB)/toploop
-ifeq ($(BEST),opt)
-	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
-endif
+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
 
 install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR)
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
+	$(INSTALLBIN) $(TOPBYTE) $(FULLBINDIR)
 	$(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS)
 ifndef CUSTOM
 	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
diff --git a/configure.ml b/configure.ml
index d4750700b..45c3bb67a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -16,8 +16,9 @@ let coq_macos_version = "8.7.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8791
 let state_magic = 58791
-let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
-"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
+let distributed_exec =
+  ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
+   "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
 
diff --git a/dev/base_include b/dev/base_include
index 2f7183dd6..2f5d8aa84 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -231,7 +231,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
 let _ =
  print_string
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d04b9637c..2ac4d2167 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
 
 git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 
-( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+   COQOCAMLLIB="$COQBIN/../lib/"
+   COQLIB="$COQBIN/../lib/coq/"
+else
+   COQOCAMLLIB="$COQBIN/../"
+   COQLIB="$COQBIN/../"
+fi
 
-echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
+( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+
+echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
new file mode 100644
index 000000000..ca0076b46
--- /dev/null
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+    pidetop_CI_BRANCH=stm+top
+    pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+fi
diff --git a/ide/coqidetop.mllib b/ide/ide_common.mllib
index df988d8f1..050c282ef 100644
--- a/ide/coqidetop.mllib
+++ b/ide/ide_common.mllib
@@ -5,4 +5,3 @@ Serialize
 Richpp
 Xmlprotocol
 Document
-Ide_slave
diff --git a/ide/ide_slave.ml b/ide/idetop.ml
index 6c7ca4f8e..e40af003b 100644
--- a/ide/ide_slave.ml
+++ b/ide/idetop.ml
@@ -457,7 +457,7 @@ let msg_format = ref (fun () ->
 
 (* The loop ignores the command line arguments as the current model delegates
    its handing to the toplevel container. *)
-let loop _args ~state =
+let loop ~opts:_ ~state =
   let open Vernac.State in
   set_doc state.doc;
   init_signal_handler ();
@@ -506,13 +506,16 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let () = Coqtop.toploop_init := (fun coq_args extra_args ->
-        let args = parse extra_args in
-        CoqworkmgrApi.(init High);
-        coq_args, args)
-
-let () = Coqtop.toploop_run := loop
-
 let () = Usage.add_to_usage "coqidetop"
 "  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
+
+let islave_init ~opts extra_args =
+  let args = parse extra_args in
+  CoqworkmgrApi.(init High);
+  opts, args
+
+let () =
+  let open Coqtop in
+  let custom = { init = islave_init; run = loop; } in
+  start_coq custom
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94a..e96b99299 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -289,16 +289,10 @@ let coqtop_path () =
     | Some s -> s
     | None ->
       match cmd_coqtop#get with
-	| Some s -> s
-	| None ->
-	  try
-            let old_prog = Sys.executable_name in
-            let pos = String.length old_prog - 6 in
-            let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
-            in
-            let new_prog = Bytes.of_string old_prog in
-            Bytes.blit_string "coqtop" 0 new_prog i 6;
-            let new_prog = Bytes.to_string new_prog in
+      | Some s -> s
+      | None ->
+        try
+          let new_prog = System.get_toplevel_path "coqidetop" in
             if Sys.file_exists new_prog then new_prog
 	    else
 	      let in_macos_bundle =
@@ -306,8 +300,8 @@ let coqtop_path () =
 		  (Filename.dirname new_prog)
 		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
-		 else "coqtop"
-	  with Not_found -> "coqtop"
+                 else "coqidetop"
+        with Not_found -> "coqidetop"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe
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
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index b3e1500ae..0105f821e 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -120,12 +120,11 @@ module Make(T : Task) () = struct
     let proc, ic, oc =
       let rec set_slave_opt = function
         | [] -> !async_proofs_flags_for_workers @
-                ["-toploop"; !T.name^"top";
-                 "-worker-id"; name;
+                ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
+                   CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
         | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vio2vo"
+        | ("-async-proofs" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -134,7 +133,8 @@ module Make(T : Task) () = struct
       let args =
         Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
       let env = Array.append (T.extra_env ()) (Unix.environment ()) in
-    Worker.spawn ~env Sys.argv.(0) args in
+    let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+    Worker.spawn ~env worker_name args in
     name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
 
   let manager cpanel (id, proc, ic, oc) =
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 36b5d18ab..841cc08c0 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -11,6 +11,10 @@
 let debug = false
 
 type priority = Low | High
+
+(* Default priority *)
+let async_proofs_worker_priority = ref Low
+
 let string_of_priority = function Low -> "low" | High -> "high"
 let priority_of_string = function
   | "low" -> Low
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 2983b619d..be5b29177 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -14,6 +14,9 @@ type priority = Low | High
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
 
+(* Default priority *)
+val async_proofs_worker_priority : priority ref
+
 (* Connects to a work manager if any. If no worker manager, then
    -async-proofs-j and -async-proofs-tac-j are used *)
 val init : priority -> unit
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
deleted file mode 100644
index f9f6c22d5..000000000
--- a/stm/proofworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Proofworkertop
diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib
deleted file mode 100644
index c2f73089b..000000000
--- a/stm/queryworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Queryworkertop
diff --git a/stm/stm.ml b/stm/stm.ml
index 20409c25e..6b92e4737 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1849,7 +1849,7 @@ end = struct (* {{{ *)
     | RespError of Pp.t
     | RespNoProgress
 
-  let name = ref "tacworker"
+  let name = ref "tacticworker"
   let extra_env () = [||]
   type competence = unit
   type worker_status = Fresh | Old of competence
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 72b538016..4b254e811 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,7 +5,6 @@ TQueue
 WorkerPool
 Vernac_classifier
 CoqworkmgrApi
-WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib
deleted file mode 100644
index db38fde27..000000000
--- a/stm/tacworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Tacworkertop
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;
diff --git a/stm/proofworkertop.ml b/topbin/coqproofworker_bin.ml
index 4b85a05ac..7ae91cfbd 100644
--- a/stm/proofworkertop.ml
+++ b/topbin/coqproofworker_bin.ml
@@ -10,7 +10,5 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
 
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
+let () =
+  WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
diff --git a/stm/queryworkertop.ml b/topbin/coqqueryworker_bin.ml
index aa00102aa..98c858121 100644
--- a/stm/queryworkertop.ml
+++ b/topbin/coqqueryworker_bin.ml
@@ -10,7 +10,4 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
diff --git a/stm/tacworkertop.ml b/topbin/coqtacticworker_bin.ml
index 3b91df86e..2634baa83 100644
--- a/stm/tacworkertop.ml
+++ b/topbin/coqtacticworker_bin.ml
@@ -10,7 +10,4 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
 
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
+let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop
diff --git a/toplevel/coqtop_opt_bin.ml b/topbin/coqtop_bin.ml
index ea4c0ea52..4490db59e 100644
--- a/toplevel/coqtop_opt_bin.ml
+++ b/topbin/coqtop_bin.ml
@@ -13,4 +13,4 @@ let drop_setup () = Mltop.remove ()
 (* Main coqtop initialization *)
 let _ =
   drop_setup ();
-  Coqtop.start()
+  Coqtop.(start_coq coqtop_toplevel)
diff --git a/toplevel/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index 0b65cebbb..abe397830 100644
--- a/toplevel/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -31,4 +31,4 @@ let drop_setup () =
 (* Main coqtop initialization *)
 let _ =
   drop_setup ();
-  Coqtop.start()
+  Coqtop.(start_coq coqtop_toplevel)
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/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/stm/workerLoop.ml b/toplevel/workerLoop.ml
index 5130b019a..ee6d5e884 100644
--- a/stm/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -8,18 +8,22 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Default priority *)
-open CoqworkmgrApi
-let async_proofs_worker_priority = ref Low
-
 let rec parse = function
   | "--xml_format=Ppcmds" :: rest -> parse rest
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let loop init coq_args extra_args =
-  let args = parse extra_args in
+let arg_init init ~opts extra_args =
+  let extra_args = parse extra_args in
   Flags.quiet := true;
   init ();
-  CoqworkmgrApi.init !async_proofs_worker_priority;
-  coq_args, args
+  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/ide/ide_slave.mli b/toplevel/workerLoop.mli
index 9db9ecd12..e497dee6d 100644
--- a/ide/ide_slave.mli
+++ b/toplevel/workerLoop.mli
@@ -8,5 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* This empty file avoids a race condition that occurs when compiling a .ml file
-   that does not have a corresponding .mli file *)
+(* Register a STM worker *)
+val start :
+  init:(unit -> unit) ->
+  loop:(unit -> unit) -> unit
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 343b0925d..d25dea141 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -345,13 +345,6 @@ let load_ml_object mname ?path fname=
 
 let dir_ml_load m = ignore(dir_ml_load m)
 let add_known_module m = add_known_module m None
-let load_ml_object_raw fname = dir_ml_load (file_of_name fname)
-let load_ml_objects_raw_rex rex =
-  List.iter (fun (_,fp) ->
-    let name = file_of_name (Filename.basename fp) in
-    try dir_ml_load name
-    with e -> prerr_endline (Printexc.to_string e))
-    (System.where_in_path_rex !coq_mlpath_copy rex)
 
 (* Summary of declared ML Modules *)
 
@@ -396,8 +389,6 @@ let trigger_ml_object verb cache reinit ?path name =
     if cache then perform_cache_obj name
   end
 
-let load_ml_object n m = ignore(load_ml_object n m)
-
 let unfreeze_ml_modules x =
   reset_loaded_modules ();
   List.iter
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index da195f4fc..ed1f9a12d 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -68,9 +68,6 @@ val add_coq_path : coq_path -> unit
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
 val module_is_known : string -> bool
-val load_ml_object : string -> string -> unit
-val load_ml_object_raw : string -> unit
-val load_ml_objects_raw_rex : Str.regexp -> unit
 
 (** {5 Initialization functions} *)