Zulip Chat Archive

XXX MINGW64 /c/mathlib
$ /c/Users/Kenny\ Lau/.elan/bin/elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.7.2
info: downloading component 'lean'
info: installing component 'lean'
info: checking for self-updates

  stable updated - Lean (version 3.7.2, commit 44fb9f994d0f, Release)


XXX MINGW64 /c/mathlib
$ /c/Users/Kenny\ Lau/.elan/bin/lean --make src
info: downloading component 'lean'
info: installing component 'lean'

Kenny Lau (Apr 06 2020 at 15:22):

Am I doing this properly?

Johan Commelin (Apr 06 2020 at 15:23):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md#get-scripts

Patrick Massot (Apr 06 2020 at 15:23):

No.

Johan Commelin (Apr 06 2020 at 15:24):

Kenny... you can be forgiven for entering college with a Windows machine... but shouldn't you be using Linux by now?

Johan Commelin (Apr 06 2020 at 15:25):

You should think of "Windows : Linux" as "classical : constructive"...

Kenny Lau (Apr 06 2020 at 15:25):

why... is python involved...???

Johan Commelin (Apr 06 2020 at 15:26):

Because Lean is a very bad scripting language

Simon Cruanes (Apr 06 2020 at 15:27):

Johan Commelin said:

You should think of "Windows : Linux" as "classical : constructive"...

so… a lot of people are right to use windows? :stuck_out_tongue:

Johan Commelin (Apr 06 2020 at 15:27):

No.... only Kenny is wrong

Johan Commelin (Apr 06 2020 at 15:28):

@Kenny Lau I'm really sorry: Zulip doesn't have a :troll: emoji.

Simon Cruanes (Apr 06 2020 at 15:29):

I use " :upside_down: " for that

Johan Commelin (Apr 06 2020 at 15:29):

Ooh, I've used that one for many different things

Marc Huisinga (Apr 06 2020 at 15:31):

while we're at it, what on earth is :octopus: used for? i've been wondering since i joined this chat.

Johan Commelin (Apr 06 2020 at 15:31):

happy happy joy joy

Johan Commelin (Apr 06 2020 at 15:31):

I think the octopus is clearly celebrating

Kevin Buzzard (Apr 06 2020 at 15:31):

I just used to used it randomly

Marc Huisinga (Apr 06 2020 at 15:31):

i've seen it used for people finding bugs?

Johan Commelin (Apr 06 2020 at 15:32):

Well, I think it's a sort of Lean zulip meme. You can use it whenever you want (-;

Patrick Massot (Apr 06 2020 at 15:33):

I think this is purely Johan's creation, so if Johan says you can use it whenever you want, then you can.

Kenny Lau (Apr 06 2020 at 15:34):

what do I do after installing mathlibtools?

Johan Commelin (Apr 06 2020 at 15:34):

No, I think Sean started it

Johan Commelin (Apr 06 2020 at 15:34):

Kenny Lau said:

what do I do after installing mathlibtools?

leanproject up

Johan Commelin (Apr 06 2020 at 15:34):

Gets you latest mathlib + binaries

Kenny Lau (Apr 06 2020 at 15:35):

where?

Kevin Buzzard (Apr 06 2020 at 15:35):

in root dir of project

Kenny Lau (Apr 06 2020 at 15:35):

what is leanproject?

Johan Commelin (Apr 06 2020 at 15:35):

In /home/kenny/random_junk/mathlib/

Kevin Buzzard (Apr 06 2020 at 15:35):

Works for projects which have mathlib as a dependency, and for mathlib too. Downloads compiled oleans.

Johan Commelin (Apr 06 2020 at 15:35):

Kenny Lau said:

what is leanproject?

It's Patrick's brainchild.

Johan Commelin (Apr 06 2020 at 15:35):

Amazing stuff. Better than coke.

Kenny Lau (Apr 06 2020 at 15:36):

I don't understand

Kenny Lau (Apr 06 2020 at 15:36):

I just did pip3 install mathlibtools

Johan Commelin (Apr 06 2020 at 15:36):

Basically, we don't know how people ever managed their Lean projects without it

Kenny Lau (Apr 06 2020 at 15:36):

so where was it installed

Patrick Massot (Apr 06 2020 at 15:36):

https://github.com/leanprover-community/mathlib-tools/blob/master/README.md

Kevin Buzzard (Apr 06 2020 at 15:36):

leanproject is a python script which tries to make stuff easy for the beginner. It does everything which someone at Xena wants doing when their code doesn't work.

Johan Commelin (Apr 06 2020 at 15:36):

It was installed on your computer

Johan Commelin (Apr 06 2020 at 15:36):

Hopefully in your PATH

Patrick Massot (Apr 06 2020 at 15:36):

It's Patrick's brainchild.

Actually it builds on a lot of previous work by many people.

Kenny Lau (Apr 06 2020 at 15:36):

where is leanproject located?

Kenny Lau (Apr 06 2020 at 15:37):

my PATH doesn't have much to it

Kevin Buzzard (Apr 06 2020 at 15:37):

What OS?

Kenny Lau (Apr 06 2020 at 15:37):

windows

Ryan Lahfa (Apr 06 2020 at 15:37):

Kenny Lau said:

where is leanproject located?

If you try pip3 install --user mathlibtools, is it better?

Patrick Massot (Apr 06 2020 at 15:37):

If your python setup is sane then you don't need to know where leanproject lives.

Ryan Lahfa (Apr 06 2020 at 15:37):

pip3 will try to install in a global system-packages, but sometimes, you'll encounter permissions issues because your Windows shell is not Administrator

Kenny Lau (Apr 06 2020 at 15:37):

I don't even have pip in my path, I just type the address manually

Ryan Lahfa (Apr 06 2020 at 15:38):

@Kenny Lau If you want to make it easier for you, you can use this kind of stuff: https://chocolatey.org/

Johan Commelin (Apr 06 2020 at 15:38):

Well, use the Windows search tool to find leanproject somewhere on your hard drive...

Kenny Lau (Apr 06 2020 at 15:38):

$ /c/Python-3.6.4/python -m pip install mathlibtools

Ryan Lahfa (Apr 06 2020 at 15:38):

@Kenny Lau If Python is not in your PATH, even if you install the package, Python might not know where to search

Kenny Lau (Apr 06 2020 at 15:38):

then where did python install the package to?

Ryan Lahfa (Apr 06 2020 at 15:39):

@Kenny Lau Most likely under /c/Python-3.6.4/<some folders> or in some $AppData/…

Johan Commelin (Apr 06 2020 at 15:39):

/c/Python-3.6.4/site-packages/leanproject/??

Ryan Lahfa (Apr 06 2020 at 15:40):

This might help you more than what I say, @Kenny Lau : https://docs.python.org/3/using/windows.html

Kenny Lau (Apr 06 2020 at 15:40):

I found it in C:\Python-3.6.4\Scripts

Kenny Lau (Apr 06 2020 at 15:44):

how do I link VSCode to elan?

Kenny Lau (Apr 06 2020 at 15:44):

more specifically how do I tell VSCode to use the lean installed by elan?

Johan Commelin (Apr 06 2020 at 15:44):

On the first page of the installer, an option labelled “Add Python to PATH” may be selected to have the installer add the install location into the PATH. The location of the Scripts\ folder is also added.

Johan Commelin (Apr 06 2020 at 15:45):

Kenny Lau said:

more specifically how do I tell VSCode to use the lean installed by elan?

Follow the install instructions?

Johan Commelin (Apr 06 2020 at 15:46):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md#installing-and-configuring-an-editor

Kenny Lau (Apr 06 2020 at 15:46):

I have C:\Users\Kenny Lau\.elan\bin in my PATH

Kenny Lau (Apr 06 2020 at 15:47):

but when I type lean, it says command not found

Kenny Lau (Apr 06 2020 at 15:47):

and /c/Users/Kenny\ Lau/.elan/bin/lean works fine

Johan Commelin (Apr 06 2020 at 15:47):

Does the \ matter?

Johan Commelin (Apr 06 2020 at 15:48):

As in, should that also be in your PATH?

Johan Commelin (Apr 06 2020 at 15:48):

/me doesn't know windows

Kenny Lau (Apr 06 2020 at 15:48):

oh right, VSCode can never use elan because VSCode can't have spaces

Kenny Lau (Apr 06 2020 at 15:48):

maybe i need to copy the elan to a different folder

Kenny Lau (Apr 06 2020 at 15:50):

oh and I just added C:\Python-3.6.4\Scripts to my PATH but leanproject is still command not found

Ryan Lahfa (Apr 06 2020 at 15:50):

Kenny Lau said:

oh right, VSCode can never use elan because VSCode can't have spaces

theorically you can escape spaces like you've done /c/Users/Kenny\ …/…

Kenny Lau (Apr 06 2020 at 15:50):

Kenny Lau@DESKTOP-F01EMD3 MINGW64 ~
$ leanproject
bash: leanproject: command not found

Kenny Lau@DESKTOP-F01EMD3 MINGW64 ~
$ /c/Python-3.6.4/Scripts/leanproject
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
[...]