Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add customizable variables to configure which part of a goal the goal buffer will focus on #654

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

cipher1024
Copy link

By setting coq-prefer-top-of-conclusion to t, we get Proof General to focus on the conclusion of the first goal after displaying the list of goals of a proof. The conclusion is defined as whatever is preceded by =======. In some cases, it can be useful to mark a different part of the conclusion as the main point of interest. This PR allows the customization of that marker as well as the ability to choose where to place that marker in the window when focusing on it.

@Matafou
Copy link
Contributor

Matafou commented May 25, 2022

Thanks. This is a good idea. I will have a look at your patch asap. Can you explain how the user does specify the part of the goal to follow? Is it by selecting some peace of it?

@cipher1024
Copy link
Author

Here is how I use it to improve my workflow with the Iris Proof Mode (IPM). Iris encodes different kinds of assumptions in the conclusion of a goal so the conclusion you're actually interested in is not quite the same as the one you're interested in with the Iris Proof Mode.

I put these lines in my init.el file. It makes the experience with IPM nicer but non-IPM goals are also displayed nicely with these settings:

(setq coq-prefer-top-of-conclusion t) ;; this is already part of the package

(setq coq-goal-conclusion-marker ;; this will get proof general to find the last point of interest in a goal
      (rx (or "========"
              "--------------------------------------∗"
              "--------------------------------------□")))

(setq coq-center-after-focus 'middle) ;; this will get proof general to put the conclusion marker in the middle of the *goals* window. Other options are 'top and 'bottom

@cipher1024
Copy link
Author

So the short answer to your question is: by writing a regexp that will match a piece of the goal

@cipher1024
Copy link
Author

One more note: I made sure that the default has the same behavior as the current version.

@erikmd
Copy link
Member

erikmd commented Sep 13, 2022

@Matafou @cipher1024 what is the status of this PR?

@Matafou
Copy link
Contributor

Matafou commented Sep 14, 2022

Looks good and useful to me. Thanks again!
@cipher1024 can you add a line to the CHANGES file, rebase into one commit please?
We need to add a documentation on these variables (coq-prefer-top-of-conclusion itself isn't).

Comment on lines +126 to 130
:type '(radio
(const :tag "move conclusion marker to the top of the window" top)
(const :tag "move conclusion marker to the middle of the window" middle)
(const :tag "move conclusion marker to the bottom of the window" bottom)))

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For better user configuration should we merge this preference with coq-prefer-top-of-conclusion?
Currently if this one is nil then we show the end of the conclusion (of the first goal). Something like:

    (const :tag "focus on the end of the conclusion even if it hides the conclusion marker" tail)

coq-prefer-top-of-conclusioncould be left for compatibilty.
@cipher1024 what do you think?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants