From f5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 10 Dec 2017 03:31:55 +0100
Subject: [make] remove unneeded generated file "tolink.ml"

When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.

This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.

Fixes #6364.
---
 .gitignore                |  1 -
 Makefile                  |  2 +-
 Makefile.build            | 18 ++++++------------
 doc/refman/RefMan-uti.tex | 11 ++++-------
 toplevel/coqtop_bin.ml    |  6 +-----
 5 files changed, 12 insertions(+), 26 deletions(-)

diff --git a/.gitignore b/.gitignore
index 36536ec96..cec51986d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml
 
 kernel/byterun/coq_jumptbl.h
 kernel/copcodes.ml
-tools/tolink.ml
 ide/index_urls.txt
 .lia.cache
 checker/names.ml
diff --git a/Makefile b/Makefile
index 0078dba20..2637996ed 100644
--- a/Makefile
+++ b/Makefile
@@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
diff --git a/Makefile.build b/Makefile.build
index 3e4c5a0b4..f11719c07 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -386,12 +386,12 @@ $(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $<
 
 ifeq ($(BEST),opt)
-$(COQTOPEXE): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP)
+$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \
 	                   -I kernel/byterun/ -cclib -lcoqrun \
                            $(SYSMOD) -package camlp5.gramlib \
-	                   tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \
+	                   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \
 	                   $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
@@ -401,20 +401,14 @@ $(COQTOPEXE): $(COQTOPBYTE)
 endif
 
 # Are "-cclib lcoqrun -dllib -lcoqrun" necessary?
-$(COQTOPBYTE): tools/tolink.cmo $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
+$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \
+	$(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \
 	                 -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \
                          $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
-	                 tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \
+	                 $(LINKCMO) $(BYTEFLAGS) \
 	                 $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@
 
-tools/tolink.ml: Makefile.build Makefile.common
-	$(SHOW)"ECHO... >" $@
-	$(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@
-	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
-	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
-
 # coqc
 
 COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 002e9625c..962aa98b6 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -12,19 +12,16 @@ linking. Nowadays, the preferred method is to use \texttt{ocamlfind}.
 
 The most basic custom toplevel is built using:
 \begin{quotation}
-\texttt{\% make tools/tolink.cmx}
 \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
-  -package coq.toplevel -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+  -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
 
-For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use:
+For example, to statically link LTAC, you can just do:
 \begin{quotation}
-\texttt{\% make tools/tolink.cmx}
 \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
-  -package coq.toplevel -package coq.ltac -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+  -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
-
-We will remove the need for the \texttt{tolink} file in the future.
+and similarly for other plugins.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml
index 62459003b..56aced92a 100644
--- a/toplevel/coqtop_bin.ml
+++ b/toplevel/coqtop_bin.ml
@@ -1,6 +1,2 @@
 (* Main coqtop initialization *)
-let () =
-  (* XXX: We should make this a configure option *)
-  List.iter Mltop.add_known_module Str.(split (regexp " ") Tolink.static_modules);
-  (* Start the toplevel loop *)
-  Coqtop.start()
+let () = Coqtop.start()
-- 
cgit v1.2.3