Mathematics in Lean

Stream: new members

[Patrick Steele]

I'm trying to work through Mathematics in Lean, but I'm encountering errors in... the standard library? I'm getting

./.lake/packages/mathlib/././Mathlib/Tactic/Clean.lean:32:12: error: unknown identifier 'letFunAnnotation?'

Do I have an old standard library? Too _new_ a standard library?

[Patrick Massot]

This should never be an issue. How did you get Mathematics in Lean? What did you do exactly?

[Kyle Miller]

That looks like you have the nightly Lean version somehow, rather than the one Mathematics in Lean wants.

[Patrick Steele]

nightly

Yes, I built from source. I'm currently rebuilding from v4.4.0-rc1.

[Eric Wieser]

Building (lean?) from source is going to be a very unpleasant and long experience, as you almost certainly won't be able to/want to use lake exe cache get

[Patrick Steele]

I got "Mathematics in Lean" by cloning https://github.com/leanprover-community/mathematics_in_lean, and lean itself (and lake, etc) by building from source. I'm somewhat willing to pay the pain of building it.

[Patrick Steele]

that said, I don't even know what lake exe cache get does, aside from making assumptions based on the words

[Patrick Massot]

You should have prefaced your question with your masochistic assertion.

[Patrick Massot]

I wasted time cloning the current version of Mathematics in Lean and getting the cache because you didn't say from the beginning that you chose to ignore instructions and "pay the pain".

[Patrick Steele]

I'm sorry about that.

[Patrick Massot]

Anyway, the answer to your question is: this way of using Lean isn't supported, I'm afraid you will have to solve your issue by yourself or follow installation instructions.

[Patrick Steele]

Sounds good.

[Patrick Steele]

Thanks

[Kyle Miller]

Once you have a working MIL and have gone through it, feel free to compile Lean then (and only then) if you are interested in developing Lean itself. Generally, nobody builds Lean from source for downstream projects. Even I use pre-built binaries for Mathlib development rather than building my own, even though I have my own local builds of Lean for Lean development.

[Kyle Miller]

There are some times that pain worth paying for, but I'd say this isn't one of those times :-)

[Patrick Steele]

I expected my original question to be on the same level as a Python learner asking about print needing or not needing parenthesis, which is why I asked. That is, something simple like "specify a different stdlib version."

[Patrick Steele]

The good news is that the build just finished, and I now see goals and givens, as opposed to errors

[Kyle Miller]

If you want to know the details, the problem is that your Lean was so new that there isn't even an updated mathlib yet. When the next Lean release is made, mathlib will be updated to account for the following change, among others. https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/408573423

[Kyle Miller]

When you come across a Lean project, pay special attention to the lean-toolchain file: https://github.com/leanprover-community/mathematics_in_lean/blob/master/lean-toolchain

[Patrick Steele]

Yes, that makes sense. I'd not entirely internalized that lean didn't ship with (what I've been calling) a standard library.

[Kyle Miller]

(Patrick is one of the authors of Mathematics in Lean by the way, so I don't need to reiterate that it's also worth paying special attention to instructions, to at least make sure that following the instructions works before trying a custom setup.)

[Eric Wieser]

Patrick Steele said:

that said, I don't even know what lake exe cache get does, aside from making assumptions based on the words

It downloads pre-built "binaries" for the mathlib library, to save users a few hours of compilation every time mathlib updates

[Patrick Steele]

(In far more detail than anyone cares about, I use Nix, and the lean4 Github repo had a flake.nix file, so I did what seemed natural and just pointed nix at it. That seemed to work fine, giving me lean and lake and so on.)

[Patrick Steele]

(pinning that to a tagged release was how I made progress.)

[Eric Wieser]

But the binaries are cached based on the exact version of Lean you built, so if you build things from source it's very easy to get a cache miss

[Patrick Steele]

Yes, this all makes sense. Thanks everyone, and sorry for derailing you all.

[Eric Wieser]

Patrick Steele said:

I got "Mathematics in Lean" by cloning https://github.com/leanprover-community/mathematics_in_lean, and lean itself (and lake, etc) by building from source. I'm somewhat willing to pay the pain of building it.

Note that Lake will ignore your wishes and download pre-built binaries for ProofWidgets rather than building them from source, so it will be challenging to achieve your goal of "build everything from source"

[Eric Wieser]

(and even for Std and Mathlib, it will download a fresh copy of the source rather than using your copy of the source)

[Patrick Steele]

Noted, thanks.