diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 109 |
1 files changed, 28 insertions, 81 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index d4be81c61a..5da1310206 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,13 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let with_option o f x = - let old = !o in o:=true; - 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 +(* If [restore] is false, whenever [f] modifies the ref, we will + preserve the modification. *) +let with_modified_ref ?(restore=true) r nf f x = + let old_ref = !r in r := nf !r; + try + let pre = !r in + let res = f x in + (* If r was modified don't restore its old value *) + if restore || pre == !r then r := old_ref; + res + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + r := old_ref; + Exninfo.iraise reraise + +let with_option o f x = with_modified_ref ~restore:false o (fun _ -> true) f x +let without_option o f x = with_modified_ref ~restore:false o (fun _ -> false) f x +let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x + +(* hide the [restore] option as internal *) +let with_modified_ref r nf f x = with_modified_ref r nf f x let with_options ol f x = let vl = List.map (!) ol in @@ -25,62 +39,16 @@ let with_options ol f x = 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 -> - 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 -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None +let record_aux_file = ref false let test_mode = ref false -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") -type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) -let async_proofs_cmd_error_resilience = ref true - -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 async_proofs_delegation_threshold = ref 0.03 +let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let debug = ref false -let stm_debug = ref false let in_debugger = ref false let in_toplevel = ref false @@ -88,12 +56,8 @@ let in_toplevel = ref false let profile = false let ide_slave = ref false -let ideslave_coqtop_flags = ref None - -let time = ref false let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false @@ -144,10 +108,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let make_silent flag = quiet := flag -let is_silent () = !quiet -let is_verbose () = not !quiet - let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = !auto_intros @@ -156,14 +116,6 @@ 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 - let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity @@ -199,14 +151,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 @@ -215,15 +159,18 @@ let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) -let native_compiler = ref false +let output_native_objects = ref false (* 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 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 |