Better mechanism for loading initial plugins

 Instead of dirty hacks in toplevel/coqtop.ml, we simply add
 some Declare ML Module in Prelude.v. Gain: now that coqdep
 is clever enough, dependencies are automatic, and we can
 simplify the Makefile quite a lot: no more references to
 INITPLUGINSBEST and the like.

 Besides, mltop.ml4 can also be simplified a lot: by
 giving $(CONTRIBSTATIC) to coqmktop instead of contrib.cma,
 now coqtop is aware that it already contain the static plugins
 (or not), and subsequent ML Module are ignored correctly
 without us having to do anything :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11979 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 15 insertions, 46 deletions

diff --git a/Makefile.build b/Makefile.build
index ecc70a1e53..ea2fad1284 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -101,7 +101,7 @@ ifndef ORDER_ONLY_SEP
 $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
 endif
 
-VO_TOOLS_DEP := $(BESTCOQTOP) $(INITPLUGINSBEST)
+VO_TOOLS_DEP := $(BESTCOQTOP)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif
@@ -153,19 +153,17 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-coqbinaries:: ${COQBINARIES} ${CSDPCERT} $(INITPLUGINSOPT) $(INITPLUGINS)
+coqbinaries:: ${COQBINARIES} ${CSDPCERT}
 
 coq: coqlib tools coqbinaries
 
-coqlib:: initplugins theories contrib
+coqlib:: theories contrib
 
 coqlight: theories-light tools coqbinaries
 
 states:: states/initial.coq
 
-initplugins: $(INITPLUGINSOPT) $(INITPLUGINS)
-
-plugins: $(INITPLUGINSOPT) $(INITPLUGINS) $(PLUGINSOPT) $(PLUGINS)
+plugins: $(PLUGINSOPT) $(PLUGINS)
 
 $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
@@ -669,9 +667,7 @@ install-tools::
 
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
-	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINS)
-	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT)
 	$(MKDIR) $(FULLCOQLIB)/states
 	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
@@ -690,9 +686,7 @@ endif
 
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT)
-	$(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINS)
-	$(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT)
 	$(MKDIR) $(FULLCOQLIB)/states
 	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	-$(INSTALLLIB) revision $(FULLCOQLIB)
diff --git a/Makefile.common b/Makefile.common
index 71e85d7f06..5a981ae122 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -267,11 +267,6 @@ ifneq ($(HASNATDYNLINK),false)
  PLUGINS:=$(CONTRIBS)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
- ifeq ($(BEST),opt)
-  INITPLUGINSBEST:=$(INITPLUGINSOPT)
- else
-  INITPLUGINSBEST:=$(INITPLUGINS)
- endif
 else
  CONTRIBSTATIC:=$(CONTRIBS)
 endif
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f0c67df3a2..84de55e24d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,3 +15,11 @@ Require Export Specif.
 Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
+(* Initially available plugins *)
+Declare ML Module "extraction_plugin".
+Declare ML Module "cc_plugin".
+Declare ML Module "ground_plugin".
+Declare ML Module "dp_plugin".
+Declare ML Module "recdef_plugin".
+Declare ML Module "subtac_plugin".
+Declare ML Module "xml_plugin".
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b75ef535f4..cd13c6c880 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -346,7 +346,6 @@ let init is_ide =
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
         Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
-      Mltop.load_initial_plugins ();
       load_vernac_obj ();
       require ();
       load_rcfile();
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 9bac42c93c..fc808f0b7c 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -226,36 +226,13 @@ let file_of_name name =
 
 let stdlib_use_plugins = Coq_config.has_natdynlink
 
-(** List of plugins we want to dynamically load at launch-time.
-    Order matters, for instance ground_plugin needs cc_plugins. *)
-
-let initial_plugins =
-  [ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin"; 
-    "Recdef_plugin"; "Subtac_plugin"; "Xml_plugin"; ]
-
-(** Other plugins of the standard library. We need their list
-    to avoid trying to load them if they have been statically compiled
-    into coqtop. Otherwise, they will be loaded automatically when
-    doing the corresponding Require. *)
-
-let other_stdlib_plugins =
-  [ "Omega_plugin"; "Romega_plugin"; "Micromega_plugin"; "Quote_plugin";
-    "Ring_plugin"; "Newring_plugin"; "Field_plugin"; "Fourier_plugin";
-    "Rtauto_plugin" ]
-
-let initially_known_modules =
-  if stdlib_use_plugins then Stringset.empty
-  else
-    let all_plugins = initial_plugins @ other_stdlib_plugins in
-    List.fold_right Stringset.add all_plugins Stringset.empty
-
 (* [known_loaded_module] contains the names of the loaded ML modules
  * (linked or loaded with load_object). It is used not to load a 
  * module twice. It is NOT the list of ML modules Coq knows. *)
 
 type ml_module_object = { mnames : string list }
 
-let known_loaded_modules = ref initially_known_modules
+let known_loaded_modules = ref Stringset.empty
 
 let add_known_module mname =
   known_loaded_modules := Stringset.add mname !known_loaded_modules
@@ -335,9 +312,6 @@ let (inMLModule,outMLModule) =
 let declare_ml_modules l =
   Lib.add_anonymous_leaf (inMLModule {mnames=l})
 
-let load_initial_plugins () =
-  if stdlib_use_plugins then declare_ml_modules initial_plugins
-
 let print_ml_path () =
   let l = !coq_mlpath_copy in
   ppnl (str"ML Load Path:" ++ fnl () ++ str"  " ++
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index af638241c0..715355635e 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -64,7 +64,6 @@ val inMLModule : ml_module_object -> Libobject.obj
 val outMLModule : Libobject.obj -> ml_module_object
 
 val declare_ml_modules : string list -> unit
-val load_initial_plugins : unit -> unit
 
 val print_ml_path : unit -> unit