## Stream: maths

### Topic: MathLib installing

#### Nicholas McConnell (Feb 16 2020 at 05:06):

I'm having a bit of an issue installing mathlib. For many years I have already had Python 2, but I installed Python 3 for mathlib sake. In https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md it says I need to type "which python" in Git Bash, with the App Installers turned off in 'Manage App Execution Aliases'. When I do that it still says "/c/Users/nicho/AppData/Local/Microsoft/WindowsApps/python" in the terminal. (Either that or "no python found".) Please let me know what to do as soon as possible. I have an important project due on March 4 and it's important I have enough time after installing mathlib to work out the mathematics.

#### Mario Carneiro (Feb 16 2020 at 05:07):

You don't need python for mathlib to work

#### Nicholas McConnell (Feb 16 2020 at 05:07):

I'm intrigued, doesn't the website say I do...

#### Mario Carneiro (Feb 16 2020 at 05:07):

it helps with some of the tooling, but nothing essential for functioning

#### Mario Carneiro (Feb 16 2020 at 05:08):

Do you have lean? You can create a project, add a mathlib dependency, and then leanpkg will download it for you

#### Mario Carneiro (Feb 16 2020 at 05:08):

You may have to compile it yourself and this takes a while, but not more than an hour

#### Mario Carneiro (Feb 16 2020 at 05:08):

the python is to help with this part

#### Nicholas McConnell (Feb 16 2020 at 05:09):

Alright, I'll do that tomorrow, it's really late for me

#### Nicholas McConnell (Feb 16 2020 at 05:09):

Thanks for the help

#### Sebastien Gouezel (Feb 16 2020 at 08:47):

@Patrick Massot , it is maybe time to put your all-in-one zip file with mathlib and vscode for windows somewhere, together with a link at the first line of the windows installation instructions, explaining that if you just want to try Lean and mathlib this is by far the simplest option?

#### Patrick Massot (Feb 16 2020 at 17:26):

Yes, I was waiting for the GitHub action transition to settle down, but I guess now it's ready.

#### Patrick Massot (Feb 16 2020 at 19:35):

I've done a bit a research about this idea. Clearly there is no way we can distribute VScode while respecting the license. So we'll need to use https://github.com/VSCodium/vscodium which is a free binary release of VScode (yes, Microsoft's open sourcing is weird). The next step is to install the extension and I immediately hit a bug. I'll wait a bit to see whether this bug could be fixed quickly, but most probably we'll need a hack to install the extension. @Gabriel Ebner how hard would it be for you to also release a version of the VScode extension that could simply be copied in the state the installation procedure creates?

#### Gabriel Ebner (Feb 16 2020 at 19:38):

Can't you just extract the .vsix file? (click "download extension" here). The vsix file is just a zip file. AFAICT it contains exactly the same directory structure as ~/.vscode/extensions/jroesch.lean-0.14.11/ on my machine.

#### Patrick Massot (Feb 16 2020 at 19:40):

I'm looking for a link I could actually follow from a script.

#### Patrick Massot (Feb 16 2020 at 19:41):

I would prefer not to use selenium to download our own extension...

#### Gabriel Ebner (Feb 16 2020 at 19:44):

git clone https://github.com/leanprover/vscode-lean
cd vscode-lean
npm i
./node_modules/.bin/vsce package
ls *.vsix       # voilà


#### Patrick Massot (Feb 16 2020 at 19:45):

Doing that for every mathlib nightly feels a bit silly, right? Why not doing it as part of your release workflow and have the vsix file as a GitHub artefact somewhere?

#### Gabriel Ebner (Feb 16 2020 at 19:49):

I'll see what I can do. Don't hold your breath though.

Nice!

#### Nicholas McConnell (Feb 17 2020 at 03:31):

In Git Bash, "update-mathlib" responds with "command not found", and "source ~/.profile" didn't work either

#### Mario Carneiro (Feb 17 2020 at 03:33):

you did the first three lines before update-mathlib?

#### Mario Carneiro (Feb 17 2020 at 03:34):

do lean and leanpkg work?

#### Nicholas McConnell (Feb 17 2020 at 03:35):

Yeah, and leanpkg works

#### Mario Carneiro (Feb 17 2020 at 03:37):

That's fine. Go to my_project/_target/mathlib and then lean --make src and go get a coffee (or dinner)

#### Mario Carneiro (Feb 17 2020 at 03:38):

Alternatively, download the compiled olean files from https://github.com/leanprover-community/mathlib-nightly/releases and unzip them to the _target/mathlib folder

#### Mario Carneiro (Feb 17 2020 at 03:40):

