Stream: Coq devs & plugin devs

Topic: Vernacstate.Declare.get_current_proof_name

Nicolas Magaud (Jan 11 2021 at 14:35):

In some old ML-written tactics, I use the function Vernacstate.Declare.get_current_proof_name to retrieve the name of a proof and then create some auxiliary names using the retrieved name as a string. Starting in Coq 8.12.2, this function seems to be deprecated. Is there an alternative around to achieve the same behavior ? Thanks in advance.

Emilio Jesús Gallego Arias (Jan 11 2021 at 19:23):

Hi @Nicolas Magaud , proof state is now threaded functionally [instead of kept in a global reference], so you need to pass it along your plugin.

Usual entry point is in the tactic / vernacular extension point, example:

VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
  { fun ~pstate -> Declare.Proof.compact pstate }

Emilio Jesús Gallego Arias (Jan 11 2021 at 19:25):

That will allow the tactic code to modify the proof state

Emilio Jesús Gallego Arias (Jan 11 2021 at 19:25):

Supported qualifiers are:

let understand_state = function
  | "close_proof" -> "VtCloseProof", false
  | "open_proof" -> "VtOpenProof", true
  | "proof" -> "VtModifyProof", false
  | "proof_opt_query" -> "VtReadProofOpt", false
  | "proof_query" -> "VtReadProof", false
  | "read_program" -> "VtReadProgram", false
  | "program" -> "VtModifyProgram", false
  | "declare_program" -> "VtDeclareProgram", false
  | "program_interactive" -> "VtOpenProofProgram", false
  | s -> fatal ("unsupported state specifier: " ^ s)

Emilio Jesús Gallego Arias (Jan 11 2021 at 19:25):

Not sure how well documented coqpp is tho

Karl Palmskog (Jan 11 2021 at 19:28):

@Théo Zimmermann I think this topic belongs in Coq devs

Gaëtan Gilbert (Jan 11 2021 at 19:49):

since it's tactics you can just do as abstract: Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (name, poly) ->

Notification Bot (Jan 11 2021 at 20:46):

This topic was moved here from #Miscellaneous > Vernacstate.Declare.get_current_proof_name by Théo Zimmermann

Last updated: Oct 13 2024 at 01:02 UTC