Display all focused goals

lephe commented 2 years ago

I'm back again, with more quality-of-life improvements (or at least I hope!).

This PR shows more information about the goals (video below). This is basically all straight out of CoqIDE:

All focused goals are shown and numbered (also since Sublime has Unicode support I figure a full-width separator line is prettier). This is fairly important to me, because eauto or inversion often generate subgoals that I don't expect, and seeing them right away shows that I've gone in the wrong direction.
Background goals, shelved goals (including evars) and admitted goals are counted separately in the "Goals:" line, which makes it easier to keep track of goals. Especially with evars the current goal counter is mostly useless.
A show_goals setting (with values "primary" or "current", the proposed default being "current") allows reverting to the single-goal display, which I assume can be useful in inline mode to not blow up the size of the phantom.

https://user-images.githubusercontent.com/33732078/145720762-96dba1cf-d158-4435-95e2-e1882ed47168.mp4

This is all an extension of format_response() since the protocol part (specifically the Goal request) is already set up.

I'm not sure if the sublime module was deliberately not loaded in coq.py; if so we could add a function parameter, but it would need to travel pretty far down the call chain from CoqPlugin.py to format_response().

lephe commented 2 years ago

I just saw that I could improve this in several ways; there are issues with multi-character bullets, opening braces, and "No more goals" being displayed when finishing a bullet point. I'll keep working on this; any feedback is welcome though!

lephe commented 2 years ago

I added the structured response type as you suggested. It's named CoqGoalResponse (rather than CoqResponse) because the response structure differs widely between commands, and all of this goal classification really only applies to the Goal command. For the same reason, send() still returns an XML generator, however CoqBot.current_goal() does the wrapping.

There is also slightly more structure than you might expect, since goals are classified into categories, and the hypotheses are separated from the goal string itself. (The method to separate depends on the protocol version, it didn't feel right to leave it at the formatting level in CoqPlugin.py.)

I also updated the setting to be either "primary" (only one goal) or "focused" (all currently-focused goals), which is at least an improvement.

I still need to move the format_response() function to CoqPlugin.py and clean up some behaviors. I'm not sure the way I programmed it really matches the way you envisioned it though, so feedback is still welcome.

Calvin-L commented 2 years ago

The changes look great to me 🥂

I still need to move the format_response() function to CoqPlugin.py and clean up some behaviors.

Cool! Let me know when you're ready to have this merged.

lephe commented 2 years ago

Excellent, thank you so much! :D

I realized that background goals are not represented by a single pair, but by a stack of pairs ("before current" goals, "after current" goals). This is relevant when you have nested bullet points, since after the last bullet point of the nested list there are no more focused goals and no more background goals at the current level, but there might be background goals at the lower level. I updated the CoqGoalResponse API to handle background goals separately, as it seemed better to keep the return type of the goals() method consistent rather than to involve a stack specifically when querying background goals.

I moved string generation to a new section of CoqPlugin.py, which removed the requirement for the sublime module to be loaded in coq.py, as discussed.

Because of the CoqGoalResponse being a structured object now, it can't be directly combined with the feedback messages of the previous command. I changed the show_goal() method to now accept two parameters, text:str and goal:CoqGoalResponse, instead of one. Depending on the use case either or both can be set to produce text in the proof display.

Speaking of feedback messages, I noticed the usual messages like f is defined weren't displayed. This is controlled by a "verbose" bool in the Add command. I enabled it in order to test the feedback messages; I think it'd be nice to support them as they can also contain some important information when loading modules. Is there a reason to turn them off (ie. should I add an option) or can we just leave them on?

In the same vein, I suspect messages like "This subproof is complete, but there are unfocused goals" might be annoying in the inline view. I can add an option if that's a concern.

Finally, here is the full test case I used (in addition to real scripts):

Goal True -> (1=1/\2=2) /\ (3=3 /\ (4=4 /\ 5=5) /\ 6=6) /\ 7=7.
  intros.
  split; split.
  Focus 3.
    split; [ | split ].
    Focus 2.
      - split.
      all: admit.
    all: reflexivity.
  all: reflexivity.
Admitted.

Definition x := 2.

Goal True -> (1=1 /\ 2=2 /\ 3=3) /\ 4=4 /\ 5=5.
  intros.
  split; [|split].
  - split; [|split].
    * reflexivity.
    * reflexivity.
    * reflexivity.
  - auto.
  - auto.
Qed.

Goal forall (x y z: nat), x = y -> y = z -> x = z.
  intros.
  etransitivity.
  all: eassumption.
Qed.

Some things like focusing with 2:{ aren't tested here because of some parsing issues (to be addresses later!). :)

Pending any new issues/details this is ready to merge. Sorry for the pretty big diff!

Calvin-L commented 2 years ago

(Sorry for the long wait on this; I've been on vacation for a while!)

Calvin-L / sublime-coq-plugin

Display all focused goals #5