From c954bb5600e39f2cc19a96bcbb912ac694b3c16a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Fri, 24 Jun 2016 01:06:46 +0200
Subject: Makefile.install: fix the install of plugin cmi

 Now that the plugins are packed, a plugin forms now a unique
 compilation unit, and we only need to install the main cmi file of
 this plugin (foo_plugin.cmi).

 Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and
 some other cleanup in Makefile.common (no more INITPLUGINS variable,
 for instance).
---
 Makefile.common | 81 +++++++++++++++++++++++----------------------------------
 1 file changed, 33 insertions(+), 48 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 310e30a0c..49fe1fd93 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -57,7 +57,7 @@ CORESRCDIRS:=\
   proofs 	tactics 	pretyping	interp		stm \
   toplevel	parsing 	printing	intf	engine	ltac
 
-PLUGINS:=\
+PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
@@ -67,7 +67,7 @@ PLUGINS:=\
 SRCDIRS:=\
   $(CORESRCDIRS)  \
   tools 	tools/coqdoc	\
-  $(addprefix plugins/, $(PLUGINS))
+  $(addprefix plugins/, $(PLUGINDIRS))
 
 COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
@@ -98,60 +98,45 @@ OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
 # plugins object files
 ###########################################################################
 
-OMEGACMA:=plugins/omega/omega_plugin.cmo
-ROMEGACMA:=plugins/romega/romega_plugin.cmo
-MICROMEGACMA:=plugins/micromega/micromega_plugin.cmo
-QUOTECMA:=plugins/quote/quote_plugin.cmo
-RINGCMA:=plugins/setoid_ring/newring_plugin.cmo
-NSATZCMA:=plugins/nsatz/nsatz_plugin.cmo
-FOURIERCMA:=plugins/fourier/fourier_plugin.cmo
-EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cmo
-FUNINDCMA:=plugins/funind/recdef_plugin.cmo
-FOCMA:=plugins/firstorder/ground_plugin.cmo
-CCCMA:=plugins/cc/cc_plugin.cmo
-BTAUTOCMA:=plugins/btauto/btauto_plugin.cmo
-RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cmo
-NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cmo
-OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
+OMEGACMO:=plugins/omega/omega_plugin.cmo
+ROMEGACMO:=plugins/romega/romega_plugin.cmo
+MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
+QUOTECMO:=plugins/quote/quote_plugin.cmo
+RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
+NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
+FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
+EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
+FUNINDCMO:=plugins/funind/recdef_plugin.cmo
+FOCMO:=plugins/firstorder/ground_plugin.cmo
+CCCMO:=plugins/cc/cc_plugin.cmo
+BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
+RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
+NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
+OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         z_syntax_plugin.cmo \
         numbers_syntax_plugin.cmo \
         r_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
         string_syntax_plugin.cmo )
-DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo
-DERIVECMA:=plugins/derive/derive_plugin.cmo
-SSRMATCHINGCMA:=plugins/ssrmatching/ssrmatching_plugin.cmo
-
-PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
-        $(QUOTECMA) $(RINGCMA) \
-        $(FOURIERCMA) $(EXTRACTIONCMA) \
-        $(CCCMA)  $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
-        $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \
-	$(DERIVECMA) $(SSRMATCHINGCMA)
-
-ifneq ($(HASNATDYNLINK),false)
- STATICPLUGINS:=
- INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
-	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs)
- PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs)
+DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
+DERIVECMO:=plugins/derive/derive_plugin.cmo
+SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
+
+PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
+        $(QUOTECMO) $(RINGCMO) \
+        $(FOURIERCMO) $(EXTRACTIONCMO) \
+        $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
+        $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
+	$(DERIVECMO) $(SSRMATCHINGCMO)
+
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ STATICPLUGINS:=$(PLUGINSCMO)
+ PLUGINS:=
 else
-ifeq ($(BEST),byte)
  STATICPLUGINS:=
- INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
-	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs)
- PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs)
-else
- STATICPLUGINS:=$(PLUGINSCMA)
- INITPLUGINS:=
- INITPLUGINSOPT:=
- PLUGINS:=
- PLUGINSOPT:=
-endif
+ PLUGINS:=$(PLUGINSCMO)
 endif
+PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
 
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
-- 
cgit v1.2.3