Zulip Chat Archive

Stream: general

Topic: moving mathlib to 3.5c


view this post on Zulip Rob Lewis (Jan 29 2020 at 16:40):

I'm looking into transitioning mathlib to Lean 3.5c now. This will allow us to take advantage of various features, bug fixes, etc that have been implemented there. The current version is backward compatible -- mathlib builds under both 3.4.2 and 3.5c right now. But this will probably change in the future.

Right now, the upgrade path looks easy enough: we change mathlib's leanpkg.toml to read lean_version = "leanprover-community/lean:3.5.0". Any user running elan just needs to run leanpkg configure in mathlib root, and elan should find the binary. Projects that use mathlib as a dependency should do similar, with leanpkg upgrade to bump mathlib to a 3.5 version.

At the same time we change leanpkg.toml, we'll change the CI to push 3.5.0 nightlies. I think this means update-mathlib and cache-olean should continue to work seamlessly, and shouldn't break on older commits from before the change.

Maybe I'm too optimistic -- what am I missing? What will break?

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 16:50):

Let's find out!

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:18):

I think @Mario Carneiro might have a few things to say here. I know he doesn't follow the blessed path and other users don't either.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:19):

There are some PRs to 3.5c that I think might as well be merged before a move. 87, 97, and 99 look pretty unobjectionable. 88 would be great too. I tagged a handful that I think would be backward compatible, but we don't necessarily need all of them.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:21):

I wasn't using elan until about two hours ago; it's a painless switch. Power users should be able to upgrade their lean version on their own, I guess. I'm not sure how many non-power users we have who aren't using elan.

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:21):

The travis build has (or had?) a daily cron job to compile itself with 3.5. Has it made it to the Github Actions?

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:22):

Right now Actions compiles mathlib with 3.4.2 and the 3.5c nightly every build.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:22):

The only change there will be removing the 3.4.2 build and switching 3.5c from nightly to a particular release.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:23):

Or just changing 3.4.2 to a 3.5c release, if we want to keep testing the nightlies.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:24):

BTW, one of the CI checks on leanprover-community/lean is failing right now. It doesn't look significant. But might be nice to get that working when we switch.

view this post on Zulip Simon Hudon (Jan 29 2020 at 17:24):

What check is that?

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:25):

See the build here: https://github.com/leanprover-community/lean/pull/99

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:25):

It's a doc PR so I don't think I broke anything!

view this post on Zulip Bryan Gin-ge Chen (Jan 29 2020 at 17:26):

The failure is here; looks totally unrelated, so hopefully it should work if restarted.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:28):

The same problem shows up on a build on Anne's PR from earlier today. But it could be a temporary thing, yeah.

view this post on Zulip Rob Lewis (Jan 29 2020 at 17:31):

A related question, how hard is it to direct elan to a local Lean build? I think @Gabriel Ebner mentioned doing this at some point?

view this post on Zulip Bryan Gin-ge Chen (Jan 29 2020 at 17:33):

I've been doing it; I don't remember the details but it wasn't hard. I think I just followed the instructions from the command line help.

edit: try elan toolchain help link

view this post on Zulip Patrick Massot (Jan 29 2020 at 18:06):

I still vote that rintro should replace intro in the core library (the interactive versions of course).

view this post on Zulip Patrick Massot (Jan 29 2020 at 18:07):

Also issue #95 should be fixable without breaking anything.

view this post on Zulip Rob Lewis (Jan 29 2020 at 22:15):

I still vote that rintro should replace intro in the core library (the interactive versions of course).

This might be a surprisingly big refactor. rintro would have to be implemented without depending on anything that uses intro. Possible, but it will take work. I guess we could rename intro to intro' and bootstrap.

view this post on Zulip Patrick Massot (Jan 29 2020 at 22:21):

This is why I said "the interactive version". Of course we would still use tactic.intro. And if this is not enough then indeed we can rename intro to intro'. We can even call it updating stage0 or whatever sounds like Lean4 bootstrapping.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 01:51):

I don't think the implementation of rintro uses tactic.interactive.intro at all, and in any case tactic.intro is essentially the same thing

view this post on Zulip Mario Carneiro (Jan 30 2020 at 01:52):

if we want a noninteractive version of rintro, it will have a much more complicated type because it creates a complicated hierarchy of subgoals

