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).

3 files changed, 56 insertions, 61 deletions

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)
diff --git a/Makefile.dev b/Makefile.dev
index f35b861c1..26092e8dc 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -187,16 +187,16 @@ EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
 CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
 
-omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
-micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
-setoid_ring: $(RINGVO) $(RINGCMA)
-nsatz: $(NSATZVO) $(NSATZCMA)
-extraction: $(EXTRACTIONCMA)
-fourier: $(FOURIERVO) $(FOURIERCMA)
-funind: $(FUNINDCMA) $(FUNINDVO)
-cc: $(CCVO) $(CCCMA)
-rtauto: $(RTAUTOVO) $(RTAUTOCMA)
-btauto: $(BTAUTOVO) $(BTAUTOCMA)
+omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
+micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
+setoid_ring: $(RINGVO) $(RINGCMO)
+nsatz: $(NSATZVO) $(NSATZCMO)
+extraction: $(EXTRACTIONCMO)
+fourier: $(FOURIERVO) $(FOURIERCMO)
+funind: $(FUNINDCMO) $(FUNINDVO)
+cc: $(CCVO) $(CCCMO)
+rtauto: $(RTAUTOVO) $(RTAUTOCMO)
+btauto: $(BTAUTOVO) $(BTAUTOCMO)
 
 .PHONY: omega micromega setoid_ring nsatz extraction
 .PHONY: fourier funind cc rtauto btauto
diff --git a/Makefile.install b/Makefile.install
index ed29bc1e7..09c3331f0 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -9,6 +9,11 @@
 # This makefile regroups installation rules
 # It is included by Makefile.build
 
+# NOTA: currently, the install rules below assume that everything needed
+# has already been correctly built. In particular, this is *not* enforced
+# by dependencies between rules, so do *not* try overly clever things like
+# 'make world install' in one unique command
+
 ifeq ($(LOCAL),true)
 install:
 	@echo "Nothing to install in a local build!"
@@ -16,6 +21,8 @@ else
 install: install-coq install-coqide install-doc-$(WITHDOC)
 endif
 
+# NOTA: for install-coqide, see Makefile.ide
+
 install-doc-all: install-doc
 install-doc-no:
 
@@ -72,12 +79,15 @@ install-tools:
 	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
 
-# The list of .cmi to install, including the ones obtained
-# from .mli without .ml, and the ones obtained from .ml without .mli
+# The list of .cmi to install, including in particular
+# - the ones obtained from .mli without .ml
+# - the ones of modules in core cma's
+# - the ones corresponding to packed plugins
 
 INSTALLCMI = $(sort \
 	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
-	$(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))
+	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
+	$(PLUGINS:.cmo:.cmi)
 
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)