## Stream: general

### Topic: moving mathlib to 3.5c

#### 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?

Let's find out!

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

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

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

#### 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?

#### Rob Lewis (Jan 29 2020 at 17:22):

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

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

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

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

#### Simon Hudon (Jan 29 2020 at 17:24):

What check is that?

#### Rob Lewis (Jan 29 2020 at 17:25):

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

#### Rob Lewis (Jan 29 2020 at 17:25):

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

#### Bryan Gin-ge Chen (Jan 29 2020 at 17:26):

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

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

#### 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?

#### 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

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

#### Patrick Massot (Jan 29 2020 at 18:07):

Also issue #95 should be fixable without breaking anything.

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

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

#### 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

#### 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

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

#### Mario Carneiro (Jan 30 2020 at 11:08):

We don't need dlist

#### Mario Carneiro (Jan 30 2020 at 11:08):

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

#### Rob Lewis (Jan 30 2020 at 12:39):

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

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

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

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

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

#### Rob Lewis (Jan 30 2020 at 13:22):

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

#### 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

#### Rob Lewis (Jan 30 2020 at 14:12):

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

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

#### Mario Carneiro (Jan 30 2020 at 17:49):

What is new in the olean files?

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

#### 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

#### Rob Lewis (Jan 31 2020 at 10:05):

So we should:

and then I think we're ready.

#### 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

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

#### 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?

#### Yury G. Kudryashov (Jan 31 2020 at 23:43):

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

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

#### Rob Lewis (Feb 04 2020 at 16:19):

I can do the rest from the mathlib side.

#### Simon Hudon (Feb 04 2020 at 17:16):

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

Thanks!

#### Yury G. Kudryashov (Feb 04 2020 at 18:00):

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

#### Yury G. Kudryashov (Feb 04 2020 at 18:00):

(after this release)

#### Mario Carneiro (Feb 04 2020 at 18:24):

yes, not in 3.5.0c but soon enough.

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

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

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

#### Simon Hudon (Feb 04 2020 at 18:41):

We can create an issue for those proposed changes.

#### 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

#### Rob Lewis (Feb 04 2020 at 22:47):

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

#### Rob Lewis (Feb 04 2020 at 22:48):

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

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

#### Rob Lewis (Feb 04 2020 at 22:49):

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

#### Johan Commelin (Feb 05 2020 at 11:50):

CI is happy with the move: #1958

#### Rob Lewis (Feb 05 2020 at 12:13):

Report any version-related disasters here!

#### Johan Commelin (Feb 05 2020 at 12:17):

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

#### Yury G. Kudryashov (Feb 05 2020 at 22:35):

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

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

#### 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?

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

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

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

#### 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?

#### Patrick Massot (Feb 09 2020 at 13:21):

At least this is what I ended up doing yesterday.

#### Patrick Massot (Feb 09 2020 at 13:21):

I'll see what happens with the next nightly.

#### 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?

Yes it did

#### Patrick Massot (Feb 10 2020 at 21:26):

Nice, I should resume work on rename_var then.

#### 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