If all goes well, you should be able to put import data.real.basic in a lean file in the project and vscode should be happy with it after waiting a few seconds. If it takes longer than that something may have gone wrong with the compile

#### Mario Carneiro (Feb 17 2020 at 03:41):

Alternatively, if anyone wants to diagnose installing python on windows be my guest

#### Nicholas McConnell (Feb 17 2020 at 03:45):

Alright, I've unzipped the tar

#### Nicholas McConnell (Feb 17 2020 at 03:45):

But "import tactic" still doesn't work

#### Nicholas McConnell (Feb 17 2020 at 03:46):

I don't suppose the src has to be the same folder as my lean file?

#### Mario Carneiro (Feb 17 2020 at 03:46):

Make sure it gets unzipped to the same folder as mathlib itself, i.e. each foo.olean file should be right next to the analogous foo.lean file

#### Nicholas McConnell (Feb 17 2020 at 03:47):

On another note, when I did the other things, my_project/_target existed but there wasn't a mathlib folder

#### Mario Carneiro (Feb 17 2020 at 03:47):

Your lean file should be in my_project/src, and you have to have vscode open to the my_project folder.

#### Mario Carneiro (Feb 17 2020 at 03:48):

maybe try leanpkg configure from my_project directory?

#### Mario Carneiro (Feb 17 2020 at 03:48):

assuming you have already done leanpkg add leanprover-community/mathlib

#### Nicholas McConnell (Feb 17 2020 at 03:50):

I'm not sure what's going on

#### Mario Carneiro (Feb 17 2020 at 03:50):

You should really be more specific about error messages and the like

#### Nicholas McConnell (Feb 17 2020 at 03:50):

I have my project in the src folder, I have the terminal open to /my_project, and "import tactic" still isn't any different

#### Nicholas McConnell (Feb 17 2020 at 03:51):

"invalid import: tactic
could not resolve import: tactic"

#### Mario Carneiro (Feb 17 2020 at 03:51):

Try "Lean: restart" from the crtl-shift-p menu of vscode

#### Nicholas McConnell (Feb 17 2020 at 03:52):

"Cannot find runtime 'node' on PATH. Is 'node' installed?"

#### Mario Carneiro (Feb 17 2020 at 03:52):

Did you "open folder" at my_project in vscode?

#### Mario Carneiro (Feb 17 2020 at 03:53):

These are not terminal commands

#### Mario Carneiro (Feb 17 2020 at 03:53):

in vscode, there is a button to "open folder"

#### Mario Carneiro (Feb 17 2020 at 03:53):

open my_project

#### Mario Carneiro (Feb 17 2020 at 03:54):

are you using vscode?

Yeah?

#### Mario Carneiro (Feb 17 2020 at 03:54):

Do you see a folder hierarchy on the left side, like src/ and src/foo.lean?

Yup

#### Nicholas McConnell (Feb 17 2020 at 03:55):

Now "import tactic" has a different error message, which I just stated

#### Mario Carneiro (Feb 17 2020 at 03:55):

The my_project/src folder should be almost empty, it should just have whatever scratch files you are working on

#### Mario Carneiro (Feb 17 2020 at 03:55):

mathlib doesn't go there

#### Mario Carneiro (Feb 17 2020 at 03:56):

so my_project\src\tactic\default.lean should not exist

#### Nicholas McConnell (Feb 17 2020 at 03:56):

It has "algebra", "algebraic_geometry", ..., "topology" ---- supposedly what folder should they go in?

delete all of it

#### Mario Carneiro (Feb 17 2020 at 03:56):

that stuff goes in _target/mathlib/src

#### Mario Carneiro (Feb 17 2020 at 03:57):

and it's probably already there, hence the duplicate import

Ahh I see

#### Nicholas McConnell (Feb 17 2020 at 03:58):

Well, now it says it can't resolve the import again

#### Mario Carneiro (Feb 17 2020 at 03:59):

You created a file src/foo.lean and put import tactic in it?

#### Nicholas McConnell (Feb 17 2020 at 03:59):

Yeah? (Well, fermat.lean)

#### Mario Carneiro (Feb 17 2020 at 03:59):

does the file _target\deps\mathlib\src\tactic\default.lean exist?

#### Nicholas McConnell (Feb 17 2020 at 03:59):

Oh come to think of it, it actually works now

#### Nicholas McConnell (Feb 17 2020 at 03:59):

Dunno why it didn't right after the last thing it did, maybe it was readjusting

#### Nicholas McConnell (Feb 17 2020 at 04:00):

Thanks a bunch for the help

#### Mario Carneiro (Feb 17 2020 at 04:00):

