Stream: Coq users

Topic: Import undoes `Ltac foo ::=` side effects


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 28 2021 at 20:30):

(this, in fact, seems related to https://github.com/coq/coq/issues/12206 and https://gitter.im/coq/coq?at=5ea971003d58de7a38e31365).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC