Lake with more projects

Stream: lean4

[Martin Dvořák]

I have project X (which depends on Mathlib) uploaded to GitHub.
I have project Y in my computer, where Y depends on the project X from GitHub (and also on Mathlib, but I removed the explicit reference to Mathlib from Y's lakefile, so I get Mathlib only transitively).
Now, in order to build Y using Lake, I had to downgrade the lean-toolchain of Y to the X's lean-toolchain.
Only then I managed to build Y.
Is this behavior expected?

[Joachim Breitner]

What was the error message?

[Martin Dvořák]

I don't remember. It was several screens long.

[Martin Dvořák]

A natural follow-up question is:

Let's say project X depends on Mathlib from day D and project Y depends on Mathlib from day E, where D < E.
Are there circumstances under which Y can import X?

[Martin Dvořák]

I am worried that one day I will need to import project A that depends on Mathlib version α and project B that depends on Mathlib version β into a project C (where the Mathlib version is under my control, but I cannot change either A or B, so one of them will certainly be "off"). In short:

Mathlib α → A → C ← B ← Mathlib β

This is probably the most serious issue from all I have described. Has it been taken into consideration when developing Lake?

[Henrik Böving]

The way you deal with this in other programming languages is that you put constraints on the versions that your package can operate with. So for example one might say I need it the version to be >= 1.3.0 and another might say >= 1.2.0 and <= 1.4.0. And then you can run some constraint solver in your thing that ends up figuring out which one to use. But right now lake is not at all capable of doing this. I don't know if it is planned but we will definitely need a version resolution mechanism (regardless of whether we use semver or whatever else) sooner or later.

[Mario Carneiro]

Unless A compiles with Mathlib β or B compiles with Mathlib α you are out of luck, because you can't have two mathlibs in the dependency graph

[Martin Dvořák]

What I think is very likely situation:

Std σ → Mathlib α → A → C ← B ← Std τ

[Mario Carneiro]

same deal

[Mario Carneiro]

you can control the version used by setting Std υ as a dependency in C, but you will probably be forced to use Std σ if you want the build cache from mathlib

[Mario Carneiro]

It's not a deal-breaker, because if you are lucky B still compiles with Std σ

[Martin Dvořák]

Mario Carneiro said:

Unless A compiles with Mathlib β or B compiles with Mathlib α you are out of luck, because you can't have two mathlibs in the dependency graph

Let's continue here:

Mathlib α → A → C ← B ← Mathlib β

If everything goes well and Mathlib β is newer than Mathlib α, both A and B will ideally compile with Mathlib β.
Does then Lake have mechanisms that allow the author of C to specify {Mathlib β, A, B} while preserving the dependency on the original repositories containing A and B?

[Mario Carneiro]

if C depends on Mathlib β then A and B will be compiled against it

[Martin Dvořák]

Oh, just keep an explicit dependency on Mathlib in the C's lakefile?

[James Gallicchio]

FWIW, I think the end solution that we're gravitating towards is to automate the process of dependency updates, so that all projects are up to date with all their dependencies at all times and there is never disagreement about which version of a dependency to use. (Though, being downstream of mathlib is going to be a challenge, given how frequently it updates...)

[Martin Dvořák]

Though, being downstream of mathlib is going to be a challenge, given how frequently it updates.

I expect it to be a big issue. Maybe just maybe Mathlib should have an official release, not more than once per month, and external projects be recommended to depend on the official release.

[James Gallicchio]

I have plans to let projects track less-frequently updating dependencies and stay up-to-date with respect to those; so for example, you could say "stay up to date with lean-toolchain" and then your project would only update Mathlib when it updates to the new toolchain releases :)

[Ruben Van de Velde]

That might help for projects depending on multiple projects downstream of mathlib, but it sounds even more painful for that first line of dependents, since now you have a whole month of breaking changes to deal with, and a month's delay to get new content from mathlib

[Ruben Van de Velde]

(I don't have good answers either, besides pushing as much as possible into mathlib for as long as that works)

[James Gallicchio]

Ruben Van de Velde said:

it sounds even more painful for that first line of dependents

that's the tradeoff you make as a library maintainer, based on how much breakage you expect from each update :shrug: but the goal is for your downstream clients to be able to choose to update less frequently than you do.

the other goal is to be able to "fix your downstreams" before merging changes upstream. So if e.g. Martin cares a lot about project Y when updating project X, he can make the necessary changes to Y before even merging a change to X, so that there's no surprise breakage.

[Martin Dvořák]

Ruben Van de Velde said:

now you have a whole month of breaking changes to deal with, and a month's delay to get new content from mathlib

I think it is not necessarily a dichotomy. You can have a ˙develop˙ branch that depends on the newest Mathlib, and you can have a release that syncs with the official Mathlib release. Most users of your library will depend on the latter.

[Ruben Van de Velde]

Has anyone rebuilt the mathlib update bot we had for mathlib 3, btw?

[Kevin Buzzard]

To put this in context,at this point in time it seems unlikely that anyone would want to depend on a project which depends on mathlib, let alone depending on two such projects. I am very unclear about the current concrete aims of mathlib; for me a key motivation was to get an undergraduate degree in mathematics in there, but this has now largely been achieved (at least for the undergraduate degree I took) and much of the work of my students could be summarised as getting a master's level course in there. But is the idea to let it expand forever?

[Siddhartha Gadgil]

Kevin Buzzard said:

To put this in context,at this point in time it seems unlikely that anyone would want to depend on a project which depends on mathlib, let alone depending on two such projects. I am very unclear about the current concrete aims of mathlib; for me a key motivation was to get an undergraduate degree in mathematics in there, but this has now largely been achieved (at least for the undergraduate degree I took) and much of the work of my students could be summarised as getting a master's level course in there. But is the idea to let it expand forever?

For the record, I do have the first kind of dependency. A project LeanAide has a bunch of tools and depends on Mathlib and another was a project which was code for my course, hence depended on LeanAide.

[Kevin Buzzard]

I stand corrected! Thanks Siddhartha.