Ltac2: importing a mutable definition does not undo its mutations

[SkySkimmer]

cf #10556

The previous behaviour can be gotten by doing eg

(* auxiliary definition to avoid repeating it, if it's a simple expression it can also be inlined *)
Ltac2 original_def := ...

Ltac2 mutable the_def := original_def.

Ltac2 Set the_def := original_def.

instead of Ltac2 mutable the_def := ....

Also add test for Ltac2 mutable definitions vs Import/Export.

This exposes some complex behaviour around repeated imports when using Set as.

[SkySkimmer]

@coqbot run full ci

[rlepigre]

Are we sure this is the right semantics? It seems to me that seeing toplevel commands like Ltac2 Set as things running only at "module initialization" (by analogy to OCaml's module initialization for example) would be more intuitive. In other words, maybe the effect should take place as soon as one Imports a module that performs the effect directly, or a module that Exports the module doing the effect (and so on), and also, ensure that the effect can only be run once, on the first Import that should trigger it, and subsequent Imports are no-ops. CC @Janno.

[SkySkimmer]

Ocaml module initialization would be Require time not Import.

[rlepigre]

Ocaml module initialization would be Require time not Import.

That's why I put it in quotes, I agree the analogy is not perfect.

[SkySkimmer]

@coqbot run full ci

[ppedrot]

@SkySkimmer refman not happy

[ppedrot]

@coqbot run full ci

[ppedrot]

I have no strong opinion about the expected semantics of Ltac2 late binding w.r.t. require / import. The new behaviour is more expressive than the previous one, and it's reasonable to me. @rlepigre @Janno are you fine with the current semantics?

[rlepigre]

I have no strong opinion about the expected semantics of Ltac2 late binding w.r.t. require / import. The new behaviour is more expressive than the previous one, and it's reasonable to me. @rlepigre @Janno are you fine with the current semantics?

I don't have a very strong opinion either. What would be most intuitive to me would be to perform the update at Require time, to make this similar to what you'd get in OCaml. But is that even be an option?

[SkySkimmer]

That's what ltac1 does.

[ppedrot]

Let's merge then @coqbot merge now

[coqbot-app[bot]]

@ppedrot: You cannot merge this PR because:

• There is no kind: label.

[ppedrot]

@coqbot merge now