Many changes in the Makefile infrastructure + a beginning of ocamlbuild

 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

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

1 files changed, 13 insertions, 17 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 2c9c6d213..50059ae17 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -28,7 +28,7 @@ let split_list l = Str.split spaces l
 let copts     = split_list Tolink.copts
 let core_objs = split_list Tolink.core_objs
 let core_libs = split_list Tolink.core_libs
-let ide       = split_list Tolink.ide 
+let ide       = split_list Tolink.ide
 
 (* 3. Toplevel objects *)
 let camlp4topobjs =
@@ -89,25 +89,21 @@ let files_to_link userfiles =
     if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
-  let ide_objs = if !coqide then 
-    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
-  else [] 
+  let ide_objs =
+    if !coqide then "Threads"::"Lablgtk"::"GtkThread"::ide else []
   in
-  let ide_libs = if !coqide then 
-    ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
-     "ide/ide.cma" ]
-  else [] 
+  let ide_libs =
+    if !coqide then
+      ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ]
+    else []
   in
-  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs
-  and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
-  let objstolink,libstolink =
-    if !opt then 
-      ((List.map native_suffix objs) @ userfiles,
-       (List.map native_suffix libs) @ userfiles)
-    else 
-      (objs @ userfiles, libs @ userfiles )
+  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in
+  let modules = List.map module_of_file (objs @ userfiles)
+  in
+  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
+  let libstolink =
+    (if !opt then List.map native_suffix libs else libs) @ userfiles
   in
-  let modules = List.map module_of_file objstolink in
   (modules, libstolink)
 
 (* Gives the list of all the directories under [dir].