Paolo Giarrusso (Oct 05 2021 at 13:25): Paolo Giarrusso (Oct 05 2021 at 13:25):It seems that #[global] Bind Scope isn't superglobal, which is unfortunate in combination with namespacey-modules (here using Include since it makes the problem more annoying):
Module Type N_alias. (* In fact, imagine a newtype wrapper*)
Definition t := N.
#[global] Bind Scope N_scope with t.
End N_alias.
Module virt_addr.
Include N_alias.
End virt_addr.
#[global] Bind Scope N_scope with virt_addr.t. (* Seems I need this too, or the next line fails! *)
Definition test (a b : virt_addr.t) : virt_addr.t := a + b.
More in general, I suspect real namespaces should not hide #[export] effects https://github.com/coq/ceps/pull/25...
Paolo Giarrusso (Oct 05 2021 at 13:25):Is this an unexpected bug or an expected behavior?
Paolo Giarrusso (Oct 05 2021 at 14:03):Also mentioned in https://github.com/coq/ceps/pull/25#issuecomment-934444714 for future reference.
Pierre-Marie Pédrot (Oct 05 2021 at 14:06):Yes, there is a perennial confusion between superglobal / export semantics for stuff that is attached to kernel definitions
Pierre-Marie Pédrot (Oct 05 2021 at 14:06):both semantics make sense imo
Pierre-Marie Pédrot (Oct 05 2021 at 14:06):(there is the same issue with Arguments / head constants, etc.)
Paolo Giarrusso (Oct 05 2021 at 14:22):with Namespace virt_addr. we could get an even better semantics: declarations are visible iff containing _modules_ are imported, _not_ counting namespaces.
Paolo Giarrusso (Oct 05 2021 at 14:24):But for now, having both #[global] and #[export] work for everything uniformly would be great, even if I understand that’s sadly tons of work (due to unnecessary complexity?)
Gaëtan Gilbert (Oct 05 2021 at 14:27):backwards compat more than complexity I think
although it's also kinda hard to find what's using global for what meaning, that could count as complexity
Paolo Giarrusso (Oct 05 2021 at 16:44):FWIW filed https://github.com/coq/coq/issues/14988 to refer to it.
Last updated: Oct 13 2024 at 01:02 UTC