Installation problem

Stream: new members

[Raphael Appenzeller]

Hi, I played the NNG and absolutely loved it. So I wanted the real deal and followed the download instructions and downloaded the tutorials. When I run code tutorials, Visual Studio Code opens and I can read 00_first_proof.lean. I get yellow bars and a message Loading... on the right. After about 10 minutes I get Error updating: excessive memory consumption detected and lots of errors. What do I do?

[Alex J. Best]

Did you download the tutorials project using leanproject get?

[Raphael Appenzeller]

Yes.

[Mauricio Collares]

What's your OS and how did you install Lean? I understand you followed the instructions page, just wondering if there's something specific to your situation.

[Raphael Appenzeller]

I use Windows. I used bash.

[Raphael Appenzeller]

My harddrive is somewhat full. Only 8 GB free, but that should be enough, no?

[Raphael Appenzeller]

I already had python, but downloaded bash and VS Code following the guidelines.

[Mauricio Collares]

That sounds right, assuming you installed elan using after installing bash as in the instructions. Can you delete the tutorial folder, re-download it using leanproject get and paste the command output here?

[Mauricio Collares]

There might be a hint in there

[Raphael Appenzeller]

First I get:
grafik.png
on which I just click OK.

[Raphael Appenzeller]

$ leanproject get tutorials
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
git checkout --detach 5bf57407a1db721efa8856c40b31ad50cf4c3f44 # in directory _target/deps/mathlib

[Mauricio Collares]

You can use #backticks if the formatting is getting messed up, but hopefully there's more to the output

[Mauricio Collares]

I don't know how Git for Windows works, but on Linux you have to type "yes" explicitly to authorize a new host. The dialog text might be truncated. You can try typing "yes" on the text box before clicking OK to see if it helps, because this stray text box is very suspicious.

[Raphael Appenzeller]

