Merge PR #6859: [stm] Make toplevels standalone executables.

48 files changed, 271 insertions, 250 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/.travis.yml b/.travis.yml
index 890ee6d7c..8218467d2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -275,7 +275,7 @@ install:
 - opam switch "$COMPILER" && opam update
 - eval $(opam config env)
 - opam config list
-- opam install -j ${NJOBS} -y num camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM}
+- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} jbuilder camlp5${CAMLP5_VER} ${EXTRA_OPAM}
 - opam list
 
 script:
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..5f5eaf3a4 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 $@'
@@ -499,16 +504,16 @@ $(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coq
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
-# a connection to coqtop -ideslave
+# a connection to coqidetop
 
 FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
  ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.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..37f698e0c 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -36,7 +36,7 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 
 # Note : for just building bin/coqide, we could only consider
 # config, lib, ide and ide/utils. But the coqidetop plugin (the
-# one that will be loaded by coqtop -ideslave) refers to some
+# one that will be loaded by coqidetop) refers to some
 # core modules of coq, for instance printing/*.
 
 IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
@@ -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/coq.ml b/ide/coq.ml
index 65456d685..63986935a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -152,7 +152,7 @@ let print_status = function
 let check_connection args =
   let lines = ref [] in
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in
+  let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
   let cmd = requote cmd in
   try
     let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
@@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor =
     else
       "on"
   in
-  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in
   let env =
     match !ideslave_coqtop_flags with
     | None -> None
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..64f165cde 100644
--- a/ide/ide_slave.ml
+++ b/ide/idetop.ml
@@ -18,9 +18,8 @@ open Printer
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
-    function and a rewind function. This specialized loop is triggered
-    when the -ideslave option is passed to Coqtop. *)
+(** Idetop : an implementation of [Interface], i.e. mainly an interp
+    function and a rewind function. *)
 
 
 (** Signal handling: we postpone ^C during input and output phases,
@@ -429,7 +428,7 @@ let eval_call c =
   Xmlprotocol.abstract_eval_call handler c
 
 (** Message dispatching.
-    Since coqtop -ideslave starts 1 thread per slave, and each
+    Since [coqidetop] starts 1 thread per slave, and each
     thread forwards feedback messages from the slave to the GUI on the same
     xml channel, we need mutual exclusion.  The mutex should be per-channel, but
     here we only use 1 channel. *)
@@ -457,7 +456,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 +505,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/flags.ml b/lib/flags.ml
index 56940f1cf..7e0065beb 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -57,8 +57,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let ide_slave = ref false
-
 let raw_print = ref false
 
 let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 17776d68a..02d8a3adc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,9 +52,6 @@ val in_toplevel : bool ref
 
 val profile : bool
 
-(* -ide_slave: printing will be more verbose, will affect stm caching *)
-val ide_slave : bool ref
-
 (* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a258d5052..5485c4bf1 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -11,15 +11,11 @@
 type t = int
 let initial = 1
 let dummy = 0
-let fresh, in_range =
+let fresh =
   let cur = ref initial in
-  (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
+  fun () -> incr cur; !cur
 let to_string = string_of_int
-let of_int id =
-  (* Coqide too to parse ids too, but cannot check if they are valid.
-   * Hence we check for validity only if we are an ide slave. *)
-  if !Flags.ide_slave then assert (in_range id);
-  id
+let of_int id = id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
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..85a7f1495 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)]
-        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vio2vo"
+                   CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+        | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+        | ("-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..016201128 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
+(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
 
 let error s =
   prerr_endline ("fake_id: error: "^s);
@@ -284,7 +284,7 @@ let read_command inc = Parser.parse grammar inc
 
 let usage () =
   error (Printf.sprintf
-    "A fake coqide process talking to a coqtop -ideslave.\n\
+    "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
      Usage: %s (file|-) [<coqtop>]\n\
      Input syntax is the following:\n%s\n"
      (Filename.basename Sys.argv.(0))
@@ -296,20 +296,8 @@ let main =
   if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (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 def_args = ["--xml_format=Ppcmds"] 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..89602c9b5 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,6 @@ 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" }
-
     |"-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} *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f0e41d27c..938e9718a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2243,7 +2243,7 @@ let with_fail st b f =
       | HasNotFailed ->
           user_err ~hdr:"Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info
+          if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end