moving mathlib to 3.5c

Stream: general

[Rob Lewis]

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?

[Kevin Buzzard]

Let's find out!

[Simon Hudon]

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]

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]

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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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]

What check is that?

[Rob Lewis]

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

[Rob Lewis]

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

[Bryan Gin-ge Chen]

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

[Rob Lewis]

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]

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]

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]

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

[Patrick Massot]

Also issue #95 should be fixable without breaking anything.

[Rob Lewis]

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]

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]

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]

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]

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]

We don't need dlist

[Mario Carneiro]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

What is new in the olean files?

[Rob Lewis]

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

[Wojciech Nawrocki]

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]

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]

So we should:

• fix the leanpkg warning
• merge anything else to leanprover-community/lean that's ready to go
• make a 3.5.1 release
• update https://github.com/leanprover-community/mathlib/tree/update-3-5 for 3.5.1

and then I think we're ready.

[Kevin Buzzard]

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

[Rob Lewis]

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]

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

[Yury G. Kudryashov]

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

[Rob Lewis]

@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]

I can do the rest from the mathlib side.

[Simon Hudon]

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

[Rob Lewis]

Thanks!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(after this release)

[Mario Carneiro]

yes, not in 3.5.0c but soon enough.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Simon Hudon]

We can create an issue for those proposed changes.

[Simon Hudon]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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

[Johan Commelin]

CI is happy with the move: #1958

[Rob Lewis]

Report any version-related disasters here!

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Rob Lewis]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Rob Lewis]

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]

At least this is what I ended up doing yesterday.

[Patrick Massot]

I'll see what happens with the next nightly.

[Patrick Massot]

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

[Simon Hudon]

Yes it did

[Patrick Massot]

Nice, I should resume work on rename_var then.

[Patrick Massot]

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