Take advantage of natdynlink when available: almost all contribs become loadable plugins

- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
  when launching coqtop (see Coqtop.load_initial_plugins):
     extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
     quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
  one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
  is explicitely given to configure, coqtop is statically linked with all of
  the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
  and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
  same location as the .v during the build, but can be moved later in any place of
  the ml loadpath.

This is clearly an experimentation. Feedback most welcome...

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

2 files changed, 27 insertions, 10 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b2589d42f0..fa8fca66f5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -78,7 +78,21 @@ let set_include d p =
   let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p)
 let set_rec_include d p =
   let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
- 
+
+let load_initial_plugins () =
+  (** Order matters ! For instance ground_plugin needs cc_plugin *)
+  let initial_plugins =
+    [ "extraction_plugin";
+      "jprover_plugin";
+      "cc_plugin";
+      "ground_plugin";
+      "dp_plugin";
+      "recdef_plugin";
+      (*"subtac_plugin";*)
+      "xml_plugin";
+    ] in
+  if Mltop.has_dynlink then Mltop.declare_ml_modules initial_plugins
+
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
   load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
@@ -340,6 +354,7 @@ 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 ();
+      load_initial_plugins ();
       load_vernac_obj ();
       require ();
       load_rcfile();
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 57c1464286..611567af98 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -289,18 +289,20 @@ let cache_ml_module_object (_,{mnames=mnames}) =
     (fun name ->
        let mname = mod_of_name name in
        if not (module_is_known mname) then
-         let fname = file_of_name mname in
-         begin 
-	   try 
-	     if_verbose 
+	 if has_dynlink then
+           let fname = file_of_name mname in
+	   try
+	     if_verbose
 	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
              load_object mname fname;
-             if_verbose msgnl (str"done]")
-           with e -> 
-	     if_verbose msgnl (str"failed]"); 
+             if_verbose msgnl (str"done]");
+             add_loaded_module mname
+           with e ->
+	     if_verbose msgnl (str"failed]");
 	     raise e
-	 end;
-         add_loaded_module mname)
+	 else
+	   if_verbose
+	     msgnl (str"[Ignoring ML file " ++ str mname ++ str "]"))
     mnames
 
 let export_ml_module_object x = Some x