From cb316573aa1d09433531e7c67e320c14ef05c3e2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Mar 2017 18:38:42 +0100 Subject: [option] Remove support for non-synchronous options. Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. --- library/goptions.ml | 47 +++++++++-------------------------------------- library/goptions.mli | 11 ++--------- 2 files changed, 11 insertions(+), 47 deletions(-) (limited to 'library') diff --git a/library/goptions.ml b/library/goptions.ml index c111113ca..9b4fc9985 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -24,7 +24,6 @@ type option_value = (** Summary of an option status *) type option_state = { - opt_sync : bool; opt_depr : bool; opt_name : string; opt_value : option_value; @@ -62,7 +61,6 @@ module MakeTable = val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end) -> struct type option_mark = @@ -77,13 +75,9 @@ module MakeTable = module MySet = Set.Make (struct type t = A.t let compare = A.compare end) - let t = - if A.synchronous - then Summary.ref MySet.empty ~name:nick - else ref MySet.empty + let t = Summary.ref MySet.empty ~name:nick let (add_option,remove_option) = - if A.synchronous then let cache_options (_,(f,p)) = match f with | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in @@ -103,9 +97,6 @@ module MakeTable = in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) - else - ((fun c -> t := MySet.add c !t), - (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = Feedback.msg_notice @@ -141,7 +132,6 @@ sig val key : option_name val title : string val member_message : string -> bool -> std_ppcmds - val synchronous : bool end module StringConvert = functor (A : StringConvertArg) -> @@ -156,7 +146,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeStringTable = @@ -176,7 +165,6 @@ sig val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end module RefConvert = functor (A : RefConvertArg) -> @@ -191,7 +179,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeRefTable = @@ -201,7 +188,6 @@ module MakeRefTable = (* 2- Flags. *) type 'a option_sig = { - optsync : bool; optdepr : bool; optname : string; optkey : option_name; @@ -247,11 +233,10 @@ let get_locality = function | None -> OptDefault let declare_option cast uncast append ?(preprocess = fun x -> x) - { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in let change = - if sync then let _ = Summary.declare_summary (nickname key) { Summary.freeze_function = (fun _ -> read ()); Summary.unfreeze_function = write; @@ -275,18 +260,12 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) discharge_function = discharge_options; classify_function = classify_options } in (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) - else - (fun _ m v -> - let v = preprocess v in - match m with - | OptSet -> write v - | OptAppend -> write (append (read ()) v)) in let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab; + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab; write type 'a write_function = 'a -> unit @@ -325,7 +304,7 @@ let set_option_value locality check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (_,read,write,append)) -> + | Some (name, depr, (read,write,append)) -> write (get_locality locality) (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -366,7 +345,7 @@ let set_string_option_append_value_gen locality key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (_,read,write,append)) -> + | Some (name, depr, (read,write,append)) -> append (get_locality locality) (check_string_value v (read ())) let set_int_option_value = set_int_option_value_gen None @@ -387,7 +366,7 @@ let msg_option_value (name,v) = (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (_,read,_,_)) = get_option key in + let (name, depr, (read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -397,9 +376,8 @@ let print_option_value key = let get_tables () = let tables = !value_tab in - let fold key (name, depr, (sync,read,_,_)) accu = + let fold key (name, depr, (read,_,_)) accu = let state = { - opt_sync = sync; opt_name = name; opt_depr = depr; opt_value = read (); @@ -416,15 +394,8 @@ let print_tables () = in str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_)) p -> - if sync then p ++ print_option key name (read ()) depr - else p) - !value_tab (mt ()) ++ - str "Asynchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_)) p -> - if sync then p - else p ++ print_option key name (read ()) depr) + (fun key (name, depr, (read,_,_)) p -> + p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right diff --git a/library/goptions.mli b/library/goptions.mli index 3b3651f39..f612c4e36 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -40,8 +40,8 @@ Unset Tata Tutu Titi. Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) - The created table/option may be declared synchronous or not - (synchronous = consistent with the resetting commands) *) + All options are synchronized with the document. +*) open Pp open Libnames @@ -65,7 +65,6 @@ module MakeStringTable : val key : option_name val title : string val member_message : string -> bool -> std_ppcmds - val synchronous : bool end) -> sig val active : string -> bool @@ -93,7 +92,6 @@ module MakeRefTable : val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end) -> sig val active : A.t -> bool @@ -108,8 +106,6 @@ module MakeRefTable : used when printing the option value (command "Print Toto Titi." *) type 'a option_sig = { - optsync : bool; - (** whether the option is synchronous w.r.t to the section/module system. *) optdepr : bool; (** whether the option is DEPRECATED *) optname : string; @@ -120,8 +116,6 @@ type 'a option_sig = { optwrite : 'a -> unit } -(** When an option is declared synchronous ([optsync] is [true]), the output is - a synchronous write function. Otherwise it is [optwrite] *) (** The [preprocess] function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value. *) @@ -177,7 +171,6 @@ type option_value = (** Summary of an option status *) type option_state = { - opt_sync : bool; opt_depr : bool; opt_name : string; opt_value : option_value; -- cgit v1.2.3