Stream: Coq users

Topic: Superglobal effects and namespaces


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

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

Is this an unexpected bug or an expected behavior?

view this post on Zulip Paolo Giarrusso (Oct 05 2021 at 14:03):

Also mentioned in https://github.com/coq/ceps/pull/25#issuecomment-934444714 for future reference.

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

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2021 at 14:06):

both semantics make sense imo

view this post on Zulip Pierre-Marie Pédrot (Oct 05 2021 at 14:06):

(there is the same issue with Arguments / head constants, etc.)

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 05 2021 at 16:44):

FWIW filed https://github.com/coq/coq/issues/14988 to refer to it.


Last updated: Feb 06 2023 at 12:04 UTC