RFC: @[unstable] attribute

Stream: lean4

[Mario Carneiro]

This isn't yet at the point of a real RFC, I'm still thinking through the consequences, but when designing APIs for esp. Std and Init I think it comes up sometimes that we have some API which we expect to change in the near future, and would like to limit the impact on downstream code while also making our jobs easier when it comes time to bump, by explicitly marking the API as "unstable".

As far as concrete behavior, it would behave mostly the same as @[deprecated]: any use of the unstable declaration would produce a warning that you can disable with set_option linter.unstable false. It just wouldn't come with any replacement instructions.

Lean is of course quite unstable at many levels, so there will certainly be things changing which aren't marked as @[unstable]. But not all instability is created equal and this might at least help better set expectations and document progress on a feature.

[Mario Carneiro]

I'd also be interested to hear if people can think of applications of this in mathlib

[Floris van Doorn]

First thoughts: if we use this in Mathlib, users of unstable code will use it anyway, since in math there is often not an easy alternative. I guess they get a little heads up "this code is going to break at some point", but I'm not convinced that is worth the (small) extra maintenance burden of marking things as unstable.

[Mario Carneiro]

yes, I don't really expect it to stop people from using it. But I do think it helps shift the burden a little bit (i.e. "don't come complaining to me when it breaks"), and sometimes it is possible to hold off on using it until the better version comes

[Mario Carneiro]

I also don't think we should necessarily apply it religiously. At least in mathlib, I don't think we are very good estimators of when something will be changed in the future in most cases

[Mario Carneiro]

so it would be restricted mainly to things where there is an active project on its way to replace it

[Mario Carneiro]

that is worth the (small) extra maintenance burden of marking things as unstable.

I would say the maintenance burden of marking a definition as unstable is almost negative: it's a way to signal to everyone downstream "hey I'm working here" with a little less force than private. However I think there is some burden associated with using unstable definitions since you have to turn off the linter, and then remember to remove those set_options later

[Floris van Doorn]

Mario Carneiro said:

At least in mathlib, I don't think we are very good estimators of when something will be changed in the future in most cases

"Is it a leaf file or almost a leaf file" might be a decent estimator...? Of course, we refactor things in core Mathlib files quite frequently as well, but I think we've been pretty good recently at deprecating those changes (and we cannot mark everything as unstable :-) )
I'm not against having or trying it though.