Trouble using compiling a lean package

Stream: new members

[Calle Sönne]

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]

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

[Kevin Buzzard]

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]

and lean is funded by microsoft lmao

[Kevin Buzzard]

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.

[Kenny Lau]

what, this one?

[Calle Sönne]

Im using linux (Manjaro)

[Reid Barton]

Is lean_version = "master" supposed to work?

[Kevin Buzzard]

what, this one?

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

[Calle Sönne]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(in leanpkg.toml)

[Kevin Buzzard]

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]

That did it :) Thank you

[Kevin Buzzard]

:-)