Time to move to 3.5?

Stream: general

[Scott Morrison]

I'm wondering what everyone thinks about moving mathlib to 3.5? It seems we've accumulated a fair few small fixes there by now, and it would be nice to have them. (As an example, earlier today someone wanted symmetry at h but had to learn about symmetry' at h.)

[Scott Morrison]

There's of course some hassle to move the community to a new default version. But I don't see any reason at this point that we should be fearful of switching to a "community" version; that is, it should be no more intimidating that switching from 3.4.1 to 3.4.2.

[Scott Morrison]

I'm guessing that when it becomes time to start thinking about migration plans to Lean 4, it's also going to be useful to have some flexibility on the Lean 3 side.

[Mario Carneiro]

We talked about this a bit in portland. One thing we have to get right is the lean update pipeline; everyone has forgotten how to do that and unless it's really painless no one will be incentivized to do it and bad things will happen

[Alex J. Best]

Are there any backwards incompatible changes that need to be made to mathlib in this instance, I seem to remember mathlib compiling fine with community? The only issue I had was that as olean files are linked to the lean version update-mathlib became useless. It would be good as a first step to compile oleans for community too and make update-mathlib use the ones depending on the lean version.

[Mario Carneiro]

In the upgrade to 3.5, there should be no backward incompatibilities

[Mario Carneiro]

but I want to restart an update schedule if we start moving ahead with 3.5, and we can't be backward compatible forever (indeed, a lot of the things we want to change are blocked precisely because of backward compatibility)

[Bryan Gin-ge Chen]

One thing we have to get right is the lean update pipeline

Related question: Is there any way to get elan update to check and update to the latest commit of 3.5? Running elan toolchain install leanprover-community/lean:nightly each time works well enough, but is less convenient (mainly because I can never remember the precise command).

[Bryan Gin-ge Chen]

The only issue I had was that as olean files are linked to the lean version update-mathlib became useless. It would be good as a first step to compile oleans for community too and make update-mathlib use the ones depending on the lean version.

I think at one point Mario suggested that we remove the version / commit check for olean files from Lean 3.5.0c. It's a tiny change, I could PR it this weekend.

[Alex J. Best]

wow yeah if that is possible that would be great. I guess that would restrict us from every changing the olean format in community, but that seems really unlikely anyway right?

[Bryan Gin-ge Chen]

Yep, here's the previous discussion.

[Simon Hudon]

I'm not too hot on the idea of removing that check. The tactics API changes in Lean 3.5.0 so the olean files for 3.5.0 refer to symbols that don't make sense in 3.4.2

[Simon Hudon]

Also, right now, we don't have a 3.5 release. I'm thinking of getting one more feature in and making a release on November 1.

[Mario Carneiro]

I don't want it breaking on every commit though

[Simon Hudon]

How about we only break it when the lean core library changes? We could hash all the Lean files in library and make the version string something like 3.5-<library-hash>

[Mario Carneiro]

I don't see why we need to deliberately break it at all. Let it break itself

[Mario Carneiro]

The olean file refers to things by their names, so it's not any more brittle than a lean file would be

[Simon Hudon]

I just think it will be no fun to debug if you run into trouble

[Mario Carneiro]

I think you will cause trouble much more frequently by doing this. Is there any chance of noting the version difference and reporting it if anything goes wrong in the import?

[Simon Hudon]

The kind of issue that I expect is tactics and definitions crashing when running them if the api they rely on has changed. This is not something that will happen necessarily when processing imports

[Kevin Buzzard]

Would there be a "release 3.5.0" or would you expect users to keep upgrading Lean like they upgrade mathlib?

[Mario Carneiro]

there would be a release 3.5, but there would also be 3.5.1 and the wait would be a lot less than 3.4.2 -> 3.5.0

[Scott Morrison]

It depends a bit on how fast 3.5 starts moving once people are actually using it. But hopefully every month or two we would bump to 3.5.(n+1).