a defines an Ltac1 tactic and
b overrides it, is
Import a supposed to shadow
b's side effect? I wouldn't expect that, but it seems what I see (in Coq 8.13.2)... which makes using
::= much more fragile than it needs to be.
From D.Dot.hkdot Require Import a b. Goal False. Proof. Fail foo. Import a. (* Was already required *) foo. Import b. Fail foo.
Ltac foo := idtac "a".
From D.Dot.hkdot Require Import a. Ltac foo ::= idtac "b"; fail.
(this, in fact, seems related to https://github.com/coq/coq/issues/12206 and https://gitter.im/coq/coq?at=5ea971003d58de7a38e31365).
I added to the issue that
I now think the fix should go in the other direction: ::= should work only on Require and never on Import, because ::= is about rebinding a dynamically bound symbol, not about shadowing.
the point of
:= (if there is one) is to violate static binding and affect existing occurrences; I'd naively expect
Import's only "destructive" effect to be shadowing, but shadowing shouldn't reset a mutable variable?
alternatively, since this is unlikely to change due to backward compat, it'd be interesting to discuss what the semantics _should_ be.
Last updated: Oct 03 2023 at 02:34 UTC