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 --- checker/checker.ml | 19 ++- config/coq_config.mli | 1 + configure | 7 +- interp/coqlib.ml | 3 + interp/coqlib.mli | 2 + interp/dumpglob.ml | 8 +- interp/dumpglob.mli | 3 +- kernel/nativelib.ml | 7 +- lib/envars.ml | 67 ++++---- lib/envars.mli | 5 +- lib/flags.ml | 6 +- myocamlbuild.ml | 2 +- plugins/micromega/coq_micromega.ml | 2 +- pretyping/recordops.mli | 1 - tools/coqc.ml | 13 +- tools/coqdep.ml | 3 +- tools/coqdoc/cdglobals.ml | 18 +- tools/coqmktop.ml | 5 +- toplevel/coqinit.ml | 6 +- toplevel/coqtop.ml | 330 +++++++++++++++++-------------------- toplevel/usage.ml | 2 +- 21 files changed, 247 insertions(+), 263 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index 280f34656..d54e9328a 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -42,21 +42,21 @@ let path_of_string s = [] -> invalid_arg "path_of_string" | l::dir -> {dirpath=dir; basename=l} -let (/) = Filename.concat +let ( / ) = Filename.concat let get_version_date () = try - let coqlib = Envars.coqlib error in - let ch = open_in (Filename.concat coqlib "revision") in + let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in - (ver,rev) + let () = close_in ch in + (ver,rev) with _ -> (Coq_config.version,Coq_config.date) let print_header () = let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; - flush stdout + Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; + flush stdout (* Adding files to Coq loadpath *) @@ -107,7 +107,7 @@ let set_rec_include d p = (* Initializes the LoadPath *) let init_load_path () = - let coqlib = Envars.coqlib error in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs in let coqpath = Envars.coqpath in @@ -306,7 +306,9 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - print_endline (Envars.coqlib error); exit 0 + Envars.set_coqlib ~fail:Errors.error; + print_endline (Envars.coqlib ()); + exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -341,6 +343,7 @@ let init_with_argv argv = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) try parse_args argv; + Envars.set_coqlib ~fail:Errors.error; if_verbose print_header (); init_load_path (); engage (); diff --git a/config/coq_config.mli b/config/coq_config.mli index f16ffbe51..94d0b6c93 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -36,6 +36,7 @@ val cflags : string (* arguments passed to gcc *) val best : string (* byte/opt *) val arch : string (* architecture *) +val arch_is_win32 : bool val osdeplibs : string (* OS dependant link options for ocamlc *) val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *) diff --git a/configure b/configure index 43317f1f5..1cfb4f125 100755 --- a/configure +++ b/configure @@ -311,10 +311,12 @@ esac # executable extension case $ARCH in - win32) + win32) + ARCH_WIN32=true EXE=".exe" DLLEXT=".dll";; - *) EXE="" + *) ARCH_WIN32=false + EXE="" DLLEXT=".so" esac @@ -1042,6 +1044,7 @@ let coqideincl = "$LABLGTKINCLUDES" let cflags = "$cflags" let best = "$best_compiler" let arch = "$ARCH" +let arch_is_win32 = $ARCH_WIN32 let has_coqide = "$COQIDE" let gtk_platform = \`$IDEARCHDEF let has_natdynlink = $HASNATDYNLINK diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 2256764a3..aac7f9a28 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -117,6 +117,9 @@ let init_modules = [ init_dir@["Wf"] ] +let prelude_module_name = init_dir@["Prelude"] +let prelude_module = make_dir prelude_module_name + let logic_module_name = init_dir@["Logic"] let logic_module = make_dir logic_module_name diff --git a/interp/coqlib.mli b/interp/coqlib.mli index b8e461665..9e0cfadae 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -54,6 +54,8 @@ val check_required_library : string list -> unit (** {6 Global references } *) (** Modules *) +val prelude_module : DirPath.t + val logic_module : DirPath.t val logic_module_name : string list diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 74c60f75b..1a44fac6c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -30,11 +30,13 @@ let dump () = !glob_output != NoGlob let noglob () = glob_output := NoGlob -let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout - let dump_to_dotglob () = glob_output := MultFiles -let dump_into_file f = glob_output := File f; open_glob_file f +let dump_into_file f = + if String.equal f "stdout" then + (glob_output := StdOut; glob_file := Pervasives.stdout) + else + (glob_output := File f; open_glob_file f) let dump_string s = if dump () then Pervasives.output_string !glob_file s diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index edea94f0c..37370f6e1 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -15,8 +15,7 @@ val end_dump_glob : unit -> unit val dump : unit -> bool val noglob : unit -> unit -val dump_to_stdout : unit -> unit -val dump_into_file : string -> unit +val dump_into_file : string -> unit (** special handling of "stdout" *) val dump_to_dotglob : unit -> unit val pause : unit -> unit diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 6b2b4aa7c..c9da5222f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -32,13 +32,12 @@ let open_header = List.map mk_open open_header let compiler_name = Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ()) -let ( / ) a b = Filename.concat a b +let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) -let include_dirs () = [Filename.temp_dir_name; - coqlib ~fail:Errors.error / "kernel"; - coqlib ~fail:Errors.error / "library"] +let include_dirs () = + [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) diff --git a/lib/envars.ml b/lib/envars.ml index cf3d6503d..5e20df358 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -87,53 +87,48 @@ let coqbin = (** The following only makes sense when executables are running from source tree (e.g. during build or in local mode). *) -let coqroot = +let coqroot = Filename.dirname coqbin - + (** On win32, we add coqbin to the PATH at launch-time (this used to be done in a .bat script). *) let _ = - if String.equal Coq_config.arch "win32" then + if Coq_config.arch_is_win32 then Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) -(** [reldir instdir testfile oth] checks if [testfile] exists in - the installation directory [instdir] given relatively to - [coqroot]. If this Coq is only locally built, then [testfile] - must be found at [coqroot]. +(** [check_file_else ~dir ~file oth] checks if [file] exists in + the installation directory [dir] given relatively to [coqroot]. + If this Coq is only locally built, then [file] must be in [coqroot]. If the check fails, then [oth ()] is evaluated. *) -let reldir instdir testfile oth = - let rpath = if Coq_config.local then [] else instdir in - let out = List.fold_left ( / ) coqroot rpath in - if Sys.file_exists (out / testfile) then out else oth () +let check_file_else ~dir ~file oth = + let path = if Coq_config.local then coqroot else coqroot / dir in + if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = - let file = "theories/Init/Prelude.vo" in - reldir (if String.equal Coq_config.arch "win32" then ["lib"] else ["lib";"coq"]) file - (fun () -> - let coqlib = match Coq_config.coqlib with - | Some coqlib -> coqlib - | None -> coqroot - in - if Sys.file_exists (coqlib / file) then - coqlib - else - fail "cannot guess a path for Coq libraries; please use -coqlib option") - -let coqlib ~fail = - if !Flags.coqlib_spec then - !Flags.coqlib - else if !Flags.boot then - coqroot - else - guess_coqlib fail + let prelude = "theories/Init/Prelude.vo" in + let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in + check_file_else ~dir ~file:prelude + (fun () -> + let coqlib = match Coq_config.coqlib with + | Some coqlib -> coqlib + | None -> coqroot + in + if Sys.file_exists (coqlib / prelude) then coqlib + else + fail "cannot guess a path for Coq libraries; please use -coqlib option") + +(** coqlib is now computed once during coqtop initialization *) + +let set_coqlib ~fail = + if not !Flags.coqlib_spec then + let lib = if !Flags.boot then coqroot else guess_coqlib fail in + Flags.coqlib := lib + +let coqlib () = !Flags.coqlib let docdir () = - reldir ( - if String.equal Coq_config.arch "win32" then - ["doc"] - else - ["share";"doc";"coq"] - ) "html" (fun () -> Coq_config.docdir) + let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in + check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir) let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in diff --git a/lib/envars.mli b/lib/envars.mli index c0142a8d7..19ba8d2c0 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -25,7 +25,10 @@ val expand_path_macros : warn:(string -> unit) -> string -> string val home : warn:(string -> unit) -> string (** [coqlib] is the path to the Coq library. *) -val coqlib : fail:(string -> string) -> string +val coqlib : unit -> string + +(** [set_coqlib] must be runned once before any access to [coqlib] *) +val set_coqlib : fail:(string -> string) -> unit (** [docdir] is the path to the Coq documentation. *) val docdir : unit -> string diff --git a/lib/flags.ml b/lib/flags.ml index 43ebe1491..9f4e81408 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -168,11 +168,7 @@ let canonical_path_name p = (* Options for changing coqlib *) let coqlib_spec = ref false -let coqlib = ref ( - (* same as Envars.coqroot, but copied here because of dependencies *) - Filename.dirname - (canonical_path_name (Filename.dirname Sys.executable_name)) -) +let coqlib = ref "(not initialized yet)" (* Options for changing camlbin (used by coqmktop) *) let camlbin_spec = ref false diff --git a/myocamlbuild.ml b/myocamlbuild.ml index a0e2e7ef7..5a03470a4 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -58,7 +58,7 @@ let _ = begin Options.ocamllex := A Coq_config.ocamllex; end -let w32 = (Coq_config.arch = "win32") +let w32 = Coq_config.arch_is_win32 let w32pref = "i586-mingw32msvc" let w32ocamlc = w32pref^"-ocamlc" diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index eff1d4ba9..082814655 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1764,7 +1764,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste Lazy.force require_csdp; let cmdname = - List.fold_left Filename.concat (Envars.coqlib ~fail:Errors.error) + List.fold_left Filename.concat (Envars.coqlib ()) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 6afba15bf..11e558a76 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -11,7 +11,6 @@ open Nametab open Term open Globnames open Libobject -open Library (** Operations concerning records and canonical structures *) 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 = diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index dfe576a69..3841f4f9c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -9,7 +9,7 @@ open Util open Pp -let (/) = Filename.concat +let ( / ) = Filename.concat let set_debug () = let () = Backtrace.record_backtrace true in @@ -97,7 +97,7 @@ let theories_dirs_map = [ (* Initializes the LoadPath *) let init_load_path () = - let coqlib = Envars.coqlib ~fail:Errors.error in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in let coqpath = Envars.coqpath in @@ -135,7 +135,7 @@ let init_ocaml_path () = let add_subdir dl = Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in - Mltop.add_ml_dir (Envars.coqlib ~fail:Errors.error); + Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c0b47f0c1..79467cacd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -18,22 +18,24 @@ open Coqinit let () = at_exit flush_all +let ( / ) = Filename.concat + let fatal_error info = pperrnl info; flush_all (); exit 1 let get_version_date () = try - let coqlib = Envars.coqlib ~fail:Errors.error in - let ch = open_in (Filename.concat coqlib "revision") in + let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in - (ver,rev) + let () = close_in ch in + (ver,rev) with e when Errors.noncritical e -> (Coq_config.version,Coq_config.date) let print_header () = - let (ver,rev) = (get_version_date ()) in - pp (str "Welcome to Coq "++ str ver ++ str " (" ++ str rev ++ str ")" ++ fnl ()); + let (ver,rev) = get_version_date () in + ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); pp_flush () let output_context = ref false @@ -42,7 +44,8 @@ let memory_stat = ref false let print_memory_stat () = if !memory_stat then - pp (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()) + ppnl + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes") let _ = at_exit print_memory_stat @@ -99,8 +102,8 @@ let load_vernac_obj () = let load_init = ref true let require_prelude () = - let q = qualid_of_string "Coq.Init.Prelude" in - Library.require_library [Loc.ghost,q] (Some true) + let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in + Library.require_library_from_dirpath [Coqlib.prelude_module,vo] (Some true) let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list @@ -111,10 +114,12 @@ let require () = let compile_list = ref ([] : (bool * string) list) -let add_compile verbose glob_opt s = +let glob_opt = ref false + +let add_compile verbose s = set_batch_mode (); Flags.make_silent true; - if not glob_opt then Dumpglob.dump_to_dotglob (); + if not !glob_opt then Dumpglob.dump_to_dotglob (); compile_list := (verbose,s) :: !compile_list let compile_file (v,f) = @@ -146,6 +151,14 @@ let set_vm_opt () = Vm.set_transp_values (not !boxed_val); Vconv.set_use_vm !use_vm +(** Options for proof general *) + +let set_emacs () = + Flags.print_emacs := true; + Pp.make_pp_emacs (); + Vernacentries.qed_display_script := false; + Flags.make_term_color false + (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the @@ -182,186 +195,134 @@ let usage () = flush stderr ; exit 1 +let error_missing_arg s = + prerr_endline ("Error: extra argument expected after option "^s); + prerr_endline "See --help for the syntax of supported options"; + exit 1 + let warning s = msg_warning (strbrk s) let filter_opts = ref false +let exitcode () = if !filter_opts then 2 else 0 let verb_compat_ntn = ref false let no_compat_ntn = ref false -let parse_args arglist = - let glob_opt = ref false in - let rec parse = function - | [] -> [] - | "-with-geoproof" :: s :: rem -> - if String.equal s "yes" then Coq_config.with_geoproof := true - else if String.equal s "no" then Coq_config.with_geoproof := false - else usage (); - parse rem - | "-impredicative-set" :: rem -> - set_engagement Declarations.ImpredicativeSet; parse rem - - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem - | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem - | ("-I"|"-include") :: [] -> usage () - - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: ([] | [_]) -> usage () - - | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem - | "-top" :: [] -> usage () - - | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem - | "-exclude-dir" :: [] -> usage () - - | "-notop" :: rem -> unset_toplevel_name (); parse rem - | "-q" :: rem -> no_load_rc (); parse rem - - | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem - | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem - | "-full" :: rem -> warning "option -full deprecated\n"; parse rem - - | "-batch" :: rem -> set_batch_mode (); parse rem - | "-boot" :: rem -> boot := true; no_load_rc (); parse rem - | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem - | "-outputstate" :: s :: rem -> set_outputstate s; parse rem - | "-outputstate" :: [] -> usage () - - | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem - - | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem - | ("-inputstate"|"-is") :: [] -> usage () - - | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem - | "-load-ml-object" :: [] -> usage () - - | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem - | "-load-ml-source" :: [] -> usage () - - | ("-load-vernac-source"|"-l") :: f :: rem -> - add_load_vernacular false f; parse rem - | ("-load-vernac-source"|"-l") :: [] -> usage () - - | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> - add_load_vernacular true f; parse rem - | ("-load-vernac-source-verbose"|"-lv") :: [] -> usage () - - | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem - | "-load-vernac-object" :: [] -> usage () - - | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem - (* À ne pas documenter : l'option 'stdout' n'étant - éventuellement utile que pour le debugging... *) - | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem - | "-dump-glob" :: [] -> usage () - | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem - - | "-require" :: f :: rem -> add_require f; parse rem - | "-require" :: [] -> usage () - - | "-print-mod-uid" :: f :: rem -> Flags.print_mod_uid := true; - add_require f; parse rem - - | "-compile" :: f :: rem -> add_compile false !glob_opt f; parse rem - | "-compile" :: [] -> usage () - - | "-compile-verbose" :: f :: rem -> add_compile true !glob_opt f; parse rem - | "-compile-verbose" :: [] -> usage () - - | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem - | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem - | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem - - | "-beautify" :: rem -> make_beautify true; parse rem +let print_where = ref false +let print_config = ref false - | "-unsafe" :: f :: rem -> add_unsafe f; parse rem - | "-unsafe" :: [] -> usage () +let get_slave_number = function + | "off" -> -1 + | "on" -> 0 + | s -> let n = int_of_string s in assert (n > 0); n - | "-debug" :: rem -> set_debug (); parse rem +let get_bool opt = function + | "yes" -> true + | "no" -> false + | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 - | "-time" :: rem -> Flags.time := true; parse rem - - | "-compat" :: v :: rem -> - Flags.compat_version := get_compat_version v; parse rem - | "-compat" :: [] -> usage () - - | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem - | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem - - | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> - Flags.print_emacs := true; Pp.make_pp_emacs(); - Vernacentries.qed_display_script := false; - Flags.make_term_color false; - parse rem - | "-emacs-U" :: rem -> - warning "Obsolete option \"-emacs-U\", use -emacs instead."; - Flags.make_term_color false; - parse ("-emacs" :: rem) - - | "-coq-slaves" :: "off" :: rem -> Flags.coq_slave_mode := -1; parse rem - | "-coq-slaves" :: "on" :: rem -> Flags.coq_slave_mode := 0; parse rem - - | "-coq-slaves" :: n :: rem -> (* internal use *) - assert (int_of_string n > 0); - Flags.coq_slave_mode := int_of_string n; - parse rem - - | "-unicode" :: rem -> add_require "Utf8_core"; parse rem - - | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem - | "-coqlib" :: [] -> usage () - - | "-where" :: _ -> - print_endline (Envars.coqlib ~fail:Errors.error); - exit (if !filter_opts then 2 else 0) - - | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) - - | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem - - | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - - | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0) - - | "-init-file" :: f :: rem -> set_rcfile f; parse rem - | "-init-file" :: [] -> usage () - - | "-notactics" :: rem -> - warning "Obsolete option \"-notactics\"."; - remove_top_ml (); parse rem - - | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem - - | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem - - | "-xml" :: rem -> Flags.xml_export := true; parse rem - - | "-output-context" :: rem -> output_context := true; parse rem - - (* Scanned in Flags. *) - | "-v7" :: rem -> error "This version of Coq does not support v7 syntax" - | "-v8" :: rem -> parse rem - - | "-ideslave" :: rem -> Flags.ide_slave := true; parse rem - - | "-filteropts" :: rem -> filter_opts := true; parse rem - - | "-color" :: rem -> Flags.make_term_color true; parse rem - - | "-no-native-compiler" :: rem -> no_native_compiler := true; parse rem - - | s :: rem -> - if !filter_opts then - s :: (parse rem) - else - (prerr_endline ("Don't know what to do with " ^ s); usage ()) +let parse_args arglist = + let args = ref arglist in + let extras = ref [] in + let rec parse () = match !args with + | [] -> List.rev !extras + | opt :: rem -> + args := rem; + let next () = match rem with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: "-as" :: p :: rem -> set_include d p; args := rem + | d :: "-as" :: [] -> error_missing_arg "-as" + | d :: rem -> set_default_include d; args := rem + | [] -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: "-as" :: p :: rem -> set_rec_include d p; args := rem + | d :: "-as" :: [] -> error_missing_arg "-as" + | d :: p :: rem -> set_rec_include d p; args := rem + | _ -> error_missing_arg opt + end + + (* Options with one arg *) + |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) + |"-coq-slaves" -> Flags.coq_slave_mode := (get_slave_number (next ())) + |"-compat" -> Flags.compat_version := get_compat_version (next ()) + |"-compile" -> add_compile false (next ()) + |"-compile-verbose" -> add_compile true (next ()) + |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true + |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-init-file" -> set_rcfile (next ()) + |"-inputstate"|"-is" -> set_inputstate (next ()) + |"-load-ml-object" -> Mltop.dir_ml_load (next ()) + |"-load-ml-source" -> Mltop.dir_ml_use (next ()) + |"-load-vernac-object" -> add_vernac_obj (next ()) + |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) + |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) + |"-outputstate" -> set_outputstate (next ()) + |"-print-mod-uid" -> Flags.print_mod_uid := true; add_require (next ()) + |"-require" -> add_require (next ()) + |"-top" -> set_toplevel_name (dirpath_of_string (next ())) + |"-unsafe" -> add_unsafe (next ()) + |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) + + (* Options with zero arg *) + |"-batch" -> set_batch_mode () + |"-beautify" -> make_beautify true + |"-boot" -> boot := true; no_load_rc () + |"-color" -> Flags.make_term_color true + |"-config"|"--config" -> print_config := true + |"-debug" -> set_debug () + |"-dont-load-proofs" -> Flags.load_proofs := Flags.Dont + |"-emacs" -> set_emacs () + |"-filteropts" -> filter_opts := true + |"-force-load-proofs" -> Flags.load_proofs := Flags.Force + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () + |"-ideslave" -> Flags.ide_slave := true + |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet + |"-just-parsing" -> Vernac.just_parsing := true + |"-lazy-load-proofs" -> Flags.load_proofs := Flags.Lazy + |"-m"|"--memory" -> memory_stat := true + |"-noinit"|"-nois" -> load_init := false + |"-no-compat-notations" -> no_compat_ntn := true + |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true + |"-no-native-compiler" -> no_native_compiler := true + |"-notop" -> unset_toplevel_name () + |"-output-context" -> output_context := true + |"-q" -> no_load_rc () + |"-quality" -> term_quality := true; no_load_rc () + |"-quiet"|"-silent" -> Flags.make_silent true + |"-time" -> Flags.time := true + |"-unicode" -> add_require "Utf8_core" + |"-v"|"--version" -> Usage.version (exitcode ()) + |"-verbose-compat-notations" -> verb_compat_ntn := true + |"-vm" -> use_vm := true + |"-where" -> print_where := true + |"-xml" -> Flags.xml_export := true + + (* Deprecated options *) + |"-byte" -> warning "option -byte deprecated, call with .byte suffix" + |"-opt" -> warning "option -opt deprecated, call with .opt suffix" + |"-full" -> warning "option -full deprecated" + |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () + |"-emacs-U" -> + warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () + |"-v7" -> error "This version of Coq does not support v7 syntax" + |"-v8" -> warning "Obsolete option \"-v8\"." + + (* Unknown option *) + | s -> extras := s :: !extras + end; + parse () in try - parse arglist + parse () with | UserError(_, s) as e -> if is_empty s then exit 1 @@ -376,9 +337,16 @@ let init arglist = Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic"; begin try - let foreign_args = parse_args arglist in - if !filter_opts then - (print_string (String.concat "\n" foreign_args); exit 0); + let extras = parse_args arglist in + if not (List.is_empty extras) && not !filter_opts then begin + prerr_endline ("Don't know what to do with " ^ String.concat " " extras); + prerr_endline "See --help for the list of supported options"; + exit 1 + end; + Envars.set_coqlib Errors.error; + if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ())); + if !print_config then (Usage.print_config (); exit (exitcode ())); + if !filter_opts then (print_string (String.concat "\n" extras); exit 0); if !Flags.ide_slave then begin Flags.make_silent true; Ide_slave.init_stdout () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 1bfc8f701..e9e576962 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -94,7 +94,7 @@ let print_usage_coqc () = let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" (Envars.coqlib ~fail:Errors.error); + Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; -- cgit v1.2.3