I'm using Proof.run_tactic
in coq 8.8. From that I can get the new evar_map
, but if the tactic updates the proof context I don't seem to have a way of getting the new env
. It seems it'd be possible if I could access the proof
record but that's hidden by the module.
Umm, Coq 8.8 is too old , in particular with regards to this part of the API ; more generally, why are you calling that function, what are you trying to do concretely?
We're decompiling proof terms into Ltac scripts, which involves running tactics on subgoals to see if they would succeed. We keep track of the context, but haven't found a way to retrieve the context after the tactic is executed.
@Emilio Jesús Gallego Arias are you saying that this part of the API isn't accessible at all in 8.8, or that you don't know how to help us because we are on 8.8? If the former, we can invest some time into updating to the latest Coq, but we will need help. We've been delaying forever because it is difficult without much support, and we have ~15000 LOC in Ocaml across our plugin suite
This plan reminds me of http://helm.cs.unibo.it/procedural/
@Talia Ringer I was referring more to the fact that we have quite updated all that API in recent versions, so advice for 8.8 may significantly differ from advice for 8.13/8.14; moreover handling of proof envs is unfortunately fragile at best. Note that you can access the env in the monad just by building a tactic of type env Proofview.tactic
(using bind + tclEnv) and calling run_tactic
on it, however this env will be in general different from the one used by run_tactic in the next call as it is usually meant to be Global.env
.
Interesting, why does run_tactic
expect Global.env
?
I don't know why tclENV isn't Global.env but it isn't so run_tactic needs to be provided an env
Talia Ringer said:
Interesting, why does
run_tactic
expectGlobal.env
?
Actually how the envs are working in this part of the system is the kind of darkest black magic you could expect from research software ; I don't understand it, and it is likely broken [@Pierre-Marie Pédrot please tell me I'm wrong] On the good side I think cleaning this part up is a huge priority but we have been lagging behind.
I guess if you provide us with a bit more context, we may be able to help more; note that the answer to the original question is likely "just add >> tlcENV ()
to the tactic you are running, if you want the "global tactic env", or use enter
+ the Goal.t
API to get a per goal local proof env.
Having to use enter
is however not very flexible, due to the return type, but that could be fixed in several ways.
And maybe it is time we fix it.
Last updated: Dec 05 2023 at 12:01 UTC