From 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 Aug 2013 14:29:58 +0000 Subject: 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 --- tools/coqc.ml | 13 +++++++++---- tools/coqdep.ml | 3 ++- tools/coqdoc/cdglobals.ml | 18 +++++++++++------- tools/coqmktop.ml | 5 +++-- 4 files changed, 25 insertions(+), 14 deletions(-) (limited to 'tools') 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 = -- cgit v1.2.3