The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Hello coq-club;

(1) It appears that VSCoq2, the "flagship" Coq extension for VSCode, is implementing a real-time tactic update mode of operation. This means that instead of the workflow [write a tactic > execute written tactic], the environment finds the current tactic your cursor is at, and also brings the proof state to that point.

I am wondering if people find this convenient, and what the best practices to deal with it are?

Personally, I prefer manually changing the proof state. This is because I prefer to go back and forth on my tactics to see how the proof state has evolved. Sometimes, I look at the current proof state, and refactor older tactics. Sometimes, navigating the proof via some [Next Tactic] hotkey is also nice, instead of having to place my cursor at the exact location needed.

(2) Another feature I noticed that VSCoq2 is implementing is this: When you have a tactic that produces multiple goals (e.g, split), each of the goals are put in some "accordion" UI-element. While the "accordion" looks visually nice, the issue is that all-but-the-first accordion is collapsed by default. This means that you have to click uncollapse to see all the other goals. For this reason, I am unsure if this is helpful as it is.

I suspect that the collapsed accordion presentation would be helpful if it worked the following way: Currently, when you focus on any subgoal using - or {, the rest of the goals disappear until you unfocus. It would be nice if the collapsed accordion options would keep the "sister" goals that are immediately outside the current focus. (I understand that this may be hard to implement given how coqtop works.)

(3) If I close the tab in VSCode with the proof state by accident, how do I reopen it without having to restart the IDE?

If anyone would like to share their thoughts and best practices for using the newer version of VSCoq, I would be very interested.

Thanks!

--Agnishom