Thanks so much for your help. This is all the output I get. (both when I just click OK, and when I write yes (appears as ***) in the box.

[Mauricio Collares]

Here's what I get on my Linux machine:

$ leanproject get tutorials
Cloning from git@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: 264090, done.
remote: Counting objects: 100% (79/79), done.
remote: Compressing objects: 100% (28/28), done.
remote: Total 264090 (delta 67), reused 54 (delta 51), pack-reused 264011
Receiving objects: 100% (264090/264090), 141.03 MiB | 8.47 MiB/s, done.
Resolving deltas: 100% (210712/210712), done.
> git checkout --detach 5bf57407a1db721efa8856c40b31ad50cf4c3f44    # in directory _target/deps/mathlib
HEAD is now at 5bf57407a1 chore(category_theory/fin_category): Speed up `as_type_equiv_obj_as_type` (#13298)
Looking for mathlib oleans for 5bf57407a1
  locally...
  remotely...
  Found remote mathlib oleans
Located matching cache
  5bf57407a1: 100%|████████████████████████████████| 66.1M/66.1M [00:18<00:00, 3.70MB/s]
Applying cache
  files extracted: 2353 [00:07, 323.57/s]

[Mauricio Collares]

This last step ("Looking for mathlib oleans...") is missing. You can try to run it separately by running leanproject get-m inside the tutorials folder. Maybe that will give a useful diagnostic message if it fails.

[Kevin Buzzard]

I think the compiled mathlib binaries take up over half a gig nowadays. The problem looks like you have got mathlib but not the compiled binaries (oleans). Doing what Mauricio suggests above is probably a good idea! Sorry it's so hard to install on Windows :-/

[Raphael Appenzeller]

ok, I ran cd tutorials, leanproject get-m. It finished quite quickly, but did not output anything. I am now running code tutorials again, it keeps Loading....

[Mauricio Collares]

Do you now have .olean files, like for example _target/deps/mathlib/src/algebra/abs.olean? What's the output of leanproject --version and leanproject --debug get-m inside the tutorials folder?

[Kevin Buzzard]

Yeah, right now the game is to get half a gig worth of olean files in that _target directory. leanproject get-m didn't output anything? That sounds weird. I don't know about Windows but on Linux you'll always get some kind of helpful output.

[Mauricio Collares]

You said you already had Python installed. Do you have Python 2 or Python 3? I don't know if leanproject supports Python 2 anymore.

[Patrick Massot]

What are you talking about Kevin? Mathlib isn't so big

[Patrick Massot]

Or maybe it became so big

[Patrick Massot]

It seems you're right

[Raphael Appenzeller]

I only have abs.lean, not abs.olean there. There is no result for --debug:
grafik.png

[Mauricio Collares]

I see you have a space in your directory name. There's a small chance leanproject doesn't handle that well, since it's not the sort of thing Linux people (such as myself) think about.

Edit: I just tested it and spaces in directory names are not a problem on Linux, though.

[Raphael Appenzeller]

$ python --version
Python 3.9.2

[Kevin Buzzard]

Patrick Massot said:

It seems you're right

I discovered this because I made a virtual machine to mark my students' projects and I gave it 10 gigs of disc space and then after 20 projects it ran out of disc space!

[Raphael Appenzeller]

I replaced the spaces with _, and reran the suggestions (including leanproject get-m inside tutorials). Still no .olean files in C:\Users\Strichcoder\Documents\Math_and_Science\Lean\tutorials\_target\deps\mathlib\src\algebra

[Kevin Buzzard]

OK here's a curveball suggestion: perhaps somehow the tarball for the relevant mathlib was corrupted? I don't know where the relevant directory is on Windows but somewhere there is a .mathlib directory and in it there might be a file called 5bf57407a1db721efa8856c40b31ad50cf4c3f44.tar.xz (you can check your leanpkg.toml for the git hash of mathlib which you're using but this is the one for the current tutorials file). Remove this and remove _target in your tutorial repo and then try leanproject get-m again?

[Raphael Appenzeller]

Hmm. I found a folder C:\Users\Strichcoder\.mathlib but it only contains a file called url. I unfortunately don't know what my leanpkg.toml is.

[Mauricio Collares]

That's a good suggestion, but while Raphael runs the experiment I have a question: Is it common for git on Windows to not produce any output, as in the above?

[Raphael Appenzeller]

the url file contains a link, https://oleanstorage.azureedge.net/mathlib/ and nothing else.

[Kevin Buzzard]

Yeah that's the right .mathlib directory , at least we now know that you haven't even downloaded the olean files. In the tutorials directory there will be a file called leanpkg.toml which says exactly which version of mathlib you want, but we don't need to worry about that right now, we know you have got no oleans rather than corrupted oleans.

[Mauricio Collares]

I'm tempted to ask you to just close the terminal and re-open it. The authorization prompt might have done something weird to your terminal, because git is definitely supposed to print stuff.

[Raphael Appenzeller]

In tutorials I have leanpkg.path and leanpkg.toml but no leanpkg.html.

[Kevin Buzzard]

Oh sorry, my bad; it's toml. Sorry for adding to the confusion :-( I edited.

[Raphael Appenzeller]

Yes, the authorization prompt might have done something. Since I typed in yes, it has since not appeared anymore when I deleted tutorials and reran leanproject get tutorials.

[Raphael Appenzeller]

But I still get:

Strichcoder@DESKTOP-LSPVCNB MINGW64 ~/Documents/Math_and_Science/Lean
$ leanproject get tutorials
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
> git checkout --detach 5bf57407a1db721efa8856c40b31ad50cf4c3f44    # in directory _target/deps/mathlib

[Kevin Buzzard]

(three ``` not 2). That's it? This is annoying.

[Mauricio Collares]

The lack of an authorization prompt is expected. Git/SSH saves the server fingerprint when you first authorize it. Then subsequent runs check that the fingerprint matches. This is called trust-on-first-use (or TOFU).

[Kevin Buzzard]

Do Windows users usually have this issue with git? No output at all? I think I'm going to shut up now and wait for a Windows power user to come along. Sorry :-(

[Raphael Appenzeller]

Even if it does not help, here the content of lenpkg.toml:

[package]
name = "tuto"
version = "0.1"
lean_version = "leanprover-community/lean:3.42.1"
path = "src/solutions"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5bf57407a1db721efa8856c40b31ad50cf4c3f44"}

[Kevin Buzzard]

Yeah that looks perfect. But do you have the oleans?

[Mauricio Collares]

I wonder if this is again related to the Git security issue. Maybe the subsequent update broke something in Git or Git Bash? I am assuming you installed Git today.

[Raphael Appenzeller]

no oleans in C:\Users\Strichcoder\Documents\Math_and_Science\Lean\tutorials\_target\deps\mathlib\src\algebra

[Mauricio Collares]

One last blind guess. Does it work if you do winpty leanproject get-m? https://github.com/git-for-windows/build-extra/blob/main/ReleaseNotes.md claims some console programs don't work under MinTTY (that is, Git Bash)

[Kevin Buzzard]

I have no idea what shell tools a Windows user has but the manual version of what leanproject get-m is doing is this: (starting in the tutorials directory):

cd _target/deps/mathlib/
wget https://oleanstorage.azureedge.net/mathlib/5bf57407a1db721efa8856c40b31ad50cf4c3f44.tar.xz
tar -xvf 5bf57407a1db721efa8856c40b31ad50cf4c3f44.tar.xz

[Arthur Paulino]

I suspect the absence of feedback from git might be related to the fact that it's being called indirectly by another program.
@Raphael Appenzeller wanna try deleting the _target folder and doing a git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib by hand?

[Kevin Buzzard]

But they seem to have the lean files, it's the oleans which are missing

[Arthur Paulino]

Is leanproject get-m a shortcut for leanproject get-mathlib-cache?

[Raphael Appenzeller]

Deleting _target and running it gives me finally some more info:

$ git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 264145, done.
remote: Counting objects: 100% (94/94), done.
remote: Compressing objects: 100% (66/66), done.
remote: Total 264145 (delta 47), reused 66 (delta 28), pack-reused 264051
Receiving objects: 100% (264145/264145), 140.28 MiB | 11.08 MiB/s, done.
Resolving deltas: 100% (210708/210708), done.
Updating files: 100% (2665/2665), done.

[Raphael Appenzeller]

(still no .oleans though)

[Mauricio Collares]

Right. So it might be the winpty thing in the release notes. I am really curious to know if winpty leanproject get-m works

[Raphael Appenzeller]

wget ... is downloading lots and lots of files..
Kevin Buzzard said:

I have no idea what shell tools a Windows user has but the manual version of what leanproject get-m is doing is this: (starting in the tutorials directory):

cd _target/deps/mathlib/
wget https://oleanstorage.azureedge.net/mathlib/5bf57407a1db721efa8856c40b31ad50cf4c3f44.tar.xz
tar -xvf 5bf57407a1db721efa8856c40b31ad50cf4c3f44.tar.xz

This has worked. I now have .olean files! I will try running VS code.

[Arthur Paulino]

I wonder if Git Bash would have handled it any better

[Mauricio Collares]

This is git bash, I think.

[Raphael Appenzeller]

grafik.png
grafik.png

[Raphael Appenzeller]

I still get the orange bars and the Loading... message which does not disappear. I should see in about 10 mins, if I get all the errors again.

[Raphael Appenzeller]

Yes, i am using Git bash.

[Mauricio Collares]

Out of curiosity, do you remember where you downloaded your Python version from?

[Arthur Paulino]

So there might have been some error message that was hidden from us because the commands were being called indirectly by leanproject (like with the git commands)

[Raphael Appenzeller]

No, I downloaded python a long time ago (~5 years).

[Mauricio Collares]

@Arthur Paulino Yep, that's what the winpty thing is supposed to fix for non-MSYS2 versions of Python. The only thing I don't get is why more people don't hit this bug.

[Raphael Appenzeller]

I still get a lot of errrors.
grafik.png

[Raphael Appenzeller]

grafik.png

[Mauricio Collares]

Awesome! So if it still doesn't work you should probably delete the tutorials folder and start afresh with winpty leanproject get tutorials

[Raphael Appenzeller]

Mauricio Collares said:

I wonder if this is again related to the Git security issue. Maybe the subsequent update broke something in Git or Git Bash? I am assuming you installed Git today.

I installed Git yesterday, yes.

[Arthur Paulino]

Raphael Appenzeller said:

No, I downloaded python a long time ago (~5 years).

How come is your Python installation so old? 3.9 is not 5 years old
Raphael Appenzeller said:

$ python --version
Python 3.9.2

[Raphael Appenzeller]

I probably updated it over the years. I just don't remember where I originally got it from.

[Raphael Appenzeller]

omg, it works! First green messages:
grafik.png

[Raphael Appenzeller]

Thank you so much. I deleted tutorials and ran winpty leanproject get tutorials. Is this a bug with git? So whenever I need to run leanproject ... I will just write winpty leanproject ... from now on?

[Raphael Appenzeller]

Thank you everyone for helping me so much!

[Mauricio Collares]

It's a bad interaction between Git Bash (MinTTY) and your non-MSYS version of Python. Very roughly (and probably very inaccurately), compiling with MSYS2 replaces some Unix functions with their Windows counterparts, including terminal ones. MinTTY does not emulate Unix terminals because it expects programs to use Windows terminal APIs via MSYS. This assumption is broken by your version of Python.

[Mauricio Collares]

And yes, if you want to run any Python program (including leanproject) in Git Bash, you should either use winpty or switch to a different Python build.

[Arthur Paulino]

(thank god we're moving further away from Python dependencies with Lean 4)

[Henrik Böving]

Introducing C dependencies /o\ :P

[Bryan Gin-ge Chen]

Is this something that we could detect in leanproject (to e.g. output a helpful message)?

[Mauricio Collares]

If anyone is wondering why extracting the oleans by hand didn't work, it's probably because leanpkg configure needed to be ran on the fresh checkout first

[Mauricio Collares]

Apparently, stdin is not a TTY in the broken configuration. So it seems like something that could be detected, yes.

[Mauricio Collares]

Relatedly, is there any reason why Git Bash is recommended over, say, PowerShell?

[Arthur Paulino]

Does PowerShell come with Windows? Maybe Git bash is recommended because, if I recall correctly, it comes with Git on Windows installations

[Eric Wieser]

Is this something leanproject even deals with directly, or is detecting it GitPython's problem?

[Mauricio Collares]

The only thing that's specific to the cache step is the use of tqdm, I think. It could be worth disabling it if sys.stderr.isatty() is False.

[Nathan Temple]

Can anyone diagnose what is going wrong with my installation based on the screenprint:

image.png

[Eric Rodriguez]

what version of Lean are you hoping to use?

[Nathan Temple]

Lean 3

[Kevin Buzzard]

Do you have a Lean 3 project open? (I can't tell because everything is folded up in your file explorer). Do you have the Lean 3 extension installed in VS Code?