Fixup for v8.17.1, fix Debug/Break for Ltac2

plugins/ltac/tactic_debug.ml

@@ -55,7 +55,6 @@ module Comm = struct
      initialization is unconditionally done for example in coqc.
      Improving this would require some tweaks in tacinterp which
      are out of scope for the current refactoring. *)
-  let init = DebugCommon.init
   open DebugHook.Intf
   open DebugHook.Answer
 
@@ -199,12 +198,9 @@ let () =
 
 (* (Re-)initialize debugger. is_tac controls whether to set the action *)
 let db_initialize is_tac =
-  if Sys.os_type = "Unix" then
-    Sys.set_signal Sys.sigusr1 (Sys.Signal_handle
-      (fun _ -> DebugCommon.set_break true));
   let open Proofview.NonLogical in
   let x = (skip:=0) >> (skipped:=0) >> (idtac_breakpt:=None) in
-  if is_tac then make Comm.init >> x else x
+  if is_tac then make DebugCommon.init >> x else x
 
 (* Prints the run counter *)
 let print_run_ctr print =

plugins/ltac2/g_ltac2.mlg

@@ -134,9 +134,11 @@ let rec dump_expr ?(indent=0) e =
   | CTacApp (f, args) -> printloc "CTacApp" e;
     dump_expr ~indent f
 (*| CTacSyn of (raw_patexpr * raw_tacexpr) list * KerName.t*)
+(*
   | CTacSyn (el, kn) -> printloc "CTacSyn" e;
     Printf.eprintf "%s> %s\n%!" (String.make indent ' ') (Names.KerName.to_string kn);
     List.iter (fun i -> let (_, e) = i in dump_expr ~indent e) el
+*)
   | CTacLet (isrec, lc, e) -> printloc "CTacLet" e;
     dump_expr ~indent e;  (* rhs only *)
   | CTacCnv _ -> printloc "CTacCnv" e

plugins/ltac2/tac2intern.ml

@@ -1036,6 +1036,7 @@ let to_simple_case env ?loc (e,t) pl =
     let (map, def) = intern_branch KNmap.empty pl in
     GTacWth { opn_match = e; opn_branch = map; opn_default = def }
 
+[@@@ocaml.warning "-32"]
 let rec dump_expr2 ?(indent=0) e =
   let printloc loc =
     let loc = match loc with
@@ -1069,6 +1070,7 @@ let rec dump_expr2 ?(indent=0) e =
   | GTacExt _ -> print "GTacExt"
   | GTacPrm  _ -> print "GTacPrm"
   | GTacAls  _ -> print "GTacAls"
+[@@@ocaml.warning "+32"]
 
 (*
 let rec dump_expr ?(indent=0) e =
@@ -1205,6 +1207,7 @@ let rec intern_rec env {loc;v=e} = match e with
   let ids = List.fold_left fold Id.Set.empty el in
   if is_rec then intern_let_rec env loc ids el e
   else intern_let env loc ids el e
+(*
 | CTacSyn (el, kn) ->
   let body = Tac2env.interp_notation kn in
   let rv = intern_rec env @@ CAst.make ?loc @@ CTacLet(false, el, body) in
@@ -1216,6 +1219,7 @@ let rec intern_rec env {loc;v=e} = match e with
   let (e2, _) = rv in
   if false then dump_expr2 e2;
   rv
+*)
 | CTacCnv (e, tc) ->
   let (e, t) = intern_rec env e in
   let tc = intern_type env tc in
@@ -1598,9 +1602,11 @@ let rec globalize ids ({loc;v=er} as e) = match er with
   in
   let bnd = List.map map bnd in
   CAst.make ?loc @@ CTacLet (isrec, bnd, e)
+(*
 | CTacSyn (el, kn) ->
   let body = Tac2env.interp_notation kn in
   globalize ids @@ CAst.make ?loc @@ CTacLet(false, el, body)
+*)
 | CTacCnv (e, t) ->
   let e = globalize ids e in
   CAst.make ?loc @@ CTacCnv (e, t)
@@ -1880,9 +1886,11 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
   let bnd' = List.Smart.map map bnd in
   let e' = subst_rawexpr subst e in
   if bnd' == bnd && e' == e then t else CAst.make ?loc @@ CTacLet (isrec, bnd', e')
+(*
 | CTacSyn (el, kn) ->
   let body = Tac2env.interp_notation kn in
   subst_rawexpr subst @@ CAst.make ?loc @@ CTacLet(false, el, body)
+*)
 | CTacCnv (e, c) ->
   let e' = subst_rawexpr subst e in
   let c' = subst_rawtype subst c in

vernac/debugCommon.ml

@@ -75,7 +75,7 @@ let set_history_size n =
 let () =
   let open Goptions in
   declare_int_option
-    { optstage = Summary.Stage.Interp;
+    { (* optstage = Summary.Stage.Interp; Not in v8.17.1 *)
       optdepr  = false;
       optkey   = ["Ltac";"Debug";"History"];
       optread  = (fun () -> Some !history_buf_size);
@@ -162,8 +162,6 @@ let check_bpt dirpath offset =
 let break = ref false
 (* causes the debugger to stop at the next step *)
 
-let set_break b = break := b
-
 let print_loc desc loc =
   let open Loc in
   match loc with
@@ -372,6 +370,9 @@ let wrap = Proofview.NonLogical.make
    Improving this would require some tweaks in tacinterp which
    are out of scope for the current refactoring. *)
 let init () =
+  if Sys.os_type = "Unix" then
+    Sys.set_signal Sys.sigusr1 (Sys.Signal_handle
+      (fun _ -> break := true));
   stack_chunks := [];
   prev_chunks := [];
   top_chunk := empty_chunk;
@@ -384,7 +385,7 @@ let init () =
     if Intf.(intf.isTerminal) then
       action := Action.StepIn
     else begin
-      set_break false;
+      break := false;
       breakpoints := BPSet.empty;
       (hook ()).Intf.submit_answer (Answer.Init);
       while

vernac/debugCommon.mli

@@ -8,8 +8,6 @@ val breakpoint_stop : Loc.t option -> bool
 
 val stepping_stop : unit -> bool
 
-val set_break : bool -> unit
-
 val action : DebugHook.Action.t ref
 
 (* Comm module stuff *)