Nettoyage des variables Coq et amélioration de coqmktop. Les

principaux changements sont:
  - coqtop (et coqc) maintenant insensible aux variables
    d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
    librairies Coq peut être spécifié par l'option -coqlib
  - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
    -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
    chemins des exécutables OCaml; en dehors du mode boot, coqmktop
    cherche les exécutables OCaml dans PATH
  - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
    étant installé en copiant l'architecture des sources (ie lib.cmxa
    est installé dans COQLIB/lib/lib.cmxa)
  - coq_makefile prend maintenant 3 paramètres sous forme de variables
    d'environnement: COQBIN pour dire où trouver les exécutables Coq,
    CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
    chemins vers les librairies sont déduits en utilisant -where

Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...). 




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

3 files changed, 37 insertions, 37 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 52923ad4e..77fdffb0d 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -89,8 +89,6 @@ 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";
@@ -121,7 +119,7 @@ let standard sds sps =
   print "clean:\n";
   print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(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) Makefile.config\n";
+         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
   if !some_mlfile then
     print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
   print "\t- rm -rf html\n";
@@ -139,10 +137,11 @@ let standard sds sps =
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
     sds;
-  print "\n\n"
+  print "\n\n";
+  print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n";
+  print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n"
 
-let header_includes () =
-  print "include Makefile.config\n.PHONY: Makefile.config\n"
+let header_includes () = ()
   
 let footer_includes () = 
   if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
@@ -187,10 +186,12 @@ let variables l =
     if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
     (* Coq executables and relative variables *)
     print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+    print "ifdef CAMLBIN\n  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n";
     print "COQC:=$(COQBIN)coqc\n";
     print "COQDEP:=$(COQBIN)coqdep -c\n";
     print "GALLINA:=$(COQBIN)gallina\n";
     print "COQDOC:=$(COQBIN)coqdoc\n";
+    print "COQMKTOP:=$(COQBIN)coqmktop\n";
     (* Caml executables and relative variables *)
     printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
     printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
@@ -228,11 +229,13 @@ let dir_of_target t =
 
 let parameters () =
   print "# \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"
+  print "# This Makefile may take 3 arguments passed as environment variables:\n";
+  print "#   - COQBIN to specify the directory where Coq binaries resides;\n";
+  print "#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n";
+  print "COQLIB:=$(shell $(COQBIN)coqtop -where)\n"; 
+  print "CAMLP4:=$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\n"; 
+  print "ifndef CAMLP4BIN\n  CAMLP4BIN:=$(CAMLBIN)\nendif\n\n";
+  print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n"
 
 let include_dirs l =
   let rec split_includes l = 
@@ -263,22 +266,18 @@ let include_dirs l =
   let str_r = parse_includes inc_r in
     section "Libraries definitions.";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\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 \\
-  -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
-  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc -I $(COQTOP)/contrib/dp \\
-  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
-  -I $(COQTOP)/contrib/firstorder -I $(COQTOP)/contrib/fourier \\
-  -I $(COQTOP)/contrib/funind -I $(COQTOP)/contrib/interface \\
-  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
-  -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\n";
-    print "  COQSRCLIBS:=-I $(COQLIB)\n";
-    print "endif\n";
+    print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
+  -I $(COQLIB)/library -I $(COQLIB)/parsing \\
+  -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
+  -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\
+  -I $(COQLIB)/toplevel -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\
+  -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\
+  -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\
+  -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\
+  -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\
+  -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\
+  -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\
+  -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\n";
     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"
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 3d93c8a90..393554568 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -15,8 +15,6 @@ open Unix
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
-let coqlib = ref Coq_config.coqlib
-
 let option_c = ref false
 let option_D = ref false
 let option_w = ref false
@@ -24,7 +22,6 @@ let option_i = ref false
 let option_sort = ref false
 let option_noglob = ref false
 let option_slash = ref false
-let option_boot = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
@@ -516,14 +513,14 @@ let rec parse = function
   | "-D" :: ll -> option_D := true; parse ll
   | "-w" :: ll -> option_w := true; parse ll
   | "-i" :: ll -> option_i := true; parse ll
-  | "-boot" :: ll -> option_boot := true; parse ll
+  | "-boot" :: ll -> Flags.boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll
   | "-I" :: r :: ll -> add_dir add_known r []; parse ll
   | "-I" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
   | "-R" :: ([] | [_]) -> usage ()
-  | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
+  | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
   | "-suffix" :: [] -> usage ()
@@ -534,13 +531,14 @@ let rec parse = function
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_boot then begin
+  if !Flags.boot then begin
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "contrib" ["Coq"]
-  end else begin 
-    add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"]; 
-    add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"];
-    add_dir add_coqlib_known (!coqlib//"user-contrib") []
+  end else begin
+    let coqlib = Envars.coqlib () in
+      add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; 
+      add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
+      add_dir add_coqlib_known (coqlib//"user-contrib") []
   end;
   List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu;
   List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu;
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index e6c3e5c07..864b2718e 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -57,6 +57,7 @@ let usage () =
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  --latin1             set ISO-8859-1 input language";
@@ -318,6 +319,8 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--boot" | "-boot") :: rem ->
+	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->