view this post on Zulip Rob Lewis (Jan 30 2020 at 09:53):

rintro depends on dlist, and interactive intro is used in proofs in some of the core dlist definitions. I'm not saying there's any theoretical reason intro needs to be implemented first, but disentangling them will take effort.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 11:08):

We don't need dlist

view this post on Zulip Mario Carneiro (Jan 30 2020 at 11:08):

I just use list A -> list A most of the time

view this post on Zulip Rob Lewis (Jan 30 2020 at 12:39):

I just noticed this issue on community Lean: https://github.com/leanprover-community/lean/issues/98

view this post on Zulip Rob Lewis (Jan 30 2020 at 12:39):

We should check that Windows elan is happy with the 3.5c release version before making the change official.

view this post on Zulip Rob Lewis (Jan 30 2020 at 12:40):

We should also look into the nightlies issue, of course, but that doesn't have to block the switch.

view this post on Zulip Rob Lewis (Jan 30 2020 at 13:20):

Does olean-rs still work with oleans from 3.5c? I know they store additional information now.

view this post on Zulip Rob Lewis (Jan 30 2020 at 13:21):

AFAICT olean-rs isn't used anywhere critical, so this also doesn't have to block the switch if there are issues. But we should at least be aware.

view this post on Zulip Rob Lewis (Jan 30 2020 at 13:22):

(I guess this is a question mostly for @Simon Hudon and @Mario Carneiro )

view this post on Zulip Rob Lewis (Jan 30 2020 at 14:11):

I created a branch for the move. Let me know if you notice any missing changes. https://github.com/leanprover-community/mathlib/tree/update-3-5

view this post on Zulip Rob Lewis (Jan 30 2020 at 14:12):

I'll see if it builds with my Windows laptop when I get home.

view this post on Zulip Rob Lewis (Jan 30 2020 at 14:25):

In the meantime, is there other infrastructure that needs to be updated? I don't see anything 3.4.2-specific in the scripts repo.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 17:49):

What is new in the olean files?

view this post on Zulip Rob Lewis (Jan 30 2020 at 17:57):

https://github.com/leanprover-community/lean/commit/354deadc203454b76f72f325e7c566f10adf52e1 at least

view this post on Zulip Wojciech Nawrocki (Jan 30 2020 at 22:42):

