All invocations to ocaml compilers go through ocamlfind

Nothing is done for camlp4
There is an issue with computing camlbindir

2 files changed, 18 insertions, 18 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 36d29a1e83..954c21d587 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -355,7 +355,7 @@ let clean sds sps =
     sds;
   print "\n";
   print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
-  print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
+  print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
   print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
 
 let header_includes () = ()
@@ -365,19 +365,19 @@ let implicit () =
   let mli_rules () =
     print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
-    print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml4_rules () =
     print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
     print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
-    print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let ml_rules () =
     print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
     print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
     print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
-    print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
     print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
 \t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
@@ -455,17 +455,18 @@ let variables is_install opt (args,defs) =
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n";
-    print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n";
-    print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n";
-    print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n";
+    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
+    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
+    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
+    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+    print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
     print "GRAMMARS?=grammar.cma\n";
     print "ifeq ($(CAMLP4),camlp5)
 CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
 else
 CAMLP4EXTEND=threads.cma
 endif\n";
-    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
+    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)/threads/ $(COQSRCLIBS) compat5.cmo \\
   $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
@@ -682,9 +683,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index be796e6956..a6254b2a44 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -149,7 +149,7 @@ let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files\
 \nFlags are:\
 \n  -coqlib dir    Specify where the Coq object files are\
-\n  -camlbin dir   Specify where the OCaml binaries are\
+\n  -ocamlfind dir Specify where the ocamlfind binary is\
 \n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
 \n  -o exec-file   Specify the name of the resulting toplevel\
 \n  -boot          Run in boot mode\
@@ -167,8 +167,8 @@ let parse_args () =
     (* Directories *)
     | "-coqlib" :: d :: rem ->
 	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
-    | "-camlbin" :: d :: rem ->
-	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-ocamlfind" :: d :: rem ->
+	Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem
     | "-camlp4bin" :: d :: rem ->
 	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
     | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
@@ -266,10 +266,9 @@ let main () =
   let (options, userfiles) = parse_args () in
   (* Directories: *)
   let () = Envars.set_coqlib ~fail:Errors.error in
-  let camlbin = Envars.camlbin () in
   let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
   (* Which ocaml compiler to invoke *)
-  let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+  let prog = if !opt then "opt" else "ocamlc" in
   (* Which arguments ? *)
   if !opt && !top then failwith "no custom toplevel in native code !";
   let flags = if !opt then [] else Coq_config.vmbyteflags in
@@ -284,14 +283,14 @@ let main () =
       (std_includes basedir) @ tolink @ [ main_file ] @ topstart
     in
     if !echo then begin
-      let command = String.concat " " (prog::args) in
+      let command = String.concat " " (Envars.ocamlfind ()::prog::args) in
       print_endline command;
       print_endline
 	("(command length is " ^
 	    (string_of_int (String.length command)) ^ " characters)");
       flush Pervasives.stdout
     end;
-    let exitcode = run_command prog args in
+    let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in
     clean main_file;
     exitcode
   with reraise -> clean main_file; raise reraise