deprecated tag

Stream: lean4

[Patrick Massot]

I'm curious about the deprecated tag. I thought that Lean 4 was still at a stage where deprecated stuff just get removed without warning. Do we have any documentation about that tag?

[Leonardo de Moura]

@Patrick Massot I added a new bullet to the release notes: https://github.com/leanprover/lean4/blob/master/RELEASES.md

I added [deprecated] yesterday. I added it to make the transition to https://github.com/leanprover/lean4/issues/1346 smooth.
Last week, @Mario Carneiro suggested we make methods such as

def Lean.Meta.getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do

more "discoverable" by making them dot-notation frieldly. That is, we would now use

def  Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do

We think this is a good modification. We also want to avoid having duplicate APIs, but we also want to avoid breaking all meta-programs written by the community last week. The [deprecated] attribute is quite convenient for making the transition smooth. Whenever users use a deprecated function, they get a warning message saying how to "fix" their code. They may also decide to ignore the message for now.
I think this is important because it makes sure packages such as Aesop and Quote4 (that were demoed last week) can still be used without modifications.

[Mario Carneiro]

I think it is fine to have aliases in some places without deprecation; dot-notation syntax in particular is one thing that we use the alias command for in mathlib even though we generally avoid aliases. Even though I would probably use MVarId.getDecl more often, I don't think we need to say that getMVarDecl is "wrong"; the only annoying bit is having to duplicate the docstring but a command like alias could do that automatically to prevent divergence.

[Mario Carneiro]

(For example, le_trans is aliased to has_le.le.trans but it would be pretty weird/nitpicky to require use of the latter)

[Leonardo de Moura]

@Mario Carneiro All functions marked as [deprecated] are dead code in the main repo. They are there (marked as deprecated) just to make sure we have a smooth transition.

[Mario Carneiro]

That said I think a deprecation linter is an essential part of easing migration pains so I'm happy to see it. Deciding when to use it, and how long to keep deprecated things around, is a tricky question, though.

[Leonardo de Moura]

Not sure how long we will keep them there. The first approximation is to keep them there until all key projects have moved to the new API.

[Nicolas Rouquette]

It would be great to have an index of Lean4 projects like what the Scala center does with scaladex: https://index.scala-lang.org/ Then we could have CI to analyze the potential impact of deprecating or changing an API across all indexed Lean4 projects.

[Leonardo de Moura]

@Nicolas Rouquette Yes, it would be awesome.

[Jannis Limperg]

Could we get an option to make the deprecated warning an error instead? Imo this would be more convenient than hunting for warnings. (Also, I like this API change!)

[Sebastian Ullrich]

I think I've mentioned it before regarding linters, but the simplest option would be one for turning warnings into errors in general

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/d6f0880d1194b304200777cc1a6ef0e5e49a06df

[Jannis Limperg]

Thanks!