Note that I changed that again later, introducing a new mod_doc object to .olean files here (the diff above is a backwards-compatible change as far as olean-rs is concerned since it doesn't change the format).

view this post on Zulip Rob Lewis (Jan 31 2020 at 10:03):

Windows, OS X, and Ubuntu all seem happy to build a 3.5 mathlib with elan. There's a leanpkg warning (on all systems) we should fix first: https://github.com/leanprover-community/lean/issues/105

view this post on Zulip Rob Lewis (Jan 31 2020 at 10:05):

So we should:

and then I think we're ready.

view this post on Zulip Kevin Buzzard (Jan 31 2020 at 11:21):

What is the difference between 3.5.0 and 3.5.1? Sorry for the naive question

view this post on Zulip Rob Lewis (Jan 31 2020 at 12:08):

Nothing much. There have been PRs merged to Lean since the 3.5.0 release that I'd like to include before we switch.

view this post on Zulip Yury G. Kudryashov (Jan 31 2020 at 23:42):

BTW, would it break compatibility if we export has_insert.insert to the root namespace instead of creating another def?

view this post on Zulip Yury G. Kudryashov (Jan 31 2020 at 23:43):

Another question: are we going to move algebraic structures from stdlib to mathlib before lean4?

view this post on Zulip Rob Lewis (Feb 04 2020 at 16:19):

@Simon Hudon @Mario Carneiro / anyone else maintaining 3.5: would it be possible to take care of the first three bullet points above soon? I think https://github.com/leanprover-community/lean/pull/106 is the only PR that really needs to make it in before we switch. Then we just need a release.

view this post on Zulip Rob Lewis (Feb 04 2020 at 16:19):

I can do the rest from the mathlib side.

view this post on Zulip Simon Hudon (Feb 04 2020 at 17:16):

Ok, I just merged a few PRs. Once, they finish building, we can make a release.

view this post on Zulip Rob Lewis (Feb 04 2020 at 17:24):

Thanks!

view this post on Zulip Yury G. Kudryashov (Feb 04 2020 at 18:00):

BTW, do you plan to introduce any non-bc changes to 3.*?

view this post on Zulip Yury G. Kudryashov (Feb 04 2020 at 18:00):

(after this release)

view this post on Zulip Mario Carneiro (Feb 04 2020 at 18:24):

yes, not in 3.5.0c but soon enough.

view this post on Zulip Mario Carneiro (Feb 04 2020 at 18:25):

some changes to core cannot be done without breaking backward compatibility (for example, changing discrete_field to field or congr' to congr)

view this post on Zulip Kevin Buzzard (Feb 04 2020 at 18:33):

some changes to core cannot be done without breaking backward compatibility (for example, changing discrete_field to field or congr' to congr)

I guess one could just have an import which defines discrete_field to be field etc? I guess this idea only goes so far though.

view this post on Zulip Yury G. Kudryashov (Feb 04 2020 at 18:36):

Do you collect proposed changes somewhere? I'd like to have export has_insert (instert) instead of a def.

view this post on Zulip Simon Hudon (Feb 04 2020 at 18:41):

We can create an issue for those proposed changes.

view this post on Zulip Simon Hudon (Feb 04 2020 at 19:28):

The release was created, the binaries are now available for Linux, we just have to wait for the other builds to finish:

https://github.com/leanprover-community/lean/releases/tag/v3.5.1

view this post on Zulip Rob Lewis (Feb 04 2020 at 22:47):

Awesome, thanks Simon! I'll finish things from the mathlib side tomorrow.

view this post on Zulip Rob Lewis (Feb 04 2020 at 22:48):

An issue for "core library changes" is a good idea. Renamings, small lemma changes, etc.

view this post on Zulip Rob Lewis (Feb 04 2020 at 22:49):

I think the first mathlib bump should be backward compatible. But 3.5.2 (or 3.6?) can break compatibility, and I don't think we need to wait that long to make the switch.

view this post on Zulip Rob Lewis (Feb 04 2020 at 22:49):

Let's see if there are any technical issues with the upgrade first.

view this post on Zulip Johan Commelin (Feb 05 2020 at 11:50):

CI is happy with the move: #1958

view this post on Zulip Rob Lewis (Feb 05 2020 at 12:13):

Report any version-related disasters here!

view this post on Zulip Johan Commelin (Feb 05 2020 at 12:17):

Thanks @Rob Lewis for all the effort you've spent on this migration

view this post on Zulip Yury G. Kudryashov (Feb 05 2020 at 22:35):

Where can I read about new features of Lean / stdlib we can use now?

view this post on Zulip Rob Lewis (Feb 05 2020 at 22:48):

The changelog has some descriptions. It should probably be updated for the ones that landed just recently. You can also look at the recent commits.

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:00):

What is the current status of the Lean version change? How is it meant to work for project using mathlib?

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:01):

I tried to bump mathlib is the perfectoid project, changing our leanpkg.toml to have the same lean_version line as mathlib. But then update-mathlib doesn't seem to work.

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:01):

I guess this breaks the convention that the lean-3.4.2 branch was to be used.

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:03):

Or maybe not. It seems leanpkg upgrade bumped mathlib to the commit corresponding to the latest nightly. But it still recompiles...

view this post on Zulip Rob Lewis (Feb 09 2020 at 11:15):

I tried on an external project a day after the change. Updating the lean_version and leanpkg upgrade worked just fine. Do you need to touch the oleans?

view this post on Zulip Patrick Massot (Feb 09 2020 at 13:21):

At least this is what I ended up doing yesterday.

view this post on Zulip Patrick Massot (Feb 09 2020 at 13:21):

I'll see what happens with the next nightly.

view this post on Zulip Patrick Massot (Feb 10 2020 at 21:00):

I didn't pay enough attention, did the fix to change made it into the Lean version mathlib is now using?

view this post on Zulip Simon Hudon (Feb 10 2020 at 21:24):

Yes it did

view this post on Zulip Patrick Massot (Feb 10 2020 at 21:26):

Nice, I should resume work on rename_var then.

view this post on Zulip Patrick Massot (Feb 11 2020 at 10:48):

I just bumped mathlib again in the perfectoid project and everything worked fine. I'm not sure what failed last time.


Last updated: May 10 2021 at 17:39 UTC