MathLib installing

Stream: maths

[Nicholas McConnell]

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]

You don't need python for mathlib to work

[Nicholas McConnell]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

the python is to help with this part

[Nicholas McConnell]

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

[Nicholas McConnell]

Thanks for the help

[Sebastien Gouezel]

@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]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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

[Gabriel Ebner]

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

[Patrick Massot]

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]

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

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean/releases/download/v0.14.11/lean-0.14.11.vsix

[Patrick Massot]

Nice!

[Nicholas McConnell]

I tried doing this https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

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

[Mario Carneiro]

you did the first three lines before update-mathlib?

[Mario Carneiro]

do lean and leanpkg work?

[Nicholas McConnell]

Yeah, and leanpkg works

[Nicholas McConnell]

But I got "bash: update-mathlib: command not found"

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Nicholas McConnell]

Alright, I've unzipped the tar

[Nicholas McConnell]

But "import tactic" still doesn't work

[Nicholas McConnell]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

maybe try leanpkg configure from my_project directory?

[Mario Carneiro]

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

[Nicholas McConnell]

I'm not sure what's going on

[Mario Carneiro]

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

[Nicholas McConnell]

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]

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

[Mario Carneiro]

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

[Nicholas McConnell]

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

[Mario Carneiro]

Did you "open folder" at my_project in vscode?

[Nicholas McConnell]

'open' is "command not found"

[Mario Carneiro]

These are not terminal commands

[Mario Carneiro]

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

[Mario Carneiro]

open my_project

[Mario Carneiro]

are you using vscode?

[Nicholas McConnell]

Yeah?

[Nicholas McConnell]

"ambiguous import, it can be 'c:\Users\nicho\Downloads\lean-3.4.2-windows\bin\my_project\_target\deps\mathlib\src\tactic\default.lean' or 'c:\Users\nicho\Downloads\lean-3.4.2-windows\bin\my_project\src\tactic\default.lean'"

[Mario Carneiro]

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

[Nicholas McConnell]

Yup

[Nicholas McConnell]

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

[Mario Carneiro]

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

[Mario Carneiro]

mathlib doesn't go there

[Mario Carneiro]

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

[Nicholas McConnell]

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

[Mario Carneiro]

delete all of it

[Mario Carneiro]

that stuff goes in _target/mathlib/src

[Mario Carneiro]

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

[Nicholas McConnell]

Ahh I see

[Nicholas McConnell]

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

[Mario Carneiro]

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

[Nicholas McConnell]

Yeah? (Well, fermat.lean)

[Mario Carneiro]

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

[Nicholas McConnell]

Oh come to think of it, it actually works now

[Nicholas McConnell]

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

[Nicholas McConnell]

Thanks a bunch for the help

[Mario Carneiro]

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

[Nicholas McConnell]

Alright

[Nicholas McConnell]

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

[Nicholas McConnell]

I'll just have to see what happens

[Mario Carneiro]

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

[Nicholas McConnell]

Ah okay

[Mario Carneiro]

There is also a number of files in the status bar

[Mario Carneiro]

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

[Mario Carneiro]

It should be speedy if compilation worked

[Nicholas McConnell]

Well it's taking a while

[Mario Carneiro]

does touch work on the command line

[Nicholas McConnell]

"touch: missing file operand
Try 'touch --help' for more information."

[Mario Carneiro]

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

[Mario Carneiro]

then restart lean and see if that fixes the issue

[Nicholas McConnell]

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

[Mario Carneiro]

oh, up one directory

[Nicholas McConnell]

I did that

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

[Mario Carneiro]

what does the status bar say?

[Nicholas McConnell]

Status bar? Not sure what that is

[Mario Carneiro]

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

[Mario Carneiro]

Here's a simple test file:

import tactic

#check tactic.tidy

[Nicholas McConnell]

Lean: [check mark] (checking visible files)

[Mario Carneiro]

and there is a squiggle over #check?

[Mario Carneiro]

I think you are good to go

[Nicholas McConnell]

Well I just tried the test file and see orange bars

[Nicholas McConnell]

Yup, I see the squiggle

[Nicholas McConnell]

So I imagine it should work

[Nicholas McConnell]

It's just completely nonresponsive to fermat.lean

[Mario Carneiro]

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

[Mario Carneiro]

What's in the file?

[Nicholas McConnell]

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

[Mario Carneiro]

great

[Nicholas McConnell]

Thank you ^^

[Floris van Doorn]

@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]

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]

Try removing the _target folder and start over.

[Johan Commelin]

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

[Patrick Stevens]

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]

(deleted)

[Notification Bot]

This topic was moved to #new members > MathLib installing by Scott Morrison.