installing mathlib

Stream: general

[Bill Thomson]

Hi, I'm a newcomer. I just successfully installed Lean following this youtube video (https://www.youtube.com/watch?v=2f_9Zetekd8&t=4s) . But when I try to install mathlib from https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md , it failed...

[Bill Thomson]

curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

doesn't work..

[Mario Carneiro]

error msg?

[Mario Carneiro]

the update-mathlib step is optional, but you need to get python first if you want to do it

[Scott Morrison]

remote-install-update-mathlib actually attempts to install python too, if it can't find it

[Scott Morrison]

But I'm not sure how thoroughly tested on windows it is.

[Scott Morrison]

One simple thing to make sure of is that you're running that command inside a suitable shell (e.g. the git for windows bash shell you installed during the video, and not a standard windows cmd prompt).

[Scott Morrison]

Beyond that, you'll have to tell us the error message!

[Bill Thomson]

pasted image

[Mario Carneiro]

looks like python wasn't found

[Bill Thomson]

i have installed python already. i double clicked into git-bash, and run the command curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash. This is the error message, saying i havent installed python...

[Mario Carneiro]

does python at the prompt work?

[Mario Carneiro]

or python3

[Mario Carneiro]

if it just sits there hit ctrl-c to quit and try python --version

[Mario Carneiro]

on my machine python --version reports Python 3.6.2 but python3 doesn't exist

[Bill Thomson]

excuse me, where do i type python --version ?

[Mario Carneiro]

at the prompt

[Mario Carneiro]

of the command line

[Bill Thomson]

i think the python at the prompt works

[Bill Thomson]

it can calculate 1+2 lol

[Mario Carneiro]

I recommend skipping the update-mathlib script, unless @Simon Hudon can fly in to save the day. It's not that well tested and it's not required to set up lean or mathlib

[Bill Thomson]

ok, so what command should i type in mingw64 to install mathlib?

[Mario Carneiro]

does lean --version work?

[Bill Thomson]

yes, it says Lean (version 3.4.2, commit cbd2b6686ddb, Release)

[Mario Carneiro]

You should create a folder to put your project in, then navigate to it in mingw using cd /c/Users/Bill/projects/my_project or wherever you decide to put it, and then run leanpkg new my_project

[Mario Carneiro]

I forget the command to add mathlib, someone will correct me, but I think it is leanpkg add leanprover-community/mathlib

[Bill Thomson]

pasted image

[Bill Thomson]

it now seems to be working! thanks a lot!!

[Mario Carneiro]

you should also run cd _target/mathlib/src and then lean --make at your convenience (it will take a while), so that vscode lean startup doesn't take ages

[Bill Thomson]

OK!

[Patrick Massot]

I recommend skipping the update-mathlib script, unless Simon Hudon can fly in to save the day. It's not that well tested and it's not required to set up lean or mathlib

I really disagree. I think update-mathlib is a very important part of the setup for almost every users. We simply need someone with Windows access to put more put efforts into getting a streamlined installation process.

[Bill Thomson]

what does update-mathlib do in practise actually?

[Scott Morrison]

update-mathlib grabs the latest precompiled version of mathlib, so you don't have to sit there for an hour while your computer compiles it

[Scott Morrison]

Can you verify for me that you are running python --version inside the git bash terminal? (That is, not the default windows terminal.)

[Scott Morrison]

You talked above about using the mingw64 terminal. I'm not a windows user so I'm not absolutely sure what that is, but my understanding is that it's very important you do everything in the same type of terminal, and probably that should be the git-bash terminal that you acquired by installing "git for windows".

[Neil Strickland]

The problem is that git bash under Windows does not give you a proper framework for installing additional packages such as python. I have installed MSYS, and python and git under MSYS, and switched VS Code to use MSYS instead of git bash, and now most things seem to work correctly. It would probably also work to stick with git bash but arrange for the PATH variable used by git bash to be set so that python can be found elsewhere. But I am not sure exactly where git bash gets its PATH from. Anyway, the current installation instructions are certainly not satisfactory if you want to have update-mathlib. It would be ideal if we could update my one-click installer to include python etc, and arrange for better integration with the rest of the ecosystem. I will try to do that if I can find time.

[Bill Thomson]

pasted image

Yes, i have been using the git-bash terminal. And the python seems to have a little problem: I think i misundertood something previously

[Bill Thomson]

you should also run cd _target/mathlib/src and then lean --make at your convenience (it will take a while), so that vscode lean startup doesn't take ages

@Mario Carneiro I think you meant cd_target/deps/mathlib/src. And inside this folder, I already see lots of folders and .lean files already. When I run lean --make, I see .olean files start poping up. Is this normal?

[Mario Carneiro]

yes, those are the build files

[Bill Thomson]

btw, how can I see the tactic state in VS code?

[Patrick Massot]

It should open automatically when you open a .lean file. If not then you can press Ctrl-Shift-Enter.

[Floris van Doorn]

I've been helping a lot of people getting the update-mathlib script recently, also on Windows. I will PR more detailed instructions soon.

[Floris van Doorn]

• Figure out where Python is installed (one option is to search for python in Start -> right click python -> open file location -> right click python -> open file location (you have to do it twice because the first one is a shortcut))
• To get python working on the command line, make sure you have both \path\to\python and \path\to\python\Scripts in your Windows PATH variable (google to find instructions how to do that)
• This probably doesn't give you the python3, because for some reason, python on windows doesn't give you python3 as an command. You can either rename python.exe to python3.exe or make a copy called python3.exe or add alias python3='python' to your ~/.bashrc file (I don't know which method is preferred)
• Now which python3 and which pip3 and python3 --version should all be working (if you used alias then which python3 doesn't work, which is fine as long as python3 --version works). On some machines pip3 --version was not working (it did not return the version number, but quit silently). If this is the case try running python3 -m pip install --upgrade pip. Then pip3 --version should also work
• After all this curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash should be working.