Ltac Debugger: goals not updated when one steps through tactics defined in different files.

[MSoegtropIMC]

Description of the problem

When stepping though a tactic in the Ltac debugger, the goal display is not updated when one steps through a tactic defined in a different file - even if one returns to the original file.

Consider these two files in the same folder:

File Ltac_Debugger_Display.v

Require Import a.
Set Ltac Debug.

Ltac b := idtac "b1"; a; idtac "b2".

Goal 2 = 1+1.
b.

File a.v

Ltac a := idtac "a1"; simpl; idtac "a2".

Now proceed as follows:

• coqc a.v
• coqide Ltac_Debugger_Display.v &
• advance proof state to after the Goal
• position the cursor at the first idtac in b and set a breakpoint with F8
• advance over the invocation of b - the debugger stops at the breakpoint
• now single step with F10 until execution returns to file Ltac_Debugger_Display.v

This leaves one in a state where "a2" is printed in the Messages window, but the goal is still:

Goal:
  
  ============================
   (2 = 1 + 1)

which is clearly wrong since the idtac "a2" comes after the simpl.

In my experience, whenever one steps through a tactic in a separate file, the goal is not updated any more until the tactic execution ends.

As far as I remember (not 100% but pretty sure) this did work fine in the debugger preview.

Coq Version

The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.13.1
(__coq-platform.2022.04.0~8.15~2022.04)

@jfehrle : FYI.

[jfehrle]

This is a display issue. The updated goal is shown in the Goal panel of Ltac_Debugger_Display after the simpl and before the idtac "a2". Note that the call stack appears only when Ltac_Debugger_Display is visible. That's why the doc recommends putting the goal and debug panels of the top script in separate windows for now.

The underlying issue is that CoqIDE allows multiple active debug Coq sessions, so how does CoqIDE know which debug session goals the user wants to see from moment to moment? CoqIDE could be stopped in a.v in multiple sessions. The compromise I chose for now was to only show the goals in the top level script's goal panel. Longer term, it's a GUI design issue. The solution is likely restricting CoqIDE to a single debugger session at a time.

Please try it with multiple windows.

[MSoegtropIMC]

Thanks, I can indeed see the update, but this is all rather weird:

• I do see the goal in the goal panel of the file from which I started debugging, but only when the debug cursor is on idtac "a2". When I do another F10, so that the debug cursor is on idtac "b2", I see again the goal as it was before simpl`
• I am not sure what you mean by "Goal panel of Ltac_Debugger_Display" - for me the Ltac_Debugger_Display doesn't have a Goal panel (just Call Stack and Variables). Or do you mean the Goal panel for the buffer with which the Ltac_Debugger_Display is attached?
• The call stack looks weird:

b:4, Ltac_Debugger_Display
:7, Ltac_Debugger_Display

what is the Ltac_Debugger_Display in the Call Stack supposed to mean?

I see the issue with multiple debug sessions. I would recommend to either not allow this - if this is really needed one can still launch two CoqIDE instances - or to have some way to select the active debug session or the default display (a buffer can also have a goal / proof state without debugging). If it makes things simpler I really would not allow multiple sessions. It doesn't make a lot of sense to make the usual case of a single session less useful in favor of a rather exotic multiple debug sessions use case. I don't know any other IDE which allows multiple debug sessions.

[jfehrle]

I do see the goal in the goal panel of the file from which I started debugging, but only when the debug cursor is on idtac "a2". When I do another F10, so that the debug cursor is on idtac "b2", I see again the goal as it was before simpl

Ignore the goal panel in the secondary file. Only look at the goal panel of the top level script. The doc says:

For multi-file debugging, we suggest detaching the Messages, Proof Context and Debugger panels so they are in separate windows. To do so, click on the arrow icon next to "Messages", select "Windows / Detach Proof" from the menu and click on "DETACH" in the Debugger panel. Note that the Debugger panel is initially attached to the Script panel of the toplevel script.

Or do you mean the Goal panel for the buffer with which the Ltac_Debugger_Display is attached?

Exactly. Windows/Detach Proof from the menu to make it a separate window.

what is the Ltac_Debugger_Display in the Call Stack supposed to mean?

It is the module name, derived from the filename Ltac_Debugger_Display. The doc says:

Stack frames normally show the name of tactic being executed, the line number and the last component of the filename without the .v suffix. The directory part of the module name is shown when the frame is not in the toplevel script file. For example, make_rewriter:387, AllTactics (Rewriter.Rewriter) refers to the file with the module name Rewriter.Rewriter.AllTactics.

but this is all rather weird ... I see the issue with multiple debug sessions. I would recommend to either not allow this

Yeah. I thought people could deal with some weirdness for a while, which I discussed in the doc. I think it's a fairly big change, best not to change everything at once--more likely I will break things and it would makes the reviews take even longer. I plan to add a number of new features such as Ltac2 before I address this. After that, I'd also like to make some general improvements bug fixes to CoqIDE after that. That may take a year :-(.

[jfehrle]

But thinking about this a bit more, I think you're right that there is a regression. I'll look at it more tomorrow. You should see the updated goal here:

[MSoegtropIMC]

@jfehrle : detaching the debugger panel doesn't work for me, because when I do so each press of F10 changes focus to the detached debugger panel, so that for stepping I have to do F10, click main window, F10, click main window, ...

[jfehrle]

As far as I remember (not 100% but pretty sure) this did work fine in the debugger preview.

I see the same behavior in V8.15.0. What Coq revision number should I try for the debugger preview?

Edit: never mind.

[jfehrle]

detaching the debugger panel doesn't work for me, because when I do so each press of F10 changes focus to the detached debugger panel, so that for stepping I have to do F10, click main window, F10, click main window, ...

You can press F10 and other debugger function keys while the focus is in the debugger panel or the Messages, Goal or Script panel of the top-level or top of stack buffer for the code you're running.

[MSoegtropIMC]

You can press F10 and other debugger function keys while the focus is in the debugger panel or the Messages, Goal or Script panel of the top-level or top of stack buffer for the code you're running.

This does not work for me (Coq Platform 8.15~2022.04.0, macOS, from sources). When I press F10 the debug panel gets focussed and further presses of F10 are ignored.

[jfehrle]

I just tried that platform version on native Windows. It works as I said except that function keys are not forwarded from the top level goals panel.

If you click on the header of the debug panel or the top-level proof/messages panels before you press F10, does that make any difference? That would be very surprising.

It may be that focus doesn't work the same across platforms either because platform-specific code in GTK or differences in the window system it interfaces to. There probably aren't many multi-window applications so this behavior may have gotten proper attention for that case. It may be that an additional grab_focus is needed. It would be difficult for me to figure this out since I don't have a macos system.

#15912 should avoid the issue. Perhaps you can apply it locally or at least in the next release of Coq Platform.

[MSoegtropIMC]

I think it depends on the exact order in which panels are detached - I found that sometimes it does work - sometimes not.

If I follow this procedure, it does not work:

• Set breakpoint
• Advance proof context with array keys until breakpoint is hit
• detach debugger window using detach button
• detach proof view window via menu "Windows/Detach Proof"
• step with F10 -> stuck after first F10
• neither explicitly clicking on the title of the detached debugger nor of the detached proof view helps - only clicking the title of main CoqIDE Window makes F10 work again, and focus us lost again after each F10

If I detach all 3 message Windows (with the arrow detach buttons) and the proof view (via the menu), then start the debugger and then detach the debug Window F10 does work.

I could reproduce both behaviors 2 times.

[jfehrle]

Glad you found a workaround.