[stm] Make toplevels standalone executables.

We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:

- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.

In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:

- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.

1 files changed, 22 insertions, 17 deletions

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)