Zulip Chat Archive

Stream: mathlib4

Topic: deprecate syntax?

Thomas Murrills (Feb 24 2024 at 00:36):

Is there currently a systematic way to deprecate e.g. tactic syntax? This is for cases where we can still parse/handle the syntax, but want to encourage moving to another syntax. It'd be nice to e.g. write attribute [deprecated <newSyntaxName>] <syntaxName>.

Mario Carneiro (Feb 24 2024 at 04:15):

No. The first instance of this is coming up soon, because fun. is deprecated in the next stable version of lean in favor of nofun

Ruben Van de Velde (Feb 24 2024 at 10:09):

That's no fun (sorry)

Thomas Murrills (Feb 24 2024 at 17:24):

I can’t wait for that phrasing to be immortalized in the release notes.

Thomas Murrills (Feb 24 2024 at 17:28):

When you say “of this” do you mean:

  1. of a new systematic way to deprecate syntax
  2. of the need to systematically deprecate syntax (which we don’t have, but want)
  3. of a case where syntax is deprecated (and we’re dealing with it on an ad-hoc basis)
  4. something else?

Mario Carneiro (Feb 24 2024 at 22:48):

mostly 3, a bit of 2

Last updated: May 02 2025 at 03:31 UTC