Paolo Giarrusso (Oct 13 2021 at 13:09): 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.
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
Gaëtan Gilbert (Oct 13 2021 at 13:19):are you using Export somewhere?
Paolo Giarrusso (Oct 13 2021 at 14:24):probably yes — there are ~307 occurrences of Export in this codebase
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!
Paolo Giarrusso (Oct 13 2021 at 14:38):I'll look into it
Gaëtan Gilbert (Oct 13 2021 at 14:39):yup, there is no transitive import without export
Paolo Giarrusso (Oct 13 2021 at 14:40):and crucially, no superglobal effects are involved
Last updated: Oct 05 2023 at 02:01 UTC