From c215c4429a85a6d73cc1a33041258cacbe4de199 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Dec 2008 13:56:19 +0000
Subject: 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
---
 tools/coqdep.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 529ca0ba54..3d93c8a908 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -246,11 +246,22 @@ let traite_fichier_Coq verbose f =
                	       try
               		 let mldir = Hashtbl.find mlKnown s in
 			 let filename = file_name ([String.uncapitalize s],mldir) in
-              		 if Coq_config.has_natdynlink then
+			 if Coq_config.has_natdynlink then
 			   printf " %s.cmo %s.cmxs" filename filename
 			 else
 			   printf " %s.cmo" filename
-              	       with Not_found -> ()
+		       with Not_found ->
+			 (** The .cmxs we want to load dynamically may come
+			     from a .cmxa, that has no corresponding .ml file.
+			     Idem with bytecode .cma. What dependency should
+			     we produce then ? For the moment, we suppose the
+			     .cmxs and .cma are at the same location. *)
+			 let mldir = Some (Filename.dirname f) in
+			 let filename = file_name ([String.uncapitalize s],mldir) in
+			 if Coq_config.has_natdynlink then
+			   printf " %s.cma %s.cmxs" filename filename
+			 else
+			   printf " %s.cma" filename
 		     end)
 		sl
 	  | Load str -> 
-- 
cgit v1.2.3