Issue of Installation on generic Linux

Stream: new members

[Kunhao Zheng]

Hi! I am a beginner in Lean and currently I've been stuck in the installation step of tutorial. When I open the folder tutorials/src in VSCode, it seems that there is something goes wrong on the line import tactic.suggest from mathlib

invalid import: data.option.defs
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold).

Here is my terminal log when getting the tutorials, is it the problem that lies in the last line?

~$ leanproject get tutorials
Cloning from git@github.com:leanprover-community/tutorials.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/tutorials.git
configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 154181, done.
remote: Counting objects: 100% (404/404), done.
remote: Compressing objects: 100% (272/272), done.
remote: Total 154181 (delta 264), reused 176 (delta 132), pack-reused 153777
Receiving objects: 100% (154181/154181), 66.03 MiB | 1.15 MiB/s, done.
Resolving deltas: 100% (121330/121330), done.
> git checkout --detach 95260613e481c2571df45c3961d491821f147dd8    # in directory _target/deps/mathlib
HEAD is now at 95260613e feat(data/nat/fib): add a strict monotonicity lemma. (#7317)
Looking for local mathlib oleans
Found local mathlib oleans
Unknown archive format '/home/kuu/.mathlib/95260613e481c2571df45c3961d491821f147dd8.tar.xz'

[Ruben Van de Velde]

Hmm, need to update your leanproject?

[Bryan Gin-ge Chen]

What version of Python are you using? I think you need Python 3.5 (?) or above to extract the .tar.xz format.

[Ruben Van de Velde]

Yeah, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanupdate.20cant.20install.20olean.20files suggests this is a python issue, indeed

[Patrick Massot]

Kunhao Zheng said:

When I open the folder tutorials/src in VSCode

Independently of your extraction issue, note you're not meant to open tutorials/src but tutorials

[Kunhao Zheng]

Ruben Van de Velde said:

Yeah, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanupdate.20cant.20install.20olean.20files suggests this is a python issue, indeed

Thank you for your hint! I am using Python 3.8.8 and I found my shutil works well as mentioned in the stream that you quote. No idea of how to tackle this issue.

[Kevin Buzzard]

If you run python --version and python3 --version and leanproject --version on the command line what do you get?

[Kunhao Zheng]

~/tutorials$ python --version
Python 3.8.5
~/tutorials$ python3 --version
Python 3.8.8
~/tutorials$ leanproject --version
leanproject, version 1.0.0

Strange that in interactive command line, my python3 will error when I try to import "lzma" but python won't, while both works fine when I try import shutil.

[Kevin Buzzard]

so probably that's the problem

[Kevin Buzzard]

I think that leanproject uses python3 under the hood. You could temporarily rename python3 to python388 and python to python3 and see if you get away with it?

[Eric Wieser]

If you have multiple python installations, you can specify which one to use for leanproject with python3 -m mathlibtools.leanproject the_rest_of_the_command

[Eric Wieser]

Kevin Buzzard said:

I think that leanproject uses python3 under the hood.

leanproject uses whichevery python you installed it with under the hood. Did you install with pip or pip3? What dopip --version and pip3 --version print?

[Kunhao Zheng]

pip --version and pip3 --version both print pip21.1. I tried the alias trick in my .bashrc but I didn't get away that.

[Kunhao Zheng]

Eric Wieser said:

If you have multiple python installations, you can specify which one to use for leanproject with python3 -m mathlibtools.leanproject the_rest_of_the_command

Specifying which python to use solve the "Unknown archive format" problem, many thanks!

[Eric Wieser]

pip --version and pip3 --version both print pip21.1

Don't they also print a python version?

[Kunhao Zheng]

kuu@DESKTOP-UGBCO1R:~/tutorials$ pip --version
pip 21.1 from /home/kuu/.local/lib/python3.8/site-packages/pip (python 3.8)
kuu@DESKTOP-UGBCO1R:~/tutorials$ pip3 --version
pip 21.1 from /home/kuu/.local/lib/python3.8/site-packages/pip (python 3.8)

like this.

[Eric Wieser]

Oh, interesting that it doesn't show the build version

[Eric Wieser]

What about which python and which python3?

[Kunhao Zheng]

In fact I think it's which python3. One of my python3 is built from source and at that time I didn't have lzma installed in my system, so maybe after my configure and make, the python3 built will error when I try to import lzma, while another version is installed directly from binary. And leanproject uses the one that I built from source, and it's thus not happy. That's probably what I can think about