Stream: Coq devs & plugin devs

Topic: Plugin enter proof mode?


view this post on Zulip Ende Jin (May 06 2022 at 15:11):

Hi new Zulip user here :) I am not sure if this is the correct format and place to ask questions but here I am :)
I am wondering how to let my customized plugin command "start a new proof/goal"?

My current way of developing plugins is to translate my command into vernac_expr and invoke Vernacinterp.interp. This works fine and satisfies most of my needs, but when I use the same idea to translate my command into VernacStartTheoremProof (which should correspond to using Theorem command), the interp function finished successfully but my VsCoq interface didn't enter the proof mode (as far as it looks like, I am not sure if there is any display error by VsCoq; I also tried to input Qed but it does error with the message "No Focused Proof....")

Looking forward to any suggestions! I guess there are some plugins that can enter the proof mode but I don't know where to find them :) Great Thanks!

view this post on Zulip Gaëtan Gilbert (May 06 2022 at 15:15):

you need to classify as vtstartproof in your mlg

view this post on Zulip Gaëtan Gilbert (May 06 2022 at 15:27):

something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90

view this post on Zulip Gaëtan Gilbert (May 06 2022 at 15:27):

(the CLASSIFIED BY part)

view this post on Zulip Ende Jin (May 06 2022 at 15:39):

Gaëtan Gilbert said:

something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90

Thanks for the help! I will try to transplant this example into mine :)


Last updated: Feb 06 2023 at 18:03 UTC