Karl Palmskog (Nov 26 2022 at 14:46): 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]
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
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
Paolo Giarrusso (Nov 26 2022 at 15:08):And I understand the confusion:
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.
Karl Palmskog (Nov 26 2022 at 15:09):my expectation is the following for all warnings:
Here, instead of 1, I get:
1'. if I don't ignore it, my project errors out
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)
Paolo Giarrusso (Nov 26 2022 at 15:10):I think the current setting is -w +deprecated-instance-without-locality?
Paolo Giarrusso (Nov 26 2022 at 15:10):Which means "error by default", and the + option has existed for quite a while
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.
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?
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
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
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"
Paolo Giarrusso (Nov 26 2022 at 15:15):I get that.
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.
Paolo Giarrusso (Nov 26 2022 at 15:18):OTOH, I think there are indeed problematic scenarios
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.
Karl Palmskog (Nov 26 2022 at 15:20):I'm also fine with making it a regular warning that doesn't error
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.
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)
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
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
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.
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-localityand 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.
Paolo Giarrusso (Nov 27 2022 at 17:28):I guess you plan to change defaults in 8.18? Hopefully all these defaults at once?
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).
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
Karl Palmskog (Nov 27 2022 at 18:22):but why weren't other deprecations handled this way then? Why is this one special?
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: Sep 09 2024 at 05:02 UTC