## Stream: new members

### Topic: Trouble using compiling a lean package

#### Calle Sönne (Nov 17 2018 at 16:15):

Im trying compile a leanpackage. I assume the way you do is by running leanpkg build in the folder where leanpkg.toml is located. However doing that gives me the following error:

error: override toolchain 'master' is not installed
info: caused by: the toolchain file at '/home/calle/herstein/leanpkg.toml' specifies an uninstalled toolchain

I have tried running leanpkg build, leanpkg init, leanpkg .configure. All of them give the same error (even just running "lean" within the folder gives same error). Other than this lean is working fine and I can use/work on other packages.

Here is the leanpkg.toml file if that explains anything:

[package]
name = "herstein"
version = "0.1"
lean_version = "master"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", rev = "c7c0d2a1bb2f0ba353bbcb0510352a25c80fc186"}

#### Johan Commelin (Nov 17 2018 at 16:20):

Hi @Calle Sönne Are you using elan? Which OS are you on?

#### Kevin Buzzard (Nov 17 2018 at 17:38):

He is using elan, it's on Windows, he showed me this on Thursday and I had no idea. Just running leanpkg by itself with no parameters gave this error

#### Kenny Lau (Nov 17 2018 at 17:39):

and lean is funded by microsoft lmao

#### Kevin Buzzard (Nov 17 2018 at 17:40):

I'm funded by Imperial College but that doesn't mean that the "official" website they insist on generating for me bears any relation to what I have been doing over the last 10 years. Big organizations are complex things Kenny.

what, this one?

#### Calle Sönne (Nov 17 2018 at 17:44):

Im using linux (Manjaro)

#### Reid Barton (Nov 17 2018 at 17:46):

Is lean_version = "master" supposed to work?

#### Kevin Buzzard (Nov 17 2018 at 17:47):

what, this one?

Yes. It's auto-generated you know! The script was written in about 2004.

#### Calle Sönne (Nov 17 2018 at 17:47):

Im using elan version 0.7.1 and lean version 3.4.2 nightly-2018-11-13

#### Reid Barton (Nov 17 2018 at 17:48):

I would put one of those version numbers in the lean_version field then.

#### Reid Barton (Nov 17 2018 at 17:48):

elan uses that field to decide which lean to invoke and I don't think it understands "master"

#### Kevin Buzzard (Nov 17 2018 at 17:48):

Try lean_version = "nightly-2018-11-13"

#### Kevin Buzzard (Nov 17 2018 at 17:49):

(in leanpkg.toml)

#### Kevin Buzzard (Nov 17 2018 at 17:50):

I see, so this is the issue. I've never used elan and I didn't understand the error. The job of elan is to ensure that the version of Lean coincides with the version used by the package. This will be an issue in future when Lean 4 hits. But it never bites me now because every package I know of uses Lean 3.4.1 or some nightly after 3.4.1 which is basically the same as 3.4.1 but with some minor irrelevant bugfix

#### Calle Sönne (Nov 17 2018 at 17:50):

That did it :) Thank you

#### Kevin Buzzard (Nov 17 2018 at 17:50):

:-)

Last updated: May 15 2021 at 23:13 UTC