From ee92d3246c6bb76140f14a9a829e955612c0e2f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 25 Nov 2024 18:21:32 +0100 Subject: [PATCH] Remove bugged option MetaCoq Template Monad Debug. It causes https://github.com/coq/vscoq/issues/892 because `optwrite` is not supposed to be able to add persistent objects (libobject) to Coq's state but `set_option_value` does add one. It's also bugged as `set_option_value ~stage:Interp (fun _ v -> v) key i` sets the option to its current value not a new value. In other words `Set MetaCoq Template Monad Debug.` has no effect but its existence causes bugs. Since nobody complained about it not working it's not worth fixing it instead of deleting it (also I'm not sure it can be fixed with the currently available APIs). --- template-coq/src/tm_util.ml | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml index aef445e47..4aa575c2a 100644 --- a/template-coq/src/tm_util.ml +++ b/template-coq/src/tm_util.ml @@ -26,33 +26,6 @@ end = struct | None -> match declare_int_option_and_ref ~key ~value:0 () with { get } -> get - let set_template_monad_verbose = - let open Goptions in - match get_option_value key with - | Some get -> - let set = fun i -> - set_option_value ~stage:Interp (fun _ v -> v) key i - in set - | None -> assert false - - let set_template_monad_debug d = - set_template_monad_verbose (if d then 1 else 0) - let get_template_monad_debug () = - if get_template_monad_verbose () > 0 then true else false - - let _ = - let open Goptions in - let key = ["MetaCoq"; "Template"; "Monad"; "Debug"] in - match get_option_value key with - | Some get -> () - | None -> - declare_bool_option - { optdepr = None; - optstage = Interp; - optkey = key; - optread = get_template_monad_debug; - optwrite = set_template_monad_debug; } - let ppdebug lvl pp = if get_template_monad_verbose () > lvl then Feedback.msg_debug (pp ()) end