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

1 files changed, 48 insertions, 35 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 1b9247616d..0bd9d0402b 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -17,7 +17,7 @@ open Unix
 (* Objects to link *)
 
 (* 1. Core objects *)
-let ocamlobjs = ["unix.cma";"nums.cma"]
+let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
 let dynobjs = ["dynlink.cma"]
 let camlp4objs = ["gramlib.cma"]
 let libobjs = ocamlobjs @ camlp4objs
@@ -44,7 +44,6 @@ let notopobjs = gramobjs
 (* 4. High-level tactics objects *)
 
 (* environment *)
-let src_coqtop = ref Coq_config.coqtop
 let opt        = ref false
 let full       = ref false
 let top        = ref false
@@ -57,11 +56,13 @@ let src_dirs () =
   if !coqide then [[ "ide" ]] else []
 
 let includes () = 
-  List.fold_right
-    (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l)
-    (src_dirs ())
-    (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ 
-     (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
+  let coqlib = Envars.coqlib () in
+    List.fold_right
+      (fun d l -> "-I" :: List.fold_left Filename.concat coqlib d :: l)
+      (src_dirs ())
+      (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ 
+	 ["-I"; "\"" ^ coqlib ^ "\""] @
+	 (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -88,11 +89,11 @@ let files_to_link userfiles =
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
   let ide_objs = if !coqide then 
-    "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
+    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
   else [] 
   in
   let ide_libs = if !coqide then 
-    ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
+    ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
      "ide/ide.cma" ]
   else [] 
   in
@@ -136,22 +137,33 @@ let all_subdirs dir =
 let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files
 Flags.are:
-  -srcdir dir   Specify where the Coq source files are
-  -o exec-file  Specify the name of the resulting toplevel
-  -opt          Compile in native code
-  -full         Link high level tactics
-  -top          Build Coq on a ocaml toplevel (incompatible with -opt)
-  -searchisos   Build a toplevel for SearchIsos
-  -ide          Build a toplevel for the Coq IDE
-  -R dir        Specify recursively directories for Ocaml\n";
+  -coqlib dir    Specify where the Coq object files are
+  -camlbin dir   Specify where the OCaml binaries are
+  -camlp4bin dir Specify where the CAmp4/5 binaries are
+  -o exec-file   Specify the name of the resulting toplevel
+  -boot          Run in boot mode
+  -opt           Compile in native code
+  -full          Link high level tactics
+  -top           Build Coq on a ocaml toplevel (incompatible with -opt)
+  -searchisos    Build a toplevel for SearchIsos
+  -ide           Build a toplevel for the Coq IDE
+  -R dir         Specify recursively directories for Ocaml\n";
   exit 1
 
 (* parsing of the command line *)
 let parse_args () =
   let rec parse (op,fl) = function
     | [] -> List.rev op, List.rev fl
-    | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem
-    | "-srcdir" :: _        -> usage ()
+    | "-coqlib" :: d :: rem -> 
+	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
+    | "-coqlib" :: _        -> usage ()
+    | "-camlbin" :: d :: rem -> 
+	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-camlbin" :: _        -> usage ()
+    | "-camlp4bin" :: d :: rem -> 
+	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
+    | "-camlp4bin" :: _        -> usage ()
+    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
     | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
@@ -254,16 +266,17 @@ let create_tmp_main_file modules =
 let main () =
   let (options, userfiles) = parse_args () in
   (* which ocaml command to invoke *)
+  let camlbin = Envars.camlbin () in
   let prog =
     if !opt then begin
       (* native code *)
       if !top then failwith "no custom toplevel in native code !";
-      let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in
+      let ocamloptexec = Filename.concat camlbin "ocamlopt" in
         ocamloptexec^" -linkall"
     end else
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
       let ocamlmktoplib = " toplevellib.cma" in
-      let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
+      let ocamlcexec = Filename.concat camlbin "ocamlc" in
       let ocamlccustom = Printf.sprintf "%s %s -linkall "
         ocamlcexec Coq_config.coqrunbyteflags in
       (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
@@ -282,22 +295,22 @@ let main () =
   try
     let args =
       options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
-    (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
+      (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
-    (* Now, with the .cma, we MUST use the -linkall option *)
+      (* Now, with the .cma, we MUST use the -linkall option *)
     let command = String.concat " " (prog::"-rectypes"::args) in
-    if !echo then 
-      begin 
-	print_endline command; 
-	print_endline 
-	  ("(command length is " ^ 
-	   (string_of_int (String.length command)) ^ " characters)");
-	flush Pervasives.stdout 
-      end;
-    let retcode = Sys.command command in
-    clean main_file;
-    (* command gives the exit code in HSB, and signal in LSB !!! *)
-    if retcode > 255 then retcode lsr 8 else retcode 
+      if !echo then 
+	begin 
+	  print_endline command; 
+	  print_endline 
+	    ("(command length is " ^ 
+	       (string_of_int (String.length command)) ^ " characters)");
+	  flush Pervasives.stdout 
+	end;
+      let retcode = Sys.command command in
+	clean main_file;
+	(* command gives the exit code in HSB, and signal in LSB !!! *)
+	if retcode > 255 then retcode lsr 8 else retcode 
   with e -> 
     clean main_file; raise e