Pierre Rousselin (Aug 18 2023 at 14:42): Pierre Rousselin (Aug 18 2023 at 14:42):As a not very serious summer topic, what do you think of the "No more goals." message when a proof is finished (at least in CoqIde and JsCoq)?
Having no more goals sounds depressing. Vim's Coqtail gives the more glorious"All goals completed."
Paolo Giarrusso (Aug 18 2023 at 16:49):You have a point, sending a patch for that can't hurt. If you file an issue, it should be hopefully be labeled "good first issue" to help people pick it up.
Pierre Rousselin (Aug 20 2023 at 09:21):Ok, I might do it for practice.
Pierre Rousselin (Aug 23 2023 at 08:50):PR submitted (but I feel bad to trigger so many tests just for this :cry:).
Karl Palmskog (Aug 23 2023 at 09:22):this kind of change might be more useful to propose in VsCoq2, Coq-LSP or ProofGeneral, given that CoqIDE is seemingly on its way out (https://github.com/coq-community/manifesto/issues/145)
Pierre Courtieu (Aug 23 2023 at 11:56):Careful with the « cannot hurt » quicky . I think Proofgeneral does not rely on this message. But I am not sure.
Karl Palmskog (Aug 23 2023 at 11:57):right, would be good if Coq gives some neutral canonical signal everybody agrees on, which can then be customized to an appropriate message at editor/protocol level... (as opposed to discussion about specific wording in Coq itself)
Pierre-Marie Pédrot (Aug 23 2023 at 12:01):That's what the protocol is about. The oddball here is ProofGeneral, which relies on scraping the output of coqtop.
Maxime Dénès (Aug 24 2023 at 06:09):@Pierre Rousselin Feel free to submit a patch for VsCoq. It should be easy and there it cannot hurt ;)
Last updated: Oct 13 2024 at 01:02 UTC