diff options
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 22 | ||||
| -rw-r--r-- | sysinit/coqloadpath.ml | 14 | ||||
| -rw-r--r-- | sysinit/dune | 5 | ||||
| -rw-r--r-- | sysinit/usage.ml | 7 |
4 files changed, 27 insertions, 21 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 56d88e6bd6..8be73ca028 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -22,14 +22,6 @@ let error_missing_arg s = exit 1 (******************************************************************************) -(* Imperative effects! This must be fixed at some point. *) -(******************************************************************************) - -let set_debug () = - let () = Exninfo.record_backtrace true in - Flags.debug := true - -(******************************************************************************) type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } @@ -168,6 +160,9 @@ let add_load_vernacular opts verb s = let add_set_option opts opt_name value = { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }} +let add_set_debug opts flags = + add_set_option opts ["Debug"] (OptionAppend flags) + (** Options for proof general *) let set_emacs opts = let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in @@ -382,10 +377,15 @@ let parse_args ~usage ~init arglist : t * string list = (* Options with zero arg *) |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Exninfo.record_backtrace true; oval + |"-bt" -> add_set_debug oval "backtrace" |"-config"|"--config" -> set_query oval PrintConfig - |"-debug" -> set_debug (); oval - |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval + + |"-debug" -> add_set_debug oval "all" + |"-d" | "-D" -> add_set_debug oval (next()) + + (* -xml-debug implies -debug. TODO don't be imperative here. *) + |"-xml-debug" -> Flags.xml_debug := true; add_set_debug oval "all" + |"-diffs" -> add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) |"-emacs" -> set_emacs oval diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml index 8635345e00..95ae5da3de 100644 --- a/sysinit/coqloadpath.ml +++ b/sysinit/coqloadpath.ml @@ -44,8 +44,18 @@ let init_load_path ~coqlib = let coq_path = Names.DirPath.make [Libnames.coq_root] in (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in - + let unix_path = + (* Usually lib/coq-stdlib/../plugins ; this kind of hacks with the + ML path should go away once we use ocamlfind to load plugins *) + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") + | Some f -> (f :> string) + in + let plugins_dirs = System.all_subdirs ~unix_path |> List.map fst in let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in let misc_ml, misc_vo = diff --git a/sysinit/dune b/sysinit/dune index 04b46fb2a2..f882f987ff 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -1,7 +1,6 @@ (library (name sysinit) - (public_name coq.sysinit) + (public_name coq-core.sysinit) (synopsis "Coq's initialization") (wrapped false) - (libraries coq.vernac) - ) + (libraries coq-core.vernac)) diff --git a/sysinit/usage.ml b/sysinit/usage.ml index 763cd54137..5886b1c5b5 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -9,9 +9,8 @@ (************************************************************************) let version () = - Printf.printf "The Coq Proof Assistant, version %s (%s)\n" - Coq_config.version Coq_config.date; - Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version + Printf.printf "The Coq Proof Assistant, version %s\n" Coq_config.version; + Printf.printf "compiled with OCaml %s\n" Coq_config.caml_version let machine_readable_version () = Printf.printf "%s %s\n" @@ -74,8 +73,6 @@ let print_usage_common co command = \n -debug debug mode (implies -bt)\ \n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ -\n -noglob do not dump globalizations\ -\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ \n -disallow-sprop forbid using the proof irrelevant SProp sort\ |