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?

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

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

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.

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

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:

- backtrack: tactic backtrack does not know how to revert effects on the global state, so eg
`try (definition_tactic foo := bla; fail)`

will leave the definition around.`abstract`

is somewhat buggy due to this - async proofs / qed opacity: if the tactics could have uncontrolled effects we wouldn't be able to skip them for qed proofs and so async proofs and -vos would be broken.
`abstract`

is treated specially for this, in the code the system for it is called "kernel side effects" or "private constants". Commands which may have global effects (basically everything that's not a tactic and not a query like Check) actually get run twice to deal with this: once for the proof, then after the proof is complete the global state gets reverted to before the proof, those commands get run again, finally the constant is added to the kernel. So for instance

```
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