RanDair Scott Porter (Jan 29 2021 at 16:43): RanDair Scott Porter (Jan 29 2021 at 16:43):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.
Emilio Jesús Gallego Arias (Jan 29 2021 at 18:00):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?
RanDair Scott Porter (Jan 29 2021 at 19:35):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.
Talia Ringer (Jan 29 2021 at 19:41):@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
Enrico Tassi (Jan 30 2021 at 08:59):This plan reminds me of http://helm.cs.unibo.it/procedural/
Emilio Jesús Gallego Arias (Jan 31 2021 at 21:47):@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 .
Talia Ringer (Feb 01 2021 at 03:44):Interesting, why does run_tactic expect Global.env?
Gaëtan Gilbert (Feb 01 2021 at 09:16):I don't know why tclENV isn't Global.env but it isn't so run_tactic needs to be provided an env
Emilio Jesús Gallego Arias (Feb 02 2021 at 23:35):Talia Ringer said:
Interesting, why does
run_tacticexpectGlobal.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.
Emilio Jesús Gallego Arias (Feb 02 2021 at 23:45):Having to use enter is however not very flexible, due to the return type, but that could be fixed in several ways.
Emilio Jesús Gallego Arias (Feb 02 2021 at 23:45):And maybe it is time we fix it.
Last updated: Dec 05 2023 at 12:01 UTC