Stream: Coq devs & plugin devs

Topic: deprecated-instance-without-locality errors


view this post on Zulip Karl Palmskog (Nov 26 2022 at 14:46):

Here's something I think I've never seen after a decade or so of Coq: ignoring a warning (deprecated-instance-without-locality) actually makes a project build (on Coq master) rather than error out. Is this really intended? The usual behavior (to me) is that if something is an error, one shouldn't be able to "fix" it by ignoring a deprecation.

File "./file.v", line 129, characters 0-84:
Error: The default value for instance locality is currently "local" in a
...
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]

view this post on Zulip Gaëtan Gilbert (Nov 26 2022 at 15:07):

I don't understand the question tbh
it is normal that ignoring a deprecation makes things work now but fail in a future version
that's what deprecated means

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:08):

It sounds like this is still a warning but Coq master enabled "fail by default" for this warning

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:08):

And I understand the confusion:

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:09):

I had heard this was becoming an error, which would imply "-w -deprecated-instance-without-locality" would not have an effect.

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:09):

my expectation is the following for all warnings:

  1. if I don't ignore it, my projects build but display the warning during compilation
  2. if I ignore it, my projects build and do not display the warning

Here, instead of 1, I get:
1'. if I don't ignore it, my project errors out

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:10):

but "-w -deprecated-instance-without-locality" does have an effect here in latest master: it prevents there being an error (and a warning)

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:10):

I think the current setting is -w +deprecated-instance-without-locality?

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:10):

Which means "error by default", and the + option has existed for quite a while

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:11):

that would be consistent with what I'm seeing, and I don't think that has ever been done for any deprecation before.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:11):

I don't recall Coq using it out of the box, which might be what's new to you (and others), and maybe a problem?

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:14):

I think it may be a problem in 8.17 and beyond in the sense of: many people will find their projects unexpectedly erroring on a warning, and not understand that a simple warning ignore will make the project unbroken

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:15):

But the intention is to give an error, and having a forced error would have the same behavior

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:15):

if you have a "full error", then you shouldn't be able to escape it by inserting "-w -deprecated-instance-without-locality"

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:15):

I get that.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:16):

But it seems like you're complaining about this hidden extra option for authors and you want it removed altogether.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:18):

OTOH, I think there are indeed problematic scenarios

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:19):

I think it's a really weird compromise (inconsistent with what has come before) to use -w +<deprecation> for something that should be a regular error.

view this post on Zulip Karl Palmskog (Nov 26 2022 at 15:20):

I'm also fine with making it a regular warning that doesn't error

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:24):

this was already a regular warning... but I agree there's at least one question: this was deprecated because it'll be removed, then readded with a different meaning. But with -w -deprecated-instance-without-locality, you might miss that and have the behavior change with essentially no notice.

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:25):

(you did get a warning a few years back but you added -w -deprecated-instance-without-locality and forgot)

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:29):

would there be hard problems with a regular error? Is there some problem with fiat-crypto-legacy (cc @Jason Gross )? It seems that was not the initial motivation? https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Make.20hint.20locality.20warning.20an.20error/near/281664899

view this post on Zulip Paolo Giarrusso (Nov 26 2022 at 15:33):

okay, Jason's plan seems to rely on -w -deprecated-instance-without-locality in some step; https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Make.20hint.20locality.20warning.20an.20error/near/282035834

view this post on Zulip Théo Zimmermann (Nov 27 2022 at 17:06):

Karl Palmskog said:

I think it's a really weird compromise (inconsistent with what has come before) to use -w +<deprecation> for something that should be a regular error.

Why should it be a regular error? The goal is just to force users to be aware of this deprecation warning and give some thoughts to fixing it. I don't see how leaving a way out for users who do not want to fix the deprecation just yet is making things worse.

view this post on Zulip Théo Zimmermann (Nov 27 2022 at 17:06):

Paolo Giarrusso said:

(you did get a warning a few years back but you added -w -deprecated-instance-without-locality and forgot)

I indeed think that's the only issue with this strategy. But people who manage their warnings explicitly at least are aware that they exist.

view this post on Zulip Paolo Giarrusso (Nov 27 2022 at 17:28):

I guess you plan to change defaults in 8.18? Hopefully all these defaults at once?

view this post on Zulip Théo Zimmermann (Nov 27 2022 at 18:01):

Yes, that's the goal AFAICT. But I don't see any PR opened or issue with a blocker label targeting 8.18+rc1 (cc @Pierre-Marie Pédrot).

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2022 at 18:14):

that's https://github.com/coq/coq/pull/16258, but it's still marked as a draft

view this post on Zulip Karl Palmskog (Nov 27 2022 at 18:22):

but why weren't other deprecations handled this way then? Why is this one special?

view this post on Zulip Théo Zimmermann (Nov 27 2022 at 18:23):

Because instead of a removal, the thing changes its behavior, so it's easy to go unnoticed and lead to surprising behavior.


Last updated: Feb 01 2023 at 16:03 UTC