Debugger proof context display should show all goals in the same format used outside the debugger

[jfehrle]

Users expect to see a consistent and complete display of the proof context whether in the debugger or not.
Currently they differ. That severely impacts the usefulness of the debugger. For example:

Set Ltac Debug.
Ltac x := split; idtac.
Goal False /\ False.
x.
(*  at a breakpoint on "idtac":
Goal:
  
  ============================
   False *)

versus

Goal False /\ False.
split.
(* 2 goals
______________________________________(1/2)
False
______________________________________(2/2)
False *)

[jfehrle]

I tried several experiments to get the information needed to print with Printer.print_and_diff without success:

• Calling Vernacstate.Declare.give_me_the_proof () - does not include changes made in the Ltac tactic
• Calling Proofview.Goal.goals - returns only 1 goal after the split while in the debugger, so not the right thing, either

@ejgallego @ppedrot or others:
How can I fetch this information while I'm in the debugger? Is there already a simple way to do this or do we need to create a new routine for it? Surely this information is available somewhere.

[ejgallego]

Calling Vernacstate.Declare.give_me_the_proof () - does not include changes made in the Ltac tactic

Indeed, as this is a deprecated API and should not be used, instead you need to get a Proof.t object, which can be accessed from many objects, depending where you are.

[herbelin]

Users expect to see a consistent and complete display of the proof context whether in the debugger or not. Currently they differ.

The following shows that the two goals are printed:

Set Ltac Debug.
Ltac x := split; assert True.
Goal False /\ True.
x.
(*
TcDebug (1) > 

Goal:
  ============================
   False

Goal:
  ============================
   True

*)

But they are printed after entering. One would need to display them before they are dispatched (maybe using Proofview.proofview, I'm not so familiar with the API).

[ppedrot]

Users expect to see a consistent and complete display of the proof context whether in the debugger or not

As you put it, this does not make sense. Goal printing is handled by the UI, so it's not the responsibility of coqtop to print goals in the debugger as they ought to look in the user interface. At best you can send them through the protocol and let the UI handle that.

[jfehrle]

@herbelin Very helpful, thanks. Looks like you tried this in coqtop, which gives different output than in CoqIDE. I'll investigate why it's different. I didn't expect that at all!

@ejgallego instead you need to get a Proof.t object, which can be accessed from many objects, depending where you are.

As an initial experiment, I'd like to access this information from Tactic_debug.db_pr_goal, which already accesses a Proofview.Goal.t. I didn't see a way to get a Proof.t object (the one in proof.ml) from it. I also looked at Tacinterp.val_interp, which enters the debugger code through Tactic_debug.debug_prompt but didn't see anything there that seemed helpful, either.

Eventually I'd like to access it from a new/modified XML protocol message in idetop.ml with an option to select which subgoal to show fully so that that information can be seen in the debugger.
Also I'd like to eventually get proof diffs to work in the debugger. Proof diffs requires a Proof.t.

@ppedrot The main problem here is that the goal display in CoqIDE is incomplete. Currently the goal is formatted and sent to the debugger as a tagged Pp.t. That should be changed so CoqIDE uses the Goal XML call to fetch the info instead.

[SkySkimmer]

at

coq/plugins/ltac/tactic_debug.ml

Line 332 in d926f04

Proofview.Goal.enter begin fun gl ->

we do enter which runs the body once for each goal. I guess this means coqide sees a message for each goal and only displays the last received.
If instead you do

  let open Proofview in
  let open Notations in
  Goal.goals >>= fun gl ->
  Monad.List.map (fun x -> x) gl >>= fun gl ->

the last gl is the list of goals (type Proofview.Goal.t list, you should be able to use that to adapt the printing.

[jfehrle]

@SkySkimmer Thanks, that is sufficient to show the goals, though I'd like to end up with a Proof.t so that debug and non-debug contexts can be handled consistently.

Idetop.goals calls Stm.finish but I suspected that I couldn't call that when I'm at a breakpoint (nested invocation of Stm routines and I expect we don't want to create new stateids for tactic calls inside Ltac tactics).

[ejgallego]

I didn't see a way to get a Proof.t object

Aha, you are a bit lower than that layer, then you need to access the Proofview.proofview object from the monad, something like what @SkySkimmer proposes is OK, but you can likely use a direct way.

[SkySkimmer]

Indeed there's no Proof.t while executing tactics.
We don't expose any way to get Proofview.proofview either but it doesn't have any more information than goals so it shouldn't matter.

[ppedrot]

Don't use Proof.t, it lives one layer higher and contains data the proof engine shouldn't know about. Instead, just expose the functions taking the minimal amount of data.

[ejgallego]

Actually Proof.t is just an artifact these days, and may go hopefully away at some point.

[jfehrle]

OK. I want to tweak Idetop.goals, which calls export_pre_goals, which requires Proof.{ sigma; goals; stack }.
If I use @SkySkimmer's code to get all the goals as Proofview.Goal.t:

• Where do I get stack from (needed to compute the background goals)?
• Each Goal.t has its own sigma but Proof.t seems to have one that's shared across all its goals. Sigma is the same across all the Goal.ts?
• Proof.goals is just the concatenation of the Goal.self values?

[ppedrot]

Where do I get stack from (needed to compute the background goals)?

You don't really have access to this from the proof engine, and it's a feature. You can observe future goals and the shelf, but it's not exactly the same thing.

Sigma is the same across all the Goal.ts?

The general answer is yes, if you don't call any effectful tactics in the meantime. Depending on the exact function you call to get the goal this can be ensured statically.

Proof.goals is just the concatenation of the Goal.self values?

It should be.

[jfehrle]

it's a feature

meaning intentional?

Since Ltac doesn't support the { ... } focus/unfocus constructs, I expect stack from Vernacstate.Declare.give_me_the_proof () should remain valid while in the debugger.
(digression: Do users need or would they want to have a similar construct in
Ltac, if only for consistency?)

The general answer is yes, if you don't call any effectful tactics in the meantime. Depending on the exact function you call to get the goal this can be ensured statically.

Perhaps you would be more specific so I'm more likely to get it right the first time? If I get it wrong the first time I would probably ask you for elaboration anyway.