diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 5 | ||||
| -rw-r--r-- | lib/control.mli | 5 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 15 | ||||
| -rw-r--r-- | lib/flags.ml | 9 | ||||
| -rw-r--r-- | lib/flags.mli | 32 |
5 files changed, 39 insertions, 27 deletions
diff --git a/lib/control.ml b/lib/control.ml index e67cd8b38d..3fbeb168c4 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } | _ -> { timeout = windows_timeout } -let timeout n f e = timeout_fun.timeout n f e +let timeout_fun_ref = ref timeout_fun +let set_timeout f = timeout_fun_ref := f + +let timeout n f e = !timeout_fun_ref.timeout n f e diff --git a/lib/control.mli b/lib/control.mli index 415e054625..59e2a15158 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b (** [timeout n f x e] tries to compute [f x], and if it fails to do so before [n] seconds, it raises [e] instead. *) + +(** Set a particular timeout function; warning, this is an internal + API and it is scheduled to go away. *) +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +val set_timeout : timeout -> unit diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index d6c340f691..61eb1dafdf 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,6 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* This needs to go trou feedback as it is invoked from IDEs, but + ideally we would like to make this independent so it can be + bootstrapped. *) + +(* Note the problem with the error invokation below calling exit... *) +(* let error msg = Feedback.msg_error msg *) +let warning msg = Feedback.msg_warning Pp.(str msg) + type arg_source = CmdLine | ProjectFile type 'a sourced = { thing : 'a; source : arg_source } @@ -122,7 +130,7 @@ let process_cmd_line orig_dir proj args = let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in - let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in + let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in let mk_path d = let p = CUnix.correct_path d orig_dir in { path = CUnix.remove_path_dot (post_canonize p); @@ -140,7 +148,7 @@ let process_cmd_line orig_dir proj args = | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> if proj.install_kind <> None then - Feedback.msg_warning (Pp.str "-install set more than once."); + (warning "-install set more than once.@\n%!"); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -167,8 +175,7 @@ let process_cmd_line orig_dir proj args = let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () - | Some _ -> Feedback.msg_warning (Pp.str - "Multiple project files are deprecated.") + | Some _ -> warning "Multiple project files are deprecated.@\n%!" in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in diff --git a/lib/flags.ml b/lib/flags.ml index 8491873e07..56940f1cf7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,6 @@ let profile = false let ide_slave = ref false let raw_print = ref false -let univ_print = ref false let we_are_parsing = ref false @@ -160,11 +159,3 @@ let print_mod_uid = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 - -let dump_bytecode = ref false -let set_dump_bytecode = (:=) dump_bytecode -let get_dump_bytecode () = !dump_bytecode - -let dump_lambda = ref false -let set_dump_lambda = (:=) dump_lambda -let get_dump_lambda () = !dump_lambda diff --git a/lib/flags.mli b/lib/flags.mli index 85aaf879f3..17776d68a4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -10,6 +10,25 @@ (** Global options of the system. *) +(** WARNING: don't add new entries to this file! + + This file is own its way to deprecation in favor of a purely + functional state, but meanwhile it will contain options that are + truly global to the system such as [compat] or [debug] + + If you are thinking about adding a global flag, well, just + don't. First of all, options make testins exponentially more + expensive, due to the growth of flag combinations. So please make + some effort in order for your idea to work in a configuration-free + manner. + + If you absolutely must pass an option to your new system, then do + so as a functional argument so flags are exposed to unit + testing. Then, register such parameters with the proper + state-handling mechanism of the top-level subsystem of Coq. + + *) + (** Command-line flags *) val boot : bool ref @@ -42,9 +61,6 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -(* Univ print flag, never set anywere. Maybe should belong to Univ? *) -val univ_print : bool ref - type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int @@ -129,13 +145,3 @@ val print_mod_uid : bool ref val profile_ltac : bool ref val profile_ltac_cutoff : float ref - -(** Dump the bytecode after compilation (for debugging purposes) *) -val dump_bytecode : bool ref -val set_dump_bytecode : bool -> unit -val get_dump_bytecode : unit -> bool - -(** Dump the VM lambda code after compilation (for debugging purposes) *) -val dump_lambda : bool ref -val set_dump_lambda : bool -> unit -val get_dump_lambda : unit -> bool |