lake new with mathlib

Stream: lean4

[Arthur Paulino]

There is an issue with the math template for a Lake package: it may use a toolchain that's incompatible with mathlib4's. That happens because at package initiation time we haven't downloaded mathlib4 yet so we can't overwrite lean-toolchain with the one from mathlib4.

Do you folks have alternative ideas?

[Patrick Massot]

Yes, this is part of what I called "lake isn't working"

[Sebastian Ullrich]

Arthur Paulino said:

Do you folks have alternative ideas?

Force the materialization of mathlib4, then copy lean-toolchain? It will likely be materialized soon enough anyway after invoking init.

[Arthur Paulino]

Patrick Massot said:

Yes, this is part of what I called "lake isn't working"

What else didn't work?

[Notification Bot]

Arthur Paulino has marked this topic as unresolved.

[Patrick Massot]

Fetching oleans, but we already discussed that one was because I didn't run it in the correct folder (although the root cause is that it expect users to run it instead of doing it right away when creating the project).

[Arthur Paulino]

Do we want Lake to call cache though? I think it's more prudent to leave cache as an independent executable in mathlib4 that is supposed to be called manually

[Arthur Paulino]

Until we have a generic and reliable implementation of caching in Lake itself, which would allow us to call lake cache get instead of lake exe cache get, configure custom hosts, inherit caches from dependencies etc, it's better to keep cache as an isolated thing

[Arthur Paulino]

The current implementation of cache is a quick - but not too dirty - solution to speed up the porting effort. With a bit more effort I was able to make it work (unreliably due to curl issues) for downstream projects like mathport.

[Patrick Massot]

Here I'm specifically talking about creating a new project. If you create a new math project there is nothing you can do before getting mathlib oleans.

[Arthur Paulino]

Even then... what if cache downloads corrupted oleans during initialization? I would be more comfortable with cache users calling it manually at its current stage

[Arthur Paulino]

If we mix things together, users might be more confused with errors, thinking that it was a bug in the scope of Lake when it was not. Or simply being confused by how the pieces come together. In my understanding, calling cache from Lake is a bad eng decision. The fundamental flaw is that mathlib4 is a downstream project wrt lake and cache is implemented in mathlib4 so it would be a weird design to call cache from lake

[Sebastian Ullrich]

That doesn't make sense, lake init _ math clearly makes Lake already conceptually dependent on mathlib4. It would not be a new dependency edge.

[Arthur Paulino]

We can call it a "soft" dependency. In fact, it only depends on the fact that there exists a Git repository hosted at github/leanprover-community/mathlib4

[Arthur Paulino]

But if we create a "hard" dependency, by making Lake rely on some implementation of mathlib4 by assuming that it behaves in a certain way, maintaining the thing coherent would be hell: imagine a Lake command that only works for certain versions of mathlib4

[Arthur Paulino]

Sebastian Ullrich said:

Arthur Paulino said:

Do you folks have alternative ideas?

Force the materialization of mathlib4, then copy lean-toolchain? It will likely be materialized soon enough anyway after invoking init.

This PR implements just that https://github.com/leanprover/lake/pull/152

[Arthur Paulino]

The PR has been merged but I don't know when that change will be released for a new toolchain.

This is important because the mathlib4 readme needs to be updated with such toolchain suggestion