Call to action: porting mathlib to Lean 3.6

Stream: general

[Gabriel Ebner]

Due to a conference deadline, I would like to release Lean 3.6 this week. I'm aware that there are still quite a few outstanding changes, but there's no need to hurry. We'll be doing a 3.7 release pretty soon after.
I've made a mathlib branch for the next Lean release and started porting: https://github.com/leanprover-community/mathlib/tree/lean-nightly However, there's lots of breakage from removing sub_eq_add_neg and add_comm. It would be really great if you could help in the porting process!

[Scott Morrison]

I wonder if the simplest thing to do is just mark those lemmas as @[simp] again, but in mathlib. Then there's no urgency, as we can patch mathlib continuously.

[Simon Hudon]

Why are bumping to 3.6 and 3.7 already?

[Gabriel Ebner]

The reason why I'd like to release 3.6 very soon (i.e. this week) is because we have a conference deadline coming up, and we'd like to have mathlib running on Lean 3.6 (mainly for the nested docstrings).

[Gabriel Ebner]

I think there have been enough changes floating around to warrant a 3.7 release. Floris suggested that it would be better to have more but smaller releases for Lean so that it is easier to migrate mathlib from one release to the next, and I agree.

[Bryan Gin-ge Chen]

As I recall the nested docstrings were originally for @Rob Lewis's next doc-gen update. Are those PRs going to land soon as well? (No rush, just curious.)

[Simon Hudon]

What I mean is that there are version numbers that we can be using like 3.5.2. Why jump up to 3.6 and 3.7 already? I don't think we have any major features yet, do we?

[Gabriel Ebner]

I was mainly going by backwards compatibility. 3.5.1 contained only bugfixes and new features, while 3.6 will break backwards compatibility. 3.7 will very likely break backwards compatibility again.

[Simon Hudon]

I can see moving to 3.6 but I don't think we could put a few backward compatibility breaking version in 3.6

[Gabriel Ebner]

I'm not sure I understand you correctly. We already have breaking changes in 3.6 (the removal of three simp lemmas). I'd also like to merge the discrete_field change, which is also very much a breaking change.

[Bryan Gin-ge Chen]

The nested comments in docstrings change is also a breaking change, since it changes the Lean grammar.

[Johan Commelin]

I think Simon means that 3.6.1 could break compatibility with 3.6

[Johan Commelin]

Just make 3.6.x a rapid chain of backwards-incompatible bumps.

[Gabriel Ebner]

Ah ok, I'm completely fine with that as well. That's just like the old days.

[Rob Lewis]

Bryan Gin-ge Chen said:

As I recall the nested docstrings were originally for Rob Lewis's next doc-gen update. Are those PRs going to land soon as well? (No rush, just curious.)

Yep, once nested docstrings land, I'll finish those up.

[Wojciech Nawrocki]

Neither of those schemes is compatible with semver, although 3.6, 3.7, .. is maybe a bit closer. To be fully compatible, the next community version would have to be called 4.0.0c or something, which would probably confuse everyone.

[Sebastian Ullrich]

That's easy, just skip straight to 5.0.0c

[Kevin Buzzard]

That will cause confusion. How about we just rename the software? "Fat"?

[Simon Cruanes]

"Mean"

[Simon Cruanes]

So that people can refer to the "lean and mean" community!

[Gabriel Ebner]

I wonder if the simplest thing to do is just mark those lemmas as @[simp] again, but in mathlib. Then there's no urgency, as we can patch mathlib continuously.

It's way too much fun and I'm already fixing up the breakage causes by the discrete_field removal anyhow.

[Anne Baanen]

I'll help with the porting process :D I guess I will start with the linear_algebra and ring_theory directories since I know them the best