Skip to content

Commit

Permalink
Remove bugged option MetaCoq Template Monad Debug.
Browse files Browse the repository at this point in the history
It causes coq/vscoq#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).
  • Loading branch information
SkySkimmer committed Nov 25, 2024
1 parent 65aa111 commit ee92d32
Showing 1 changed file with 0 additions and 27 deletions.
27 changes: 0 additions & 27 deletions template-coq/src/tm_util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit ee92d32

Please sign in to comment.