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:
try (definition_tactic foo := bla; fail)
will leave the definition around. abstract
is somewhat buggy due to thisabstract
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 instanceLemma 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: Oct 13 2024 at 01:02 UTC