Stream: Coq devs & plugin devs

Topic: Warning for deprecated subclass instances


view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 16:45):

In current master we get a somewhat weird set of warnings when using the deprecated :> syntax for subclass instances after the merge of https://github.com/coq/coq/pull/16230.

view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 16:46):

for instance,

Class Foo := {}.

Class Bar := {
  foo :> Foo;
}.

results in

The default value for field instance locality is currently "global", but
is scheduled to change in a future release. For the time being, adding
field instances without specifying an explicit locality attribute is
therefore deprecated. It is recommended to use "export" whenever
possible. Use the attributes #[local], #[global] and #[export] depending
on your choice. For example: "Class foo := { #[export] field :: bar }."
[deprecated-field-instance-without-locality,deprecated]
A coercion will be introduced instead of an instance in future versions
when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use
'#[global] Existing Instance field.' for compatibility with Coq < 8.17).
Beware that the default locality for '::' is #[export], as opposed to
#[global] for ':>' currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For example: "Class foo
:= { #[global] field :: bar }." [future-coercion-class-field,records]

view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 16:46):

that is, we get two warnings when I would have only expected one (the second one)

view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 16:47):

@Pierre Roux @Ali Caglayan is this the intended behaviour?

view this post on Zulip Pierre-Marie Pédrot (Jul 18 2022 at 16:48):

in particular the first warning is not emitted when using the :: syntax (and it has an export semantics, kind of contradicting the warning)

view this post on Zulip Pierre Roux (Jul 18 2022 at 16:50):

Indeed, I should probably remove the first warning, it's now pretty redundant. Will open a PR.

view this post on Zulip Pierre Roux (Jul 20 2022 at 09:38):

@Pierre-Marie Pédrot here it is: https://github.com/coq/coq/pull/16331


Last updated: Feb 05 2023 at 20:03 UTC