Restart lean and see how long it takes for the orange bars to go away?

Alright

#### Nicholas McConnell (Feb 17 2020 at 04:01):

There's no error, but Lean isn't even reacting with anything

#### Nicholas McConnell (Feb 17 2020 at 04:02):

I'll just have to see what happens

#### Mario Carneiro (Feb 17 2020 at 04:02):

There are orange bars on the left gutter indicating that lean is working

Ah okay

#### Mario Carneiro (Feb 17 2020 at 04:02):

There is also a number of files in the status bar

#### Mario Carneiro (Feb 17 2020 at 04:02):

does it look like it is doing a lot of work?

#### Mario Carneiro (Feb 17 2020 at 04:03):

It should be speedy if compilation worked

#### Nicholas McConnell (Feb 17 2020 at 04:03):

Well it's taking a while

#### Mario Carneiro (Feb 17 2020 at 04:03):

does touch work on the command line

#### Nicholas McConnell (Feb 17 2020 at 04:04):

"touch: missing file operand

#### Mario Carneiro (Feb 17 2020 at 04:04):

try going to _target/deps/mathlib/src and run find src/ -name '*.olean' -exec touch {} +

#### Mario Carneiro (Feb 17 2020 at 04:05):

then restart lean and see if that fixes the issue

#### Nicholas McConnell (Feb 17 2020 at 04:05):

"find: ‘src/’: No such file or directory"

#### Mario Carneiro (Feb 17 2020 at 04:05):

oh, up one directory

#### Nicholas McConnell (Feb 17 2020 at 04:06):

I did that

Well, now Lean's not responding to the file, but there are no orange bars

#### Mario Carneiro (Feb 17 2020 at 04:07):

what does the status bar say?

#### Nicholas McConnell (Feb 17 2020 at 04:07):

Status bar? Not sure what that is

#### Mario Carneiro (Feb 17 2020 at 04:07):

bottom left, look for "Lean: ..."

#### Mario Carneiro (Feb 17 2020 at 04:08):

Here's a simple test file:

import tactic

#check tactic.tidy


#### Nicholas McConnell (Feb 17 2020 at 04:09):

Lean: [check mark] (checking visible files)

#### Mario Carneiro (Feb 17 2020 at 04:09):

and there is a squiggle over #check?

#### Mario Carneiro (Feb 17 2020 at 04:10):

I think you are good to go

#### Nicholas McConnell (Feb 17 2020 at 04:10):

Well I just tried the test file and see orange bars

#### Nicholas McConnell (Feb 17 2020 at 04:10):

Yup, I see the squiggle

#### Nicholas McConnell (Feb 17 2020 at 04:10):

So I imagine it should work

#### Nicholas McConnell (Feb 17 2020 at 04:11):

It's just completely nonresponsive to fermat.lean

#### Mario Carneiro (Feb 17 2020 at 04:11):

If lean crashes, you will get a message in the bottom right

#### Mario Carneiro (Feb 17 2020 at 04:11):

What's in the file?

#### Nicholas McConnell (Feb 17 2020 at 04:12):

Oh hey, I just closed the untracked fermat.lean and now it's working

great

Thank you ^^

#### Floris van Doorn (Feb 17 2020 at 20:49):

@Nicholas McConnell about the Python issue. If you reopen Git Bash and run which python again, do you still get /c/Users/nicho/AppData/Local/Microsoft/WindowsApps/python?

#### Rocky Kamen-Rubio (Feb 20 2020 at 18:29):

I'm keep getting this error message when I run leanpkg configure. I was able to install everything successfully manually but this is coming up when I try to configure mathlib from a cloned git repository. I've check that I have leanpkg.lean and leanpkg.toml in the correct places. Does anyone have any insight? Screen-Shot-2020-02-20-at-1.26.50-PM.png

#### Patrick Massot (Feb 20 2020 at 18:31):

Try removing the _target folder and start over.

#### Johan Commelin (Feb 20 2020 at 18:31):

Aside: this should probably be in the "general" stream.

#### Patrick Stevens (Feb 23 2020 at 20:28):

Rocky Kamen-Rubio said:

I'm keep getting this error message when I run leanpkg configure. I was able to install everything successfully manually but this is coming up when I try to configure mathlib from a cloned git repository. I've check that I have leanpkg.lean and leanpkg.toml in the correct places. Does anyone have any insight? Screen-Shot-2020-02-20-at-1.26.50-PM.png

As a rule of thumb, it's much more helpful to give text rather than pictures of text, by the way.

#### Nicholas McConnell (Feb 26 2020 at 03:53):

(deleted)

Last updated: May 09 2021 at 10:11 UTC