Stream: MetaCoq

Topic: running TemplateMonad inside a tactic


view this post on Zulip joomy (Jan 14 2023 at 12:07):

When running a TemplateMonad program from Ltac using the run_template_program tactic, is there a particular reason commands like tmVariable, tmDefinition, tmAxiom are not allowed? Currently this results in an error like You can not use ... in a tactic..

I realize these commands all change the environment, but is this disallowed only because it is too powerful, or does it actually break something?

view this post on Zulip Yannick Forster (Jan 14 2023 at 12:08):

It's impossible to change the global env from ltac unfortunately

view this post on Zulip Yannick Forster (Jan 14 2023 at 12:08):

I was thinking about changing the behavior of tmDefinition to be essentially a pose, but never got around implementing it

view this post on Zulip joomy (Jan 14 2023 at 12:12):

I see. I thought since Variable, Definition etc. (as vernacular commands) are allowed in proof mode, this could be allowed too. That's unfortunate, thanks for the explanation.

view this post on Zulip Yannick Forster (Jan 14 2023 at 12:22):

I think you need to enable a setting to allow them, no? In any case they are discouraged for production code, so I see the reasoning why ltac should not have global effects

view this post on Zulip Gaëtan Gilbert (Jan 14 2023 at 12:43):

Yannick Forster said:

It's impossible to change the global env from ltac unfortunately

that's not strictly true, there's abstract

joomy said:

I see. I thought since Variable, Definition etc. (as vernacular commands) are allowed in proof mode, this could be allowed too. That's unfortunate, thanks for the explanation.

something can be allowed as a command without being possible as a tactic
AFAIK there are 2 issues with allowing tactics to have the effect of arbitrary commands:

Lemma foo : True.
Proof.
  Axiom bla : match 0 with 0 => unit | x => unit end. (* warn unused-pattern-matching-variable *)
  exact I.
Qed. (* warn again *)

Last updated: May 19 2024 at 18:02 UTC