Deprecation warnings?

Stream: lean4

[Mario Carneiro]

A lot of lean 4 changes are simplifications of the language to remove superfluous choices and increase regularity. The recent removal of rw e in favor of rw [e] is an instance of this. (Or at least that's my reconstructed rationale, the relevant commit doesn't say anything about why.) However, people have habits and when it's not in the grammar you can end up with some really bad error messages. What do people think about having syntax extensions that mimic old patterns but throw up a warning instead? I just implemented this for variables:

variables {X : Type} (a : X)
---------  'variables' has been replaced by 'variable' in lean 4

example : a = a := rfl -- works

[Mario Carneiro]

the alternative here is just to accept variables without complaint, since we clearly have the ability to parse it and make sense of it

[Sebastien Gouezel]

I'd rather go for more regularity, so having variables raise a warning looks good to me. As to whether it should work (as variable) or not, I don't really have an opinion, I would probably prefer if it doesn't work to force people to get used to the new syntax.

[Sebastian Ullrich]

Where do you want to put these deprecations? I don't think anyone would complain if it was in mathlib (heck, that's half the work necessary for automatic syntactic porting anyway) or a "Lean 4 for Lean 3 users" library, but I don't see it happening in core. We wouldn't be nearly as far as we are without the "tabula rasa" approach.

[Mario Carneiro]

Definitely mathlib

[Mario Carneiro]

although there are some deprecations I'm considering that are incompatible with (current) lean 4, for example getting rid of universes and making universe accept more than one ident

[Mario Carneiro]

I don't know how problematic it is to teach people an incompatible variant of the language

[Mario Carneiro]

Is it possible to make core tactics inaccessible? For example if I want rw to work differently I can make a notation with higher priority, but if my rw fails to accept some syntax that core rw accepts, then users will be able to call the other one

[Sebastien Gouezel]

What do you mean? Would it be nontrivial to change Lean 3 community to let it accept variable and universe for several variables, and make a global search and replace in mathlib?

[Mario Carneiro]

I think this would be quite doable. The question is more about the sociological aspect: if people use mathlib then universe u v will work and universes u v will error or give a warning, but if you don't import mathlib then universes u v will work and universe u v will be a parse error

[Mario Carneiro]

so that might get confusing if you work both with and without mathlib

[Sebastien Gouezel]

When you say "use mathlib", do you mean "use Lean 3.0 community"?

[Mario Carneiro]

I mean use mathlib for lean 4

[Mario Carneiro]

in a hypothetical future where we're all on lean 4

[Sebastien Gouezel]

My opinion is that mathlib for Lean 4 should use the same syntax as core (universe and variable) and throw a warning on universes and variables. To help the transition, we could change Lean 3 community to have the same behavior.

[Mario Carneiro]

For lean 3.0 community there is no problem, because we have enough control to just upstream the syntax change and update mathlib

[Mario Carneiro]

My opinion is that mathlib for Lean 4 should use the same syntax as core (universe and variable)

The problem is that this sentence has a false presupposition: in lean 4 core right now it is universes and variable

[Mario Carneiro]

and I think that's dumb inconsistent

[Mario Carneiro]

it's probably just an oversight but it makes a good example for discussion purposes

[Patrick Massot]

What about avoiding using the word "dumb"?

[Mario Carneiro]

My guess is that for this particular example it won't be too hard to convince the core devs to upstream this change, but I'm sure there are plenty of examples where mathlib wants to change some defaults from core and upstreaming is not an option for whatever reason

[Mario Carneiro]

Since lean 4 is so configurable we can pretty well go to town on changing default behavior, but that comes at the cost of fracturing the language to some extent, and I'm not sure yet how we should weigh such decisions

[Patrick Massot]

I'm pretty sure we don't want to recreate the "traditional Coq vs SSReflect" dichotomy.

[Mario Carneiro]

ironic that you mention that because I was just thinking we can do ssreflect in lean so much better now

[Kevin Buzzard]

What is this dichotomy?

[Patrick Massot]

One of the reasons I started using Lean is because when I tried to learn Coq all Coq documentation was assuming traditional Coq (and a CS degree and software verification target) and all SSReflect documentation was assuming knowledge of traditional Coq, and the combination was really hard to read.

[Patrick Massot]

Of course we'll have mathlib tactics, but we should really try to be compatible with core Lean 4.

[Mac]

Mario Carneiro said:

The problem is that this sentence has a false presupposition: in lean 4 core right now it is universes and variable

Mario Carneiro said:

and I think that's inconsistent

I am really curious as to why this inconsistency exists. I think it would be a wonderful question for Lean 4 team (i.e., @Sebastian Ullrich, since he checks here the most) .

[Sebastian Ullrich]

Because we missed universes when removing variables

[Mac]

Sebastian Ullrich said:

Because we missed universes when removing variables

I assume this change would make universe variadic? (because, at present, it only accepts one identifier)

[Sebastian Ullrich]

Yes, same as with variable

[François G. Dorais]

@Sebastian Ullrich Any ETA on the universes -> universe change?

[Sebastian Ullrich]

No, there are no ETAs. We are overwhelmed with feature requests (most by us), so the only way we can operate is to focus on one topic at a time instead of constantly switching between them.

[Sebastian Ullrich]

And yes, this one seems trivial (but some turn out not to be that after all). So I'll stop talking about it longer than it might take to fix it.

[Mario Carneiro]

As long as universes -> universe is on the eventual agenda, I guess it would be fine to pre-implement in mathlib4

[Julian Berman]

I gave this a shot, since I'd also noticed it awhile back. PR: https://github.com/leanprover/lean4/pull/458

[Patrick Massot]

I fear Sebastian and Leo would need more time to review your PR than doing the fix themselves, so my bet is they will close this PR. I hope you've learned interesting things while working on it.

[Julian Berman]

Yeah. I suspected the same thing while making it, and won't be offended if that happens.

[Patrick Massot]

Especially since Sebastian wrote a pretty clear message in this thread.