Zulip Chat Archive

Stream: maths

Topic: MathLib installing


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 16 2020 at 05:07):

You don't need python for mathlib to work

view this post on Zulip Nicholas McConnell (Feb 16 2020 at 05:07):

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

view this post on Zulip Mario Carneiro (Feb 16 2020 at 05:07):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2020 at 05:08):

the python is to help with this part

view this post on Zulip Nicholas McConnell (Feb 16 2020 at 05:09):

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

view this post on Zulip Nicholas McConnell (Feb 16 2020 at 05:09):

Thanks for the help

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 16 2020 at 19:40):

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

view this post on Zulip Patrick Massot (Feb 16 2020 at 19:41):

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

view this post on Zulip 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à

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Feb 16 2020 at 19:49):

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

view this post on Zulip Gabriel Ebner (Feb 16 2020 at 19:55):

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

view this post on Zulip Patrick Massot (Feb 16 2020 at 20:09):

Nice!

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:31):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:33):

you did the first three lines before update-mathlib?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:34):

do lean and leanpkg work?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:35):

Yeah, and leanpkg works

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:35):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:41):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:45):

Alright, I've unzipped the tar

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:45):

But "import tactic" still doesn't work

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:46):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:48):

maybe try leanpkg configure from my_project directory?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:48):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:50):

I'm not sure what's going on

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:50):

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

view this post on Zulip 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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:51):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:51):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:52):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:52):

Did you "open folder" at my_project in vscode?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:52):

'open' is "command not found"

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:53):

These are not terminal commands

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:53):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:53):

open my_project

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:54):

are you using vscode?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:54):

Yeah?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:54):

"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'"

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:54):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:55):

Yup

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:55):

mathlib doesn't go there

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:56):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:56):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:56):

delete all of it

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:56):

that stuff goes in _target/mathlib/src

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:57):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:57):

Ahh I see

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:58):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:59):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:59):

Yeah? (Well, fermat.lean)

view this post on Zulip Mario Carneiro (Feb 17 2020 at 03:59):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:59):

Oh come to think of it, it actually works now

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 03:59):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:00):

Thanks a bunch for the help

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:00):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:01):

Alright

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:01):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:02):

I'll just have to see what happens

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:02):

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

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:02):

Ah okay

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:02):

There is also a number of files in the status bar

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:02):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:03):

It should be speedy if compilation worked

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:03):

Well it's taking a while

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:03):

does touch work on the command line

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:04):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:04):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:05):

then restart lean and see if that fixes the issue

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:05):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:05):

oh, up one directory

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:07):

what does the status bar say?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:07):

Status bar? Not sure what that is

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:07):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:08):

Here's a simple test file:

import tactic

#check tactic.tidy

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:09):

Lean: [check mark] (checking visible files)

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:09):

and there is a squiggle over #check?

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:10):

I think you are good to go

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:10):

Well I just tried the test file and see orange bars

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:10):

Yup, I see the squiggle

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:10):

So I imagine it should work

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:11):

It's just completely nonresponsive to fermat.lean

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:11):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:11):

What's in the file?

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:12):

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

view this post on Zulip Mario Carneiro (Feb 17 2020 at 04:12):

great

view this post on Zulip Nicholas McConnell (Feb 17 2020 at 04:14):

Thank you ^^

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 20 2020 at 18:31):

Try removing the _target folder and start over.

view this post on Zulip Johan Commelin (Feb 20 2020 at 18:31):

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

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Feb 26 2020 at 03:53):

(deleted)


Last updated: May 09 2021 at 10:11 UTC