Add features: use goal count information printed at top of goals buffer in modeline, clear the goal window when proof is skipped (abort, admitted...). #755
Conversation
|
The change is nice. A few remarks here and there. 2 questions:
|
Thanks for your answer.
|
| @@ -18,7 +18,7 @@ | |||
| (setq coq-prog-name "unavailable-program") | |||
|
|
|||
| ;; ensure coq-prog-name cannot be found | |||
| (should (not (locate-file coq-prog-name exec-path))) | |||
There was a problem hiding this comment.
Could you explain this change?
There was a problem hiding this comment.
As I mentioned earlier, I wanted to appropriate this project by making sure my building was fine, so I broke a simple test first. But now I think my PR should be a bit cleaner.
etc/testsuite/#simple.v#
Outdated
There was a problem hiding this comment.
What is this file for?
etc/testsuite/.#simple.v
Outdated
There was a problem hiding this comment.
What is this file for?
The error is related to this PR, it was introduced in the first commit f6a425f. |
|
The PR should first be cleaned up (useless files, then reduced to one commit imho. |
I thank you all for taking the time for reviewing my PR (which is my first ever, that's why it was a bit messy, and I apologize for that). I think it is a bit cleaner, and I welcome any advice on how to improve it before it can be merged (if it's needed of course). |
generic/pg-goals.el
Outdated
| @@ -79,6 +79,63 @@ May enable proof-by-pointing or similar features. | |||
| ;; | |||
| ;; Goals buffer processing | |||
| ;; | |||
|
|
|||
| ;; update *goals* buffer modeline | |||
| (defun coq-parse-goals-info (goals-output) | |||
There was a problem hiding this comment.
PG is a generic interface for proof assistants, see https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Introducing-Proof-General, which does not only support Coq, see https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants . Assistant specific code should therefore go into the assistant specific directory.
There was a problem hiding this comment.
@Matafou Can you recomment where this code should be added in the coq subdir?
generic/pg-goals.el
Outdated
| (funcall pg-insert-text-function string)) | ||
| (when (not (string-equal string "")) | ||
| (funcall pg-insert-text-function string) | ||
| (coq-parse-goals-info string)) |
There was a problem hiding this comment.
I am pretty sure that calling a Coq specific function here will break any other proof assistant. Please add the mode line update to a suitable hook, such that it is only called when PG is instanciated for Coq.
generic/proof-script.el
Outdated
| @@ -1486,6 +1486,7 @@ Besides stuff that is not yet documented here, this function | |||
| and sections. | |||
| - enters some commands and their spans in some database (with for | |||
| me unknown purpose)" | |||
| (reset-goals-modeline) ; Erase goal buffer when a proof is closed | |||
There was a problem hiding this comment.
The comment here is inconsistent with your documentation of reset-goals-modeline.
There was a problem hiding this comment.
Maybe this call does not break other assistants, but it should not be called for all assistants. Please check if you can find a suitable hook to add this call.
|
I have the impression that the "clear goal window" part that is mentioned in the title of this PR is not present in the patch anymore. Can you confirm this? (I also suspect that this aspect did not work in your previous version, at least not for Admitted, as I don't remember that you have changed that the |
|
My opinion is that everything should be customizable, but I don't always apply it to myself. I think the current goal counter (on the scripting buffer) is not customizable either. |
|
Hi everyone, I modified my feature for Coq-only implementation, moved my functions to the coq subdir, and adapted the modeline update only when PG is instantiated for Coq. My goal here is to offer the possibility to users to custom the modeline as mentioned in #605. I thank you all again for this precise review of my code. |
|
I have been thinking about this PR a bit more and I think we should not merge it.
See Line 3121 in 734bcdb (add-hook 'proof-shell-handle-delayed-output-hook #'coq-update-minor-mode-alist)Feel free to submit a new PR adapting this part of the code.
Remark on the code: Testing the name of the prover in the generic code is not the way PG is supposed to be configured. Specific provers should not appear in the generic part. If noone object I shll close this PR soon. |
In response to issues #605 and #168, I moved the information of current goal to the goals buffer modeline (to save some space and visibility basically), and cleared the goals buffer when encountering skip proof tactics like Abort. or Admitted. in Coq.