Stream: Coq users

Topic: Overriding notations


view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 13:09):

EDIT: this problem might require more circumstances to trigger.

I'd like to override an existing notation for an existing scope, but I'm not sure that's possible and this might have gotten worse in 8.11.

AFAICT, it's not enough to do

(* Overrider module *)
Require Import notation_source.
(* Override notation *)

because clients of Overrider might still get the original notation, unless they import Overrider last.

Are the side effects of the original module re-executed at every transitive import? That might make sense if somebody imports notation_source directly, but I see notation_source winning even in source files that never mention it.

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 13:12):

I'm not sure I see relevant docs here:
https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Require-Import
https://coq.inria.fr/refman/language/core/modules.html#coq:cmd.Import
https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Notation

view this post on Zulip Gaëtan Gilbert (Oct 13 2021 at 13:19):

are you using Export somewhere?

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 14:24):

probably yes — there are ~307 occurrences of Export in this codebase

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 14:38):

uuuh, there is a chain of Exports leading to notation_source, which could explain this on its own :-|.
I guess that's what you meant @Gaëtan Gilbert ? Thanks a lot!

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 14:38):

I'll look into it

view this post on Zulip Gaëtan Gilbert (Oct 13 2021 at 14:39):

yup, there is no transitive import without export

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 14:40):

and crucially, no superglobal effects are involved


Last updated: Jan 28 2023 at 06:30 UTC