Misc changes around coqtop.ml :

 - Revised Coqtop.parse_args in a cleaner and lighter style
 - Improved error message in case of argument parse failure:
   * tell which option is expecting a related argument
   * in case of unknown options, warn about them all at once
   * do not hide the previous error messages by filling the
     screen with usage(). Instead, suggest the use of --help.
 - Specialized boolean config field Coq_config.arch_is_win32
 - Faster Envars.coqlib, which is back to (unit->string), and
   just access Flags.coqlib. Caveat: it must be initialized once
   via Envars.set_coqlib
 - Avoid keeping an opened channel to the "revision" file
 - Direct load of theories/init/prelude.vo, no detour via Loadpath

Beware : ./configure must be runned after this commit

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

4 files changed, 25 insertions, 14 deletions

diff --git a/tools/coqc.ml b/tools/coqc.ml
index e15a1768c..2d9c2fd33 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -117,9 +117,14 @@ let parse_args () =
     | ("-v"|"--version") :: _ -> Usage.version 0
 
     | ("-where") :: _ ->
-	print_endline (Envars.coqlib (fun x -> x)); exit 0
+        Envars.set_coqlib (fun x -> x);
+        print_endline (Envars.coqlib ());
+        exit 0
 
-    | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
+    | ("-config" | "--config") :: _ ->
+        Envars.set_coqlib (fun x -> x);
+        Usage.print_config ();
+        exit 0
 
 (* Options for coqtop : a) options with 0 argument *)
 
@@ -132,7 +137,7 @@ let parse_args () =
       |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
 	parse (cfiles,o::args) rem
 
-(* Options for coqtop : a) options with 1 argument *)
+(* Options for coqtop : b) options with 1 argument *)
 
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
@@ -144,7 +149,7 @@ let parse_args () =
 	    | []        -> usage ()
 	end
 
-(* Options for coqtop : a) options with 1 argument and possibly more *)
+(* Options for coqtop : c) options with 1 argument and possibly more *)
 
     | ("-I"|"-include" as o) :: rem ->
 	begin
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f296594d1..16e5bbde8 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -198,7 +198,8 @@ let coqdep () =
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"]
   end else begin
-    let coqlib = Envars.coqlib Errors.error in
+    Envars.set_coqlib ~fail:Errors.error;
+    let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 070778fb2..b356ac537 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let ( / ) = Filename.concat
+
 let coqdoc_out f =
   if !output_dir <> "" && Filename.is_relative f then
     if not (Sys.file_exists !output_dir) then
       (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
     else
-      Filename.concat !output_dir f
+      !output_dir / f
   else
     f
 
@@ -73,15 +75,17 @@ let normalize_filename f =
 let guess_coqlib () =
   let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
-      coqlib
+    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
     | Some _ | None ->
       let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      let rpath =
+        if Coq_config.local then []
+        else if Coq_config.arch_is_win32 then ["lib"]
+        else ["lib/coq"]
+      in
+      let coqlib = List.fold_left (/) prefix rpath in
+      if Sys.file_exists (coqlib / file) then coqlib
       else prefix
 
 let header_trailer = ref true
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 39a8ede9a..0ab732da2 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -72,10 +72,10 @@ let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
    below (for accessing the corresponding .cmi). *)
 
 let src_dirs =
-  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]  ]
+  [ []; ["lib"]; ["toplevel"]; ["kernel/byterun"]  ]
 
 let includes () =
-  let coqlib = if !Flags.boot then "." else Envars.coqlib ~fail:Errors.error in
+  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
   let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
   (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
   @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
@@ -259,6 +259,7 @@ let create_tmp_main_file modules =
 (* main part *)
 let main () =
   let (options, userfiles) = parse_args () in
+  let () = Envars.set_coqlib ~fail:Errors.error in
   (* which ocaml command to invoke *)
   let camlbin = Envars.camlbin () in
   let prog =