Stream: Coq devs & plugin devs

Topic: Proofview.tclENV: when is it useful?


view this post on Zulip Janno (Aug 19 2021 at 18:40):

I just fixed a bug in a custom OCaml tactic that used Constr_matching functions. I had naively used tclENV to get an environment to feed to is_matching and that worked fine when primitive projections were disabled. However, the parameter of the projection relies on a section variable and with primitive projections enabled retyping failed with <record value> depends on the variable <section variable> which is not declared in the context . The bug is fixed by using Goal.enter_one and then Goal.env. But now I wonder: if tclENV doesn't even contain section variables, what is it good for? Should I ever use it for anything? The docs say it returns the "global" environment of the proof but I don't know what that means.

view this post on Zulip Gaëtan Gilbert (Aug 19 2021 at 19:04):

I think it has section variables though

view this post on Zulip Janno (Aug 19 2021 at 19:12):

I've been doing some more debugging and the result depends on how exactly the tactic is called. I can only reproduce the problem when using something like all: tactic. or ; [tactic|..]. Not when I call the tactic on its own on a single goal. There might be extra complications because the OCaml code is called from an Ltac2 tactic that already uses Control.enter to focus on a single goal.

view this post on Zulip Gaëtan Gilbert (Aug 19 2021 at 19:31):

don't see how any of those would matter

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:21):

The invariants is that tclENV is the "prefix" of the environment needed, and local goal environments are just this env where the named context can be replace.

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:22):

If you ask why it's a state and not a reader, it can change due to calls to abstract and the like.

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2021 at 16:23):

As a end user you shouldn't have to use tclENV I believe (but it's still needed for the internals of the proof engine, since you don't want to call the imperative Global.env function)


Last updated: Oct 16 2021 at 02:03 UTC