From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- lib/flags.ml | 155 +++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 108 insertions(+), 47 deletions(-) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index f6d98ba5..c8e7f7af 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* o := old; raise reraise + try let r = f x in if !o = true then o := old; r + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = o := old in + Exninfo.iraise reraise + +let with_options ol f x = + let vl = List.map (!) ol in + let () = List.iter (fun r -> r := true) ol in + try + let r = f x in + let () = List.iter2 (:=) ol vl in r + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = List.iter2 (:=) ol vl in + Exninfo.iraise reraise let without_option o f x = let old = !o in o:=false; + try let r = f x in if !o = false then o := old; r + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = o := old in + Exninfo.iraise reraise + +let with_extra_values o l f x = + let old = !o in o:=old@l; try let r = f x in o := old; r - with reraise -> o := old; raise reraise + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = o := old in + Exninfo.iraise reraise let boot = ref false - +let load_init = ref true let batch_mode = ref false -let debug = ref false +type compilation_mode = BuildVo | BuildVio | Vio2Vo +let compilation_mode = ref BuildVo + +type async_proofs = APoff | APonLazy | APon +let async_proofs_mode = ref APoff +type cache = Force +let async_proofs_cache = ref None +let async_proofs_n_workers = ref 1 +let async_proofs_n_tacworkers = ref 2 +let async_proofs_private_flags = ref None +let async_proofs_full = ref false +let async_proofs_never_reopen_branch = ref false +let async_proofs_flags_for_workers = ref [] +let async_proofs_worker_id = ref "master" +type priority = Low | High +let async_proofs_worker_priority = ref Low +let string_of_priority = function Low -> "low" | High -> "high" +let priority_of_string = function + | "low" -> Low + | "high" -> High + | _ -> raise (Invalid_argument "priority_of_string") + +let async_proofs_is_worker () = + !async_proofs_worker_id <> "master" +let async_proofs_is_master () = + !async_proofs_mode = APon && !async_proofs_worker_id = "master" -let print_emacs = ref false +let debug = ref false +let in_debugger = ref false +let in_toplevel = ref false -let term_quality = ref false +let profile = false -let xml_export = ref false +let print_emacs = ref false +let coqtop_ui = ref false -type load_proofs = Force | Lazy | Dont +let ide_slave = ref false +let ideslave_coqtop_flags = ref None -let load_proofs = ref Lazy +let time = ref false let raw_print = ref false let record_print = ref true +let univ_print = ref false + +let we_are_parsing = ref false + (* Compatibility mode *) (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_2 | V8_3 | Current +type compat_version = V8_2 | V8_3 | V8_4 | Current + let compat_version = ref Current -let version_strictly_greater v = !compat_version > v + +let version_strictly_greater v = match !compat_version, v with +| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false +| V8_3, (V8_3 | V8_4 | Current) -> false +| V8_4, (V8_4 | Current) -> false +| Current, Current -> false +| V8_3, V8_2 -> true +| V8_4, (V8_2 | V8_3) -> true +| Current, (V8_2 | V8_3 | V8_4) -> true + let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_2 -> "8.2" | V8_3 -> "8.3" + | V8_4 -> "8.4" | Current -> "current" (* Translate *) @@ -73,7 +142,23 @@ let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros -let hash_cons_proofs = ref true +let universe_polymorphism = ref false +let make_universe_polymorphism b = universe_polymorphism := b +let is_universe_polymorphism () = !universe_polymorphism + +let local_polymorphic_flag = ref None +let use_polymorphic_flag () = + match !local_polymorphic_flag with + | Some p -> local_polymorphic_flag := None; p + | None -> is_universe_polymorphism () +let make_polymorphic_flag b = + local_polymorphic_flag := Some b + +(** [program_mode] tells that Program mode has been activated, either + globally via [Set Program] or locally via the Program command prefix. *) + +let program_mode = ref false +let is_program_mode () = !program_mode let warn = ref true let make_warn flag = warn := flag; () @@ -85,28 +170,8 @@ let print_hyps_limit = ref (None : int option) let set_print_hyps_limit n = print_hyps_limit := n let print_hyps_limit () = !print_hyps_limit -(* A list of the areas of the system where "unsafe" operation - * has been requested *) - -module Stringset = Set.Make(struct type t = string let compare = compare end) - -let unsafe_set = ref Stringset.empty -let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set -let is_unsafe s = Stringset.mem s !unsafe_set - (* Flags for external tools *) -let subst_command_placeholder s t = - let buff = Buffer.create (String.length s + String.length t) in - let i = ref 0 in - while (!i < String.length s) do - if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's' - then (Buffer.add_string buff t;incr i) - else Buffer.add_char buff s.[!i]; - incr i - done; - Buffer.contents buff - let browser_cmd_fmt = try let coq_netscape_remote_var = "COQREMOTEBROWSER" in @@ -122,21 +187,9 @@ let is_standard_doc_url url = url = Coq_config.wwwrefman || url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) -(* same as in System, but copied here because of dependencies *) -let canonical_path_name p = - let current = Sys.getcwd () in - Sys.chdir p; - let result = Sys.getcwd () in - Sys.chdir current; - result - (* 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 @@ -152,3 +205,11 @@ let default_inline_level = 100 let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level + +(* Disabling native code compilation for conversion and normalization *) +let no_native_compiler = ref Coq_config.no_native_compiler + +(* Print the mod uid associated to a vo file by the native compiler *) +let print_mod_uid = ref false + +let tactic_context_compat = ref false -- cgit v1.2.3