From 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 28 Oct 2017 21:02:48 +0200
Subject: [build] Remove coqmktop in favor of ocamlfind.

We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.

This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.

An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.

We also perform some smaller cleanups taking profit from ocamlfind.
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 620fec5464..0078dba20d 100644
--- a/Makefile
+++ b/Makefile
@@ -246,7 +246,7 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN)
+	rm -f $(COQTOPEXE) $(CHICKEN)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
-- 
cgit v1.2.3


From f5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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.
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 0078dba20d..2637996edd 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)
 
-- 
cgit v1.2.3