Lean Tutorial Issue

Stream: general

[Mark Morrissey]

Hi, I am a new user excited to get started with Lean! I apologize if this issue is addressed elsewhere but I could not find it.

I am following the Lean installation tutorial. Everything worked from this tutorial page: "Installing Lean and mathlib on Windows". But, on the next stage of the tutorial (titled "Lean Projects",) the 3rd step is to run in Git Bash the following command:
"leanproject get tutorials"
I get this error:
"bash: leanproject: command not found"
I am on Windows 10, using VS Code and Python 3. Thank you for any help or suggestions.

[Patrick Stevens]

Just to check, you did actually run the echo 'PATH="$HOME/.elan/bin:$PATH"' >> "$HOME/.profile" step that is slightly hidden at the end of bullet point 2 of "Installing elan"?

What's the output of ls $HOME/.elan and ls $HOME/.elan/bin?

[Mark Morrissey]

Hi,
Thank you so much for the quick response! I checked and yes I do remember running that command. Here is the output you are asking for: Screenshot-2022-04-22-180846.png

[Patrick Stevens]

Oh, sorry, my response was not actually helpful - I should have asked whether you ran pip3 install mathlibtools correctly, because that's where leanproject comes from.

[Patrick Stevens]

(I would consider running pip3 install mathlibtools again, and then show us what it output when it ran)

[Mark Morrissey]

oh no worries. Actually maybe this was the problem-- I ran 'pip3 install mathlibtools' within a specific conda environment. Apologies as my understanding of package manager is pretty poor. Should I run it in Windows command prompt?

[Mark Morrissey]

Screenshot-2022-04-22-182135.png Screenshot-2022-04-22-182219.png

[Patrick Stevens]

Ah right - in that case you'll need to make sure the Conda venv is activated before you run leanproject

[Mark Morrissey]

My understanding is I have to run leanproject in Git, but I didn't think I could activate a conda environment within Git?

[Patrick Stevens]

(Your alternatives are basically: install it in the Conda environment and then make sure you're inside Conda whenever you run leanproject; install it in a fresh venv and then make sure you're inside that fresh venv whenever you run leanproject; install it globally)

[Patrick Stevens]

Your mental model is slightly askew here. "Git for Windows" is a package which provides "Git Bash" (which is something approximating a Linux-style command line environment, but on Windows) as well as "git" (which is a source control system). The reason you're typing these commands into Git Bash is because that's the most reliable way you can get a Linux-style command line environment on Windows. Git Bash should be enough like a real command line environment that you should be able to source your Conda virtual environment from within it (although I have never tested that).

[Patrick Stevens]

I would try activating the Conda environment from within Git Bash; I'd expect it to work

[Mark Morrissey]

Ahh I just tried activated the environment within Git Bash but it didn't work. Maybe I need different syntax though--I'll look into that now. Would you recommend just installing it globally? Would I be running the install in Git Bash in that case?

[Patrick Stevens]

Installing it globally is the path that the instructions assume, so may well be easier in the long run; I believe it shouldn't matter whether you run pip3 install mathlibtools in Git Bash or your favourite Windows shell such as cmd.exe, although I'm not certain of that, so if you go down the global install route then I'd do it from Git Bash to stick the most closely to the instructions.

What went wrong when you tried activating the conda environment from Git Bash?

[Mark Morrissey]

It said: "bash: conda: command not found"

[Patrick Stevens]

And what shell do you usually run conda from - cmd.exe?

[Patrick Stevens]

If my mental model of your setup is correct, you should be able to activate Conda however you normally do it, and then type leanproject --help in the same shell that you just activated Conda in, and it will Just Work

[Mark Morrissey]

And I just tried to run 'pip3 install mathlibtools' in Git Bash and got 'bash: $'\302\203pip3': command not found' as an error. It seems like I need to install pip3 within Git Bash specifically? And you are right, my mental model of the differences between these environments is definitely off. I am very confused

[Patrick Stevens]

(There will also be some extra configuration when it comes to setting up VS Code if you continue down the conda route - I am leaning towards recommending the global install method)

[Mark Morrissey]

I have a shell called "Anaconda Prompt" that I can just launch on my computer--it is Windows
I just tried leanproject --help in my conda environment and that worked!

[Mark Morrissey]

But I agree it sounds like the global install method may be easier if I can get it to work

[Patrick Stevens]

If you're very lucky, you may find that VS Code Just Works with your current setup - I'd check whether it works out of the box before doing a global install

[Patrick Stevens]

(but I wouldn't spend much time trying to make it work if it doesn't)

[Mark Morrissey]

Can you explain how you'd check if it works? I got it working as far as that first tutorial, but when I moved onto the "Lean Projects" tutorial I ran into the error I first mentioned

[Patrick Stevens]

So you may be able to run leanproject get tutorials from your Conda prompt - I don't know whether that will have git accessible to it, but it may work

[Mark Morrissey]

Screenshot-2022-04-22-184303.png

[Mark Morrissey]

It looks like it did not have git accessible to it unfortunately

[Patrick Stevens]

In that case I would start from scratch, from the very beginning of the instructions, with a global install, ignoring Conda entirely - I am pretty sure there is an extremely short path to victory from your current state, but I am not confident I could find it without actually being at the machine

[Patrick Stevens]

(also I need to go to bed, it's almost midnight for me)

[Mark Morrissey]

Okay thank you so much for all the help, I really do appreciate how quickly you responded to this!

[Mark Morrissey]

My last question would be--any red flags to make sure I uninstall something, etc. before I restart from the beginning?

[Mark Morrissey]

And assuming not, I will get going on the global install now, sounds like we found the issue. Thanks again