N00b question

Stream: mathlib4

[Ryan Buchanan]

Is Mathlib4 built into Lean 4, or no? If not, how do I get it?

Do I have to manually import everything I use? That seems kind of tedious. Is there a way I can just import all of Mathlib 4 and start messing around with it?

P.S. I tried importing a command and it didn't work. What do I do?

[Markus Himmel]

mathlib is not bundled with Lean. You can create a project with a dependency on mathlib by following the instructions at https://leanprover-community.github.io/install/project.html#creating-a-lean-project. Once you have that set up, you can import all of mathlib at once by using import Mathlib.

[Ryan Buchanan]

Markus Himmel said:

mathlib is not bundled with Lean. You can create a project with a dependency on mathlib by following the instructions at https://leanprover-community.github.io/install/project.html#creating-a-lean-project. Once you have that set up, you can import all of mathlib at once by using import Mathlib.

Thanks! :smiley:

[Markus Schmaus]

lake +leanprover/lean4:nightly-2023-02-04 new my_project math should probably be updated.

[Mario Carneiro]

Do not worry about the date in the previous command, it ensures you will use a sufficiently recent version of lake but has no impact on the version of lean your project will use.

As I understand it this is a workaround for lake outside a directory defaulting to whatever the user has configured (usually stable which is potentially a very old stable), so asking for any specific version of lake helps ensure reproducibility

[Mario Carneiro]

So we don't actually need to bump the date most of the time; the main reason to do so is if lake new changes behavior (but I'm sure it has since last year)

[Markus Schmaus]

Isn't lake smart enough to figure out a good version if a new user hasn't configured any specific version on their own?

[Kevin Buzzard]

The issue is that someone who set up lake a year ago quite possibly has configured a specific version on their own, they just don't know this, and it's a really old and bad version from when the ecosystem was far less stable.

[Markus Schmaus]

When I read that line while setting up lean, the random nightly tag looked weird and outdated, so I ended up dropping it, and it worked fine. I would expect stable to point to a reasonably recent and working version, which could be updated without changing every documentation.

[Mario Carneiro]

@Markus Schmaus do you expect lake new to work without an internet connection?

[Mario Carneiro]

if yes, then you have to consider the possibility that the user has stable installed but it's very old

[Markus Schmaus]

If I have an internet connection I would expect lake to figure out the correct version for me.

I'm not so sure what I would expect without internet connection. Probably that lake uses the best version it can find locally, but displays a warning. How does specifying an old nightly help in that case?

[Jon Eugster]

I think it would be reasonable that (by default) lake checks for updates and updates the toolchains stable or nightly if they are used (and if the internet connection works). Is that even possible?

I believe currently it's reasonable to always call

elan toolchain update stable
lake new ...

(or aomething very similar). Would that work for the mathlib docs, too?

[Ruben Van de Velde]

But what if you have a version of lake that doesn't do that yet?

[Jon Eugster]

But that's elan not lake, and elan is able to update itself since almost forever, isn't it?

(I havent actually looked into that, so I might be wrong)