Zulip Chat Archive

Stream: general

Topic: Time to move to 3.5?


view this post on Zulip Scott Morrison (Oct 25 2019 at 23:34):

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.)

view this post on Zulip Scott Morrison (Oct 25 2019 at 23:34):

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.

view this post on Zulip Scott Morrison (Oct 25 2019 at 23:35):

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.

view this post on Zulip Mario Carneiro (Oct 25 2019 at 23:42):

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

view this post on Zulip Alex J. Best (Oct 25 2019 at 23:44):

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.

view this post on Zulip Mario Carneiro (Oct 25 2019 at 23:44):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 23:46):

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)

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 00:26):

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).

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 00:30):

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.

view this post on Zulip Alex J. Best (Oct 26 2019 at 00:36):

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?

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 00:38):

Yep, here's the previous discussion.

view this post on Zulip Simon Hudon (Oct 26 2019 at 01:37):

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

view this post on Zulip Simon Hudon (Oct 26 2019 at 01:38):

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.

view this post on Zulip Mario Carneiro (Oct 26 2019 at 01:55):

I don't want it breaking on every commit though

view this post on Zulip Simon Hudon (Oct 26 2019 at 02:04):

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>

view this post on Zulip Mario Carneiro (Oct 26 2019 at 03:08):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 03:09):

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

view this post on Zulip Simon Hudon (Oct 26 2019 at 03:13):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 03:50):

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?

view this post on Zulip Simon Hudon (Oct 26 2019 at 03:55):

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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 08:17):

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

view this post on Zulip Mario Carneiro (Oct 26 2019 at 08:20):

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

view this post on Zulip Scott Morrison (Oct 26 2019 at 08:20):

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).


Last updated: May 13 2021 at 00:41 UTC