How do I setup Mathlib for my current toolchain?

Stream: new members

[R Dong]

I created a new project using Lean 4.15.0, and I set up mathlib dependency as so:

require "leanprover-community" / "mathlib" @ git "releases/v4.15.0"

However, when I try to lean update, I get this kind of compile error:

info: state_reduction: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib'
trace: .> git clone https://github.com/leanprover-community/mathlib4 ././.lake/packages/mathlib
trace: stderr:
Cloning into '././.lake/packages/mathlib'...
Updating files: 100% (6086/6086), done.
trace: ././.lake/packages/mathlib> git checkout --detach e9ae2a61ef5c99d6edac84f0d04f6324c5d97f67 --
trace: stderr:
HEAD is now at e9ae2a61ef chore: disable docPrime linter (#20559)
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
trace: .> git clone https://github.com/leanprover-community/batteries ././.lake/packages/batteries
trace: stderr:
Cloning into '././.lake/packages/batteries'...
trace: ././.lake/packages/batteries> git checkout --detach e8dc5fc16c625fc4fe08f42d625523275ddbbb4b --
trace: stderr:
HEAD is now at e8dc5fc1 chore: bump toolchain to v4.15.0 (#1080)
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
trace: .> git clone https://github.com/leanprover-community/quote4 ././.lake/packages/Qq
trace: stderr:
Cloning into '././.lake/packages/Qq'...
trace: ././.lake/packages/Qq> git checkout --detach f0c584bcb14c5adfb53079781eeea75b26ebbd32 --
trace: stderr:
HEAD is now at f0c584b chore: bump toolchain to v4.15.0 (#66)
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
trace: .> git clone https://github.com/leanprover-community/aesop ././.lake/packages/aesop
trace: stderr:
Cloning into '././.lake/packages/aesop'...
trace: ././.lake/packages/aesop> git checkout --detach 2689851f387bb2cef351e6825fe94a56a304ca13 --
trace: stderr:
HEAD is now at 2689851 chore: bump toolchain to v4.15.0 (#187)
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
trace: .> git clone https://github.com/leanprover-community/ProofWidgets4 ././.lake/packages/proofwidgets
trace: stderr:
Cloning into '././.lake/packages/proofwidgets'...
trace: ././.lake/packages/proofwidgets> git checkout --detach 2b000e02d50394af68cfb4770a291113d94801b5 --
trace: stderr:
HEAD is now at 2b000e0 update
error: ././.lake/packages/proofwidgets/lakefile.lean:20:20: error: invalid argument name 'text' for function 'Lake.buildFileAfterDep'
error: ././.lake/packages/proofwidgets/lakefile.lean:46:2: error: invalid field 'afterBuildCacheAsync', the environment does not contain 'Lake.Package.afterBuildCacheAsync'
  pkg
has type
  Package
error: ././.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

What should I do to fix this?

[Kevin Buzzard]

Are you using a lakefile.lean or a lakefile.toml? In the FLT lakefile.lean I have

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"

(at least on the branch I'm on -- main is now on 4.16-rc2)

[R Dong]

lakefile.lean. I'll give it a try

[R Dong]

Same error

[Kevin Buzzard]

I think you need to post your full lakefille.lean so that we get to see all the other things you put in it

[R Dong]

import Lake
open Lake DSL

package "test_lean" where
  -- add package configuration options here

lean_lib «TestLean» where
  -- add library configuration options here

@[default_target]
lean_exe "test_lean" where
  root := `Main

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"

It's straight from template, plus the mathlib

[Ruben Van de Velde]

What's in your lean-toolchain?

[R Dong]

No such file

[Ruben Van de Velde]

Try creating one in the root of your project, containing leanprover/lean4:v4.15.0

[R Dong]

Same error

[Kevin Buzzard]

How did you create this project? Which instructions did you follow? lake new foobar math is the way to create a project called foobar depending on mathlib. And what do you mean by lean update above? That's not a thing.

[Kevin Buzzard]

Looking at the differences between the lakefiles, I have

@[default_target]
lean_lib «Foobar» where

instead of what you have. But my understanding of lake is poor.

[R Dong]

lake new <> math gives me 4.16, which I don't have

[R Dong]

Also, same error. I didn't mean lean update, but lean exe get cached as instructed by Mathlib wiki

[Kevin Buzzard]

Do you have elan? Elan should just be automatically downloading whichever version of lean you need

[R Dong]

I do not have elan on this machine

[R Dong]

Oh wait, I just realized my Lean version is not 4.15, but 4.11

[Sebastian Ullrich]

That is why you should be using elan :)

[R Dong]

Well, I would certainly hope the dependency solver takes into account of the current version

[Ruben Van de Velde]

That's what elan and lean-toolchain are for