Zulip Chat Archive

Stream: new members

Topic: Trouble using compiling a lean package


view this post on Zulip 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"}

view this post on Zulip Johan Commelin (Nov 17 2018 at 16:20):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 17 2018 at 17:39):

and lean is funded by microsoft lmao

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 17 2018 at 17:42):

what, this one?

view this post on Zulip Calle Sönne (Nov 17 2018 at 17:44):

Im using linux (Manjaro)

view this post on Zulip Reid Barton (Nov 17 2018 at 17:46):

Is lean_version = "master" supposed to work?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 17 2018 at 17:48):

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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 17:48):

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

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 17:49):

(in leanpkg.toml)

view this post on Zulip 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

view this post on Zulip Calle Sönne (Nov 17 2018 at 17:50):

That did it :) Thank you

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 17:50):

:-)


Last updated: May 15 2021 at 23:13 UTC