Paolo Giarrusso (Dec 28 2021 at 20:29): Paolo Giarrusso (Dec 28 2021 at 20:29):If 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.
c.v"
From D.Dot.hkdot Require Import a b.
Goal False.
Proof.
Fail foo.
Import a. (* Was already required *)
foo.
Import b.
Fail foo.
a.v:
Ltac foo := idtac "a".
b.v:
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).
Paolo Giarrusso (Dec 28 2021 at 20:42):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.
Paolo Giarrusso (Dec 28 2021 at 20:46):the point of ::= over := (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?
Paolo Giarrusso (Dec 28 2021 at 20:47):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