cannot build tutorials

Stream: new members

[ZJ Xoe]

Hello all, I want to start learning lean from the tutorials. I'm using arch linux so I install python-mathlibtools, lean-community-bin and get the tutorials by leanproject get tutorials, but I fail to build it by leanproject build

[Kevin Buzzard]

What's the error?

[ZJ Xoe]

Kevin Buzzard said:

What's the error?

something like "notation" already define, manually install lean-community 3.46(3.48 default) solve this.

[Mauricio Collares]

That will probably be fixed by https://github.com/leanprover-community/tutorials/pull/49

[Patrick Massot]

This would be fixed by following installation instructions.

[Patrick Massot]

I don't know anything about arch linux, but ZJ Xoe is clearly not using the recommended setup. I don't want to blame, only point out that fighting the software toolchain will only bring pain.

[Mauricio Collares]

That's true. @ZJ Xoe, what do you mean by "3.48 default"? If you installed a particular version of Lean using your package manager, note that using elan to manage your lean installations will solve this and a bunch of other problems you might encounter in the future. On Arch, this means removing the lean-community-bin package and installing the elan-init package from the AUR.

[Patrick Massot]

A quick search confirms what I feared: whoever is providing https://aur.archlinux.org/packages/lean-community-bin is simply actively hostile to users. There is only one supported way to use lean 3, going through elan to manage Lean versions. Encouraging people to do something else is sadistic.

[Patrick Massot]

Using such a package is fine if you want to build your lean library from the core library without any interaction with anyone else, especially without mathlib.

[Patrick Massot]

If anyone knows arch linux, is there a way to know who is hiding behind the pseudonym fanninpm?

[Eric Wieser]

Their email address at miamioh.edu reveals them to be Padraic Fanning

[Eric Wieser]

(wow, "Miami University, Oxford, Ohio" is a really weird address)

[Patrick Massot]

Where did you find that email address?

[Eric Wieser]

Github

[Patrick Massot]

How did you find the relevant GitHub account?

[Patrick Massot]

Did you simply tried the same pseudonym?

[Mauricio Collares]

It's also in the PKGBUILD file for lean-community-bin: https://aur.archlinux.org/cgit/aur.git/tree/PKGBUILD?h=lean-community-bin

[Eric Wieser]

Guessed based on username collision alone I'm afraid

[Patrick Massot]

https://aur.archlinux.org/cgit/aur.git/tree/PKGBUILD?h=lean-community-bin is indeed very useful, thanks Mauricio

[Patrick Massot]

What is crazy is this person seems to not even have an account here on the Lean Zulip.

[Eric Wieser]

Not to be confused with https://aur.archlinux.org/cgit/aur.git/tree/PKGBUILD?h=lean-community which seems to publish something equally misleading

[Eric Wieser]

(found by looking at the "conflicts" field)

[Patrick Massot]

It would be great if someone with better diplomacy skills than me could write them an email.

[Eric Wieser]

I'm not sure there's much to be done here; I think it's totally ok for package managers to decide to distribute fixed versions of lean, just in case some crazy person wants to write a command-line tool in lean itself that uses a specific version; it's just totally incompatible with how we as a community do things.

It feels a bit like package managers providing Python packages; most users just use pip instead, but if you're going to publish your own code on the package manager then you have to switch to their world.

[Eric Wieser]

Certainly we could ask for a warning message to be added to the description of the package, but I have no idea whether archlinux users would actually see that message anyway

[ZJ Xoe]

Patrick Massot said:

I don't know anything about arch linux, but ZJ Xoe is clearly not using the recommended setup. I don't want to blame, only point out that fighting the software toolchain will only bring pain.

I have no intend to fight with the toolchains, I just search 'lean' in AUR and this package looks like what I want because the tutorial project didn't mention anything about elan. Anyway, I will use elan now.

[Patrick Massot]

The readme from the tutorials repo links to installation instructions, this is what you missed.

[ZJ Xoe]

Mauricio Collares said:

That's true. ZJ Xoe, what do you mean by "3.48 default"? If you installed a particular version of Lean using your package manager, note that using elan to manage your lean installations will solve this and a bunch of other problems you might encounter in the future. On Arch, this means removing the lean-community-bin package and installing the elan-init package from the AUR.

Thank you, this pull do fix the problem. AUR generally use the latest version, so it's 3.48 in this case, and I change PKGBUILD to use 3.46.

[Patrick Massot]

I'm afraid you still don't understand: you mustn't handle versions yourself, this will only bring pain.

[Patrick Massot]

You simply need to uninstall everything Lean related that you got from AUR and follow generic linux installation instructions. Someone who is probably very nice and probably wants to do nice thing for other people simply horribly failed and set traps all over the AUR package system.

[Eric Wieser]

I suspect you can safely install elan (and only elan) from AUR, but that might be a bad idea too.

[Mauricio Collares]

Can leanproject detect mismatched lean versions and print a warning? I can imagine standalone projects not using elan or leanpkg.toml, but they wouldn't use leanproject either.

[Eric Wieser]

Are you missing a negative there?Thanks!

[Eric Wieser]

lean itself already reads the leanpkg.toml; it should definitely emit a warning if the version mismatches

[Eric Wieser]

But I guess that won't help with old lean binaries!

[ZJ Xoe]

Patrick Massot said:

You simply need to uninstall everything Lean related that you got from AUR and follow generic linux installation instructions. Someone who is probably very nice and probably wants to do nice thing for other people simply horribly failed and set traps all over the AUR package system.

Ya I know, I'm going to install elan. The behavior of "handle versions myself" occurs before I know elan.

[Patrick Massot]

Yes, installing elan and only elan should be safe. But it's also not much easier than installing it by hand.