Stream: Coq users

Topic: No more goals.


view this post on Zulip 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."

view this post on Zulip 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.

view this post on Zulip Pierre Rousselin (Aug 20 2023 at 09:21):

Ok, I might do it for practice.

view this post on Zulip Pierre Rousselin (Aug 23 2023 at 08:50):

PR submitted (but I feel bad to trigger so many tests just for this :cry:).

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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: Jun 13 2024 at 21:01 UTC