Create a mathlib branch that builds with Lean master?

Stream: general

[Jannis Limperg]

Would it be convenient to have a mathlib branch that builds with Lean master? Concretely:

• Create a new long-lived branch lean-master.
• Whenever someone PRs to Lean, they also update mathlib as follows:
  • rebase lean-master onto master
  • build lean-master with the Lean from their PR
  • fix any resulting breakage and push the fixes as soon as the PR is merged
• When a new version of Lean is released, the mathlib update goes like this:
  • rebase lean-master onto master
  • 'merge' lean-master into master (this is always a fast-forward merge due to the rebasing)
  • update the Lean version in leanpkg.toml

Advantages:

• We always have a version of mathlib that builds with Lean master. This is effectively a big integration test for Lean. I've found this very useful while developing my own PRs.
• Authors of Lean PRs fix their own breakage, which they are uniquely qualified to do because they already understand the changes. (This also serves as an incentive to avoid breakage. ;))

Disadvantages:

• The rebase steps may generate merge conflicts relating to any Lean PRs since the last release. I'm not sure how annoying this would be in practice.

[Mario Carneiro]

That sounds like lean-master is actually ahead of lean master, if it includes PRs

[Jannis Limperg]

While working on a Lean PR, the PR author would have a local branch, derived from upstream lean-master, that incorporates the necessary mathlib changes. This can be used to locally test the Lean changes. When the PR is merged, these changes go into upstream lean-master.

[Chris Wong]

Can we go even further – what's stopping us from putting lean and mathlib in the same repo?

[Chris Wong]

Correct me if I'm wrong, but the purpose of separate repositories is to allow two components to evolve independently.

So I think the first question we should ask, before going into any details, is whether we want this independence.

[Johan Commelin]

It's also separating concerns. Fooling around with mathlib is (in my eyes) a lot easier if there is no cpp code around

[Kevin Buzzard]

And there are certainly people using Lean that have no desire to use the maths library