Easy to get started

Stream: new members

[Bjørn Kjos-Hanssen]

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]

@Bjørn Kjos-Hanssen Hi, welcome!

[Johan Commelin]

How did you install Lean?

[Johan Commelin]

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]

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]

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]

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

[Johan Commelin]

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

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

Do you have leanproject installed?

[Johan Commelin]

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]

I just installed it a few days ago

[Johan Commelin]

I see. Did you follow this page by chance? https://leanprover-community.github.io/get_started.html#regular-install

[Johan Commelin]

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]

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]

Looks like you have some installation of mathlib somewhere

[Johan Commelin]

Does which leanproject in a terminal give you anything sensible?

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

Great

[Kevin Lacker]

you can install leanproject with anaconda? weird

[Johan Commelin]

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]

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

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

Ouch, that doesn't sound good

[Johan Commelin]

And in the terminal, does which leanpkg work?

[Johan Commelin]

how about which elan?

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Johan Commelin]

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

[Bjørn Kjos-Hanssen]

No, which elan just returns the empty string

[Kevin Lacker]

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

[Johan Commelin]

Bjørn Kjos-Hanssen said:

No, which elan just returns the empty string

Ooh, that's bad.

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

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]

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

[Kevin Lacker]

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

[Kevin Lacker]

the lean installation instructions will probably just quietly fail for you

[Kevin Lacker]

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]

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

[Bjørn Kjos-Hanssen]

I use Python but not Anaconda AFAIK

[Kevin Lacker]

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

[Johan Commelin]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Bjørn Kjos-Hanssen]

hmm well now I have elan

[Bjørn Kjos-Hanssen]

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

[Johan Commelin]

Great

[Johan Commelin]

would you mind trying leanproject new my_playground again?

[Bjørn Kjos-Hanssen]

That worked

[Johan Commelin]

Now open it in VScode

[Johan Commelin]

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

[Bjørn Kjos-Hanssen]

ooh... that seems to have fixed it

[Bjørn Kjos-Hanssen]

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]

(14 grad students in a class, I mean)

[Kevin Lacker]

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]

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

[Johan Commelin]

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

[Johan Commelin]

See the bundles at the bottom of the install page

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Bjørn Kjos-Hanssen]

(deleted)

[Yury G. Kudryashov]

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