channel events

Stream: lean4

[Kim Morrison]

Kim Morrison changed the description for this channel.

• Old description:

Questions & discussion around the programming language Lean. Community Guidelines

• New description:

Development of the Lean programming language. Please use "general", "mathlib4" or "new members" for questions about using Lean. Community Guidelines

[Julian Berman]

Is this channel taking over for #lean4 dev then? Or otherwise is there guidance on when to put stuff there?

[Kim Morrison]

I think there is previous discussion about this, but I'm not finding it now. My memory, possibly inaccurate, is that the feeling was that the #lean4 dev channel was not particularly useful separately (historically it was a private channel), and that instead effort should be made to steer "general" questions away from #lean4, allowing to take over that role.

[Eric Wieser]

I've often used this channel for "questions about some function within the Lean namespace" or "weird behavior of a builtin tactic". Should threads like that move elsewhere?

[Damiano Testa]

Indeed, I asked this question today in #general because of the change, but would have asked here until yesterday!

[Kim Morrison]

Hmm... I think if there's a reasonable chance the answer would be "we should fix that", then it's fine here. --- and many questions about functions in the Lean namespace or about builtin tactics admit that answer!

[Kim Morrison]

Mostly I just want to avoid "I have a new user question, and since I am programming in Lean 4 I should post in the Lean 4 channel".

[Kim Morrison]

There's no need to be excessively restrictive beyond that, so if someone wants to suggest (or just implement) different wording, please do.