From 382ee49700c4b4ee78ba95b2e86866ebd3b35d74 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Mar 2018 01:33:17 +0100
Subject: [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.
---
 Makefile.install | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'Makefile.install')

diff --git a/Makefile.install b/Makefile.install
index 02695287b9..0764b61fc7 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)
-- 
cgit v1.2.3