Tentative d'amélioration de la robustesse des Makefile générés par

coq_makefile en présence de fichiers .ml :

  - ajout d'une option -config à coqtop qui affiche les informations
    de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, 
    LOCAL)

  - coq_makefile inclut un fichier Makefile.config qui contient les
    valeurs des variables sus-mentionnées




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

5 files changed, 39 insertions, 27 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index e661455ca..aa09219bf 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -164,6 +164,9 @@ let parse_args () =
 	  try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib 
 	in
 	  print_endline coqlib; exit 0
+
+    | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
+
     | ("-v"|"--version") :: _ ->
         Usage.version ()
     | f :: rem -> 
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index b88cae064..e2ea8250d 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -89,6 +89,8 @@ let is_genrule r =
       Str.string_match genrule r 0
 
 let standard sds sps =
+  print "Makefile.config:\n";
+  print "\t$(COQBIN)/coqtop -config > $@\n\n";
   print "byte:\n";
   print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
   print "opt:\n";
@@ -113,9 +115,9 @@ let standard sds sps =
     print "\n";
   end;
   print "clean:\n";
-  print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n";
+  print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
-         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
+         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) Makefile.config\n";
   if !some_mlfile then
     print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
   print "\t- rm -rf html\n";
@@ -135,7 +137,10 @@ let standard sds sps =
     sds;
   print "\n\n"
 
-let includes () =
+let header_includes () =
+  print "include Makefile.config\n.PHONY: Makefile.config\n"
+  
+let footer_includes () = 
   if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
   if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"
 
@@ -218,11 +223,10 @@ let dir_of_target t =
 
 let parameters () =
   print "# \n";
-  print "# Compilation looks in the path for coqtop; set COQBIN if coqtop is not in path\n";
-  print "# if .ml files have to be compiled, set CAMLBIN if ocamlc is not in path\n";
-  print "# if .ml files have to be compiled, set CAMLP4BIN if camlp4/5 is not in path\n";
-  print "# \n";
-  print "# set COQTOP to a Coq source directory for compiling over Coq compiled sources\n";
+  print "# This Makefile looks for coqtop in PATH and in COQBIN to create Makefile.config\n";
+  print "# Once created, Make refers to this file to determine the important paths for Coq\n";
+  print "# and Caml binaries. To change which Coq is used to compile your contribution,\n";
+  print "# delete Makefile.config, and set COQBIN to the desired value.\n";
   print "# \n\n"
 
 let include_dirs l =
@@ -253,16 +257,8 @@ let include_dirs l =
   let str_i' = parse_includes inc_i' in
   let str_r = parse_includes inc_r in
     section "Libraries definitions.";
-    printf "CAMLP4:=%s\n" Coq_config.camlp4;
-    print "ifdef CAMLP4BIN\n";
-    print "  CAMLP4LIB:=$(shell $(CAMLP4BIN)/$(CAMLP4) -where 2> /dev/null)\n";
-    print "else\n";
-    print "  CAMLP4LIB:=$(shell $(CAMLP4) -where 2> /dev/null)\n";
-    print "endif\n";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
-    print "COQLIB:=$(shell $(COQBIN)coqtop -where 2> /dev/null)\n";
-    print "ifdef COQTOP # set COQTOP for compiling from Coq sources\n";
-    print "  COQBIN:=$(COQTOP)/bin/\n";
+    print "ifneq ($(LOCAL),0) # set COQTOP for compiling from Coq sources\n";
     print "  COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
   -I $(COQTOP)/library -I $(COQTOP)/parsing \\
   -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
@@ -275,17 +271,9 @@ let include_dirs l =
   -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
   -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
   -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml\n";
-    print "else ifneq ($(strip $(COQLIB)),)\n";
-    print "  COQSRCLIBS:=-I $(COQLIB)\n";
     print "else\n";
-    print "  $(error Cannot find coqtop in path; set variable COQBIN to the directory where coqtop is located)\n";
+    print "  COQSRCLIBS:=-I $(COQLIB)\n";
     print "endif\n";
-    if List.exists (function ML _ -> true | _ -> false) l then
-      begin
-	print "ifeq ($(strip $(CAMLP4LIB)),)\n";
-	print "  $(error Cannot find $(CAMLP4) in path; set variable CAMLP4BIN to the directory where $(CAMLP4) is located)\n";
-	print "endif\n";
-      end;
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
@@ -504,6 +492,7 @@ let directories_deps l =
 let do_makefile args =
   let l = process_cmd_line args in
     banner ();
+    header_includes ();
     warning ();
     command_line args;
     parameters ();
@@ -516,7 +505,7 @@ let do_makefile args =
 	implicit ();
 	standard sds sps;
 	(* TEST directories_deps l; *)
-	includes ();
+	footer_includes ();
 	warning ();
 	if not (!output_channel == stdout) then close_out !output_channel;
 	exit 0
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 277bc8d09..2ad5117b9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -276,6 +276,8 @@ let parse_args is_ide =
 
     | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
+    | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0
+
     | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 417a496f8..02fa69142 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -49,6 +49,7 @@ let print_usage_channel co command =
   -byte                  run the bytecode version of Coq
 
   -where                 print Coq's standard library location and exit
+  -config                print Coq's configuration information and exit
   -v                     print Coq version and exit
 
   -q                     skip loading of rcfile
@@ -84,3 +85,17 @@ options are:
   -bindir   override the default directory where coqc looks for coqtop
   -image f  specify an alternative executable for Coq
   -t        keep temporary files\n\n"
+
+(* Print the configuration information *)
+
+let print_config () = 
+  if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
+  Printf.printf "COQBIN=%s/\n" Coq_config.bindir;
+  Printf.printf "COQLIB=%s/\n" Coq_config.coqlib;
+  Printf.printf "COQTOP=%s/\n" Coq_config.coqtop;
+  Printf.printf "CAMLBIN=%s/\n" Coq_config.camldir;
+  Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
+  Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib
+
+
+
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 6c9ed474c..fb973e3ba 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -18,3 +18,6 @@ val print_usage : string -> unit
 (*s Prints the usage on the error output. *)
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit
+
+(*s Prints the configuration information *)
+val print_config : unit -> unit