Creating a Lean project

Stream: lean4

[Martin Dvořák]

Is there a reason why https://leanprover-community.github.io/install/project.html recommends this particular build?

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

[Shreyas Srinivas]

The math template was changed after that toolchain. You don't have to use that toolchain strictly speaking. Later toolchains are fine.

[Shreyas Srinivas]

However asking people to use a toolchain later than so and so, and then call lake new or init is two steps. This way, you get everything in one step, and you have a command that can be copied into the terminal.

[Shreyas Srinivas]

From a documentation perspective it is less than ideal. For a tutorial/instructions on "how to get started quickly" this is more efficient.

[Martin Dvořák]

Cannot I simply do lake new my_project math and obtain the newest version that my installation knows about?
Afterwards, I'll typically do lake update anyways.

[Shreyas Srinivas]

as long as your toolchain is newer than the suggested toolchain this will work.

[Sebastian Ullrich]

I updated the wiki instructions with the new elan command implemented specifically for this task: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#in-a-new-project
Please give it a try and feel free to update the other documentation as well

[Shreyas Srinivas]

It just says lean-toolchain, without mentioning a specific toolchain.

[Shreyas Srinivas]

Why do we need to mention it at all if we don't have to specify the toolchain date

[Sebastian Ullrich]

I suppose I didn't give enough context there, please see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elan/near/371306430

[Shreyas Srinivas]

ah okay now I get it. You can specify a path to (EDIT: some not all) lean4 projects and lake reads the lean-toolchain file of that project and installs it.

[Shreyas Srinivas]

Could we make it work for arbitrary projects? elan toolchain install <project_path>:lean-toolchain

[Sebastian Ullrich]

What's your use case?

[Shreyas Srinivas]

Dependencies. I have project a and I want to use it in project b and not deal with potential or actual toolchain mismatch hassles. So I would want to default to using the same toolchain in project b as I have in project a.

[Sebastian Ullrich]

Use cp? :big_smile:

[Sebastian Ullrich]

How to keep the project's lean-toolchain in sync is a related but separate issue; this is specifically about acquiring an initial toolchain in the first place (which ideally is the same one you then use to build the project)

[Shreyas Srinivas]

Wouldn't the second problem be solved for up to 1 dependency per project if the line in the lean-toolchain could reference the lean toolchain in another project?

[Sebastian Ullrich]

How would it know the revision of the project? Do you want elan to parse the Lake manifest?

[Mac Malone]

@Sebastian Ullrich I think @Shreyas Srinivas is asking if a lean-toolchain file could just contain a file path to another toolchain file to use. For example, in a package depending on mahtlib, the package could just put lake-packages/mathlib or similar (maybe dir:<file-path>?) in the root lean-toolchain to have it delegate to mathlib's lean-toolchain.

[Sebastian Ullrich]

That can't work as we need the toolchain in order to materialize the dependency in the first place

[Shreyas Srinivas]

Sebastian Ullrich said:

That can't work as we need the toolchain in order to materialize the dependency in the first place

Why can't the toolchain be deduced to be that mentioned in the lean-toolchain file in the provided path, and then materialize dependencies according to that toolchain?

[Alex J. Best]

But you need a version of lake/lean to get the dependency and put it in the right place to then read said file from

[Shreyas Srinivas]

Ah, I see. Lake $\subset$ toolchain