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

18 files changed, 36 insertions, 13 deletions

diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v
index ee1ddd477b..efa53b4e9d 100644
--- a/contrib/field/LegacyField.v
+++ b/contrib/field/LegacyField.v
@@ -11,5 +11,6 @@
 Require Export LegacyField_Compl.
 Require Export LegacyField_Theory.
 Require Export LegacyField_Tactic.
+Declare ML Module "field_plugin".
 
 (* Command declarations are moved to the ML side *)
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index ac1592beea..07b2973a4a 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -10,15 +10,11 @@
 
 (* "Fourier's method to solve linear inequations/equations systems.".*)
 
-Declare ML Module "quote".
-Declare ML Module "ring".
-Declare ML Module "fourier".
-Declare ML Module "fourierR".
-Declare ML Module "field".
-
-Require Export Fourier_util.
+Require Export LegacyRing.
 Require Export LegacyField.
 Require Export DiscrR.
+Require Export Fourier_util.
+Declare ML Module "fourier_plugin".
 
 Ltac fourier := abstract (fourierz; field; discrR).
 
diff --git a/contrib/micromega/Psatz.v b/contrib/micromega/Psatz.v
index b2dd99100c..a3be562077 100644
--- a/contrib/micromega/Psatz.v
+++ b/contrib/micromega/Psatz.v
@@ -22,6 +22,7 @@ Require Import Raxioms.
 Require Export RingMicromega.
 Require Import VarMap.
 Require Tauto.
+Declare ML Module "micromega_plugin".
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
index c054f218aa..f02209459f 100644
--- a/contrib/micromega/QMicromega.v
+++ b/contrib/micromega/QMicromega.v
@@ -17,6 +17,7 @@ Require Import RingMicromega.
 Require Import Refl.
 Require Import QArith.
 Require Import Qfield.
+Declare ML Module "micromega_plugin".
 
 Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq  Qle Qlt.
 Proof.
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v
index 7c6969c2f2..70786a0571 100644
--- a/contrib/micromega/RMicromega.v
+++ b/contrib/micromega/RMicromega.v
@@ -17,6 +17,7 @@ Require Import RingMicromega.
 Require Import Refl.
 Require Import Raxioms RIneq Rpow_def DiscrR.
 Require Setoid.
+Declare ML Module "micromega_plugin".
 
 Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R).
 Proof.
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v
index 0855925a3d..1da3228a98 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/contrib/micromega/ZMicromega.v
@@ -19,6 +19,7 @@ Require Import Refl.
 Require Import ZArith.
 Require Import List.
 Require Import Bool.
+Declare ML Module "micromega_plugin".
 
 Ltac flatten_bool :=
   repeat match goal with
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 3b427162e8..30b9457183 100644
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -19,6 +19,7 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+Declare ML Module "omega_plugin".
 
 Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
diff --git a/contrib/omega/OmegaPlugin.v b/contrib/omega/OmegaPlugin.v
new file mode 100644
index 0000000000..21535f0d3b
--- /dev/null
+++ b/contrib/omega/OmegaPlugin.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Declare ML Module "omega_plugin".
diff --git a/contrib/ring/Quote.v b/contrib/quote/Quote.v
index 9a11a70b9c..f21a678e1a 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/quote/Quote.v
@@ -8,6 +8,8 @@
 
 (* $Id$ *)
 
+Declare ML Module "quote_plugin".
+
 (***********************************************************************
   The "abstract" type index is defined to represent variables.
 
diff --git a/contrib/ring/g_quote.ml4 b/contrib/quote/g_quote.ml4
index 808cbbf274..808cbbf274 100644
--- a/contrib/ring/g_quote.ml4
+++ b/contrib/quote/g_quote.ml4
diff --git a/contrib/ring/quote.ml b/contrib/quote/quote.ml
index 3b13283e13..9141dc2f52 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/quote/quote.ml
@@ -119,7 +119,7 @@ open Tacexpr
   We do that lazily, because this code can be linked before
   the constants are loaded in the environment *)
 
-let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s
+let constant dir s = Coqlib.gen_constant "Quote" ("quote"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
@@ -388,7 +388,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"Quote"];
+  Coqlib.check_required_library ["Coq";"quote";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index ed1da9c56e..4ae85baf37 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -13,6 +13,7 @@ Require Export LegacyRing_theory.
 Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
+Declare ML Module "ring_plugin".
 
 (* As an example, we provide an instantation for bool. *)
 (* Other instatiations are given in ArithRing and ZArithRing in the
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index b5cd6b1d0c..93b9bc7cf5 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -10,4 +10,5 @@
 
 Require Export Setoid_ring_theory.
 Require Export Quote.
-Require Export Setoid_ring_normalize.
\ No newline at end of file
+Require Export Setoid_ring_normalize.
+Declare ML Module "ring_plugin".
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 92f74d1d94..bb6aaea7de 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -752,7 +752,7 @@ let constants_to_unfold =
       "Coq.ring.Ring_normalize.interp_vl";
       "Coq.ring.Ring_abstract.interp_acs";
       "Coq.ring.Ring_abstract.interp_sacs";
-      "Coq.ring.Quote.varmap_find";
+      "Coq.quote.Quote.varmap_find";
       (* anciennement des Local devenus Definition *)
       "Coq.ring.Ring_normalize.ics_aux";
       "Coq.ring.Ring_normalize.ivl_aux";
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 4281cc5736..3ddb6bed12 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -10,3 +10,5 @@ Require Import ReflOmegaCore.
 Require Export Setoid.
 Require Export PreOmega.
 Require Export ZArith_base.
+Require Import OmegaPlugin.
+Declare ML Module "romega_plugin".
\ No newline at end of file
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
index 342c03dbac..4b95097e2f 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/contrib/rtauto/Rtauto.v
@@ -14,6 +14,8 @@ Require Export Bintree.
 Require Import Bool.
 Unset Boxed Definitions.
 
+Declare ML Module "rtauto_plugin".
+
 Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index 95b037e3b6..fd9dd8d0d3 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -10,7 +10,8 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Declare ML Module "newring".
+Require Import Quote.
+Declare ML Module "newring_plugin".
 Require Export Ring_theory.
 Require Export Ring_tac.
 Require Import InitialRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 46d106d37a..2ff3322380 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -4,7 +4,8 @@ Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
 Require Import InitialRing.
-Declare ML Module "newring".
+Require Import Quote.
+Declare ML Module "newring_plugin".
   
 
 (* adds a definition id' on the normal form of t and an hypothesis id