## Stream: new members

### Topic: Easy to get started

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 17:39):

So the Natural Number Game is very slick and easy to understand. The beginning chapters of Logic and Proof as well. But then I get to the part where we have to "import data.set" and Visual Studio Code keeps saying "data/set not found"...

#### Johan Commelin (Sep 29 2020 at 17:48):

@Bjørn Kjos-Hanssen Hi, welcome!

#### Johan Commelin (Sep 29 2020 at 17:48):

How did you install Lean?

#### Johan Commelin (Sep 29 2020 at 17:49):

data.set is part of mathlib. You will need to work in either (i) a project that depends on mathlib, or (ii) a copy of mathlib itself.

#### Johan Commelin (Sep 29 2020 at 17:49):

If you just have a random Lean file, then you cannot really use mathlib. (There are ways, but we don't recommend them.)

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 17:59):

Thanks @Johan Commelin I guess I just followed the instructions, kind of forgot how. I think I may have a "project" (at least a directory with a .path and .toml file and src subdirectory) but not sure what "project that depends on mathlib" means.

#### Johan Commelin (Sep 29 2020 at 18:00):

Ok, well, is mathlib listed in the .toml?

#### Johan Commelin (Sep 29 2020 at 18:01):

Another common issue is that you shouldn't "Open File" in VScode, but "Open Folder".

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:02):

It's not there... so, how to list mathlib in the .toml ?

#### Johan Commelin (Sep 29 2020 at 18:02):

Do you have leanproject installed?

#### Johan Commelin (Sep 29 2020 at 18:03):

Did you install lean within the last month, or do you have some installation from say 13 months ago? (This matters for knowing what kind of installation you might have done....)

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:04):

I just installed it a few days ago

#### Johan Commelin (Sep 29 2020 at 18:06):

If you did something like brew install lean on your macos... then you won't have all the nice community tools. We're trying to get rid of that package |-;

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:06):

Probably I did... Thanks for the tip about opening a folder, that changed the error messages, for instance to invalid import: data.set /Applications/lean-3.4.2-darwin/lib/lean/library/data/set/intervals/unordered_interval.lean:40:50: error: unexpected token

#### Johan Commelin (Sep 29 2020 at 18:07):

Looks like you have some installation of mathlib somewhere

#### Johan Commelin (Sep 29 2020 at 18:08):

Does which leanproject in a terminal give you anything sensible?

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:08):

Yes, /Users/bjoernkjos-hanssen/opt/anaconda3/bin/leanproject

Great

#### Kevin Lacker (Sep 29 2020 at 18:09):

you can install leanproject with anaconda? weird

#### Johan Commelin (Sep 29 2020 at 18:09):

leanproject new my_playground will create a directory my_playground and inside it will be a lean project that has mathlib as dependency

#### Johan Commelin (Sep 29 2020 at 18:09):

I suggest you try that, and then open the my_playground folder in VScode

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:10):

That gave No such file or directory: 'leanpkg': 'leanpkg'

#### Johan Commelin (Sep 29 2020 at 18:11):

Ouch, that doesn't sound good

#### Johan Commelin (Sep 29 2020 at 18:11):

And in the terminal, does which leanpkg work?

#### Johan Commelin (Sep 29 2020 at 18:12):

how about which elan?

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:12):

it does not return anything, even though there is a leanpkg executable in the same directory

#### Johan Commelin (Sep 29 2020 at 18:12):

Btw, there is 3 minute installation video for mac os, if you are into such things

#### Johan Commelin (Sep 29 2020 at 18:13):

I understand that the installation can be complicated. But if you follow the right path, it should be easy, fast, and smooth.

#### Kevin Lacker (Sep 29 2020 at 18:13):

in my experience, the installation process very often conflicts with other things you are doing on your computer, especially different python environments

#### Kevin Lacker (Sep 29 2020 at 18:14):

in particular, the instructions suggest brew install for some components and pipx for others

#### Kevin Lacker (Sep 29 2020 at 18:14):

whereas, @Bjørn Kjos-Hanssen it seems like you have installed some python components via anaconda

#### Johan Commelin (Sep 29 2020 at 18:15):

@Bjørn Kjos-Hanssen Does which elan give you anything?

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:15):

No, which elan just returns the empty string

#### Kevin Lacker (Sep 29 2020 at 18:15):

@Bjørn Kjos-Hanssen what does which python3 give you

#### Johan Commelin (Sep 29 2020 at 18:16):

Bjørn Kjos-Hanssen said:

No, which elan just returns the empty string

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:16):

/Users/bjoernkjos-hanssen/opt/anaconda3/bin/python3

#### Johan Commelin (Sep 29 2020 at 18:16):

Without elan life will be painful. It manages different versions of lean for you. (Lean released a new version about 15 times this year already.)

#### Johan Commelin (Sep 29 2020 at 18:17):

https://leanprover-community.github.io/install/macos_details.html#installing-codeelancode

#### Kevin Lacker (Sep 29 2020 at 18:17):

so basically you are using the anaconda version of python, and the lean installation instructions are using the brew install vresion

#### Kevin Lacker (Sep 29 2020 at 18:17):

the lean installation instructions will probably just quietly fail for you

#### Kevin Lacker (Sep 29 2020 at 18:18):

are you intentionally using anaconda for something? you could just use the brew install version, but if you're doing python development in other places it'll cause conflict

#### Johan Commelin (Sep 29 2020 at 18:18):

Well, they didn't fail quietly. They told us that leanpkg didn't exist.

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:18):

I use Python but not Anaconda AFAIK

#### Kevin Lacker (Sep 29 2020 at 18:19):

try running brew install python3 if you don't mind altering your current python install

#### Johan Commelin (Sep 29 2020 at 18:19):

Please first install elan. After that, maybe all problems will be gone already

#### Kevin Lacker (Sep 29 2020 at 18:20):

i wouldn't do that - the elan install instructions assume you are using the brew version of python

#### Kevin Lacker (Sep 29 2020 at 18:20):

so how are you going to get a sane install using a different python default

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:21):

hmm well now I have elan

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:22):

which elan returns /Users/bjoernkjos-hanssen/.elan/bin/elan

Great

#### Johan Commelin (Sep 29 2020 at 18:24):

would you mind trying leanproject new my_playground again?

That worked

#### Johan Commelin (Sep 29 2020 at 18:25):

Now open it in VScode

#### Johan Commelin (Sep 29 2020 at 18:26):

And see if you can create a new file inside the project, and run import data.set or somthing

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:27):

ooh... that seems to have fixed it

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:29):

Thanks a lot.. Now just need to summarize this so that my 14 graduate students can easily replicate it :sweat_smile:

#### Bjørn Kjos-Hanssen (Sep 29 2020 at 18:29):

(14 grad students in a class, I mean)

#### Kevin Lacker (Sep 29 2020 at 18:30):

i got my python install in a screwed up place at some point and found it easier to just reinstall everything, ie uninstall my python environment and follow the lean installation instructions from the beginning

#### Kevin Lacker (Sep 29 2020 at 18:30):

so if i were telling a lot of grad students what to do, i'd tell them that

#### Johan Commelin (Sep 29 2020 at 18:33):

@Bjørn Kjos-Hanssen Note that we also have "packages" for students.

#### Johan Commelin (Sep 29 2020 at 18:34):

See the bundles at the bottom of the install page

#### Johan Commelin (Sep 29 2020 at 18:34):

https://leanprover-community.github.io/get_started.html#maybe-a-couple-of-nights

#### Johan Commelin (Sep 29 2020 at 18:35):

They are meant for people who don't usually play with the internals of their computers

#### Johan Commelin (Sep 29 2020 at 18:35):

So if this is a CS course, then maybe it's not a good idea. But if it is for maths students, then maybe yes.

(deleted)

#### Yury G. Kudryashov (Sep 29 2020 at 18:57):

In this case there were no problems with python installation. elan was missing

Last updated: May 14 2021 at 07:19 UTC