Zulip Chat Archive

Stream: new members

Topic: Easy to get started


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

view this post on Zulip Johan Commelin (Sep 29 2020 at 17:48):

@Bjørn Kjos-Hanssen Hi, welcome!

view this post on Zulip Johan Commelin (Sep 29 2020 at 17:48):

How did you install Lean?

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

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

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:00):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:01):

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:02):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:02):

Do you have leanproject installed?

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:04):

I just installed it a few days ago

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:05):

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

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

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:07):

Looks like you have some installation of mathlib somewhere

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:08):

Does which leanproject in a terminal give you anything sensible?

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:08):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:08):

Great

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:09):

you can install leanproject with anaconda? weird

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:09):

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:10):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:11):

Ouch, that doesn't sound good

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:11):

And in the terminal, does which leanpkg work?

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:12):

how about which elan?

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:12):

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

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

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

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:14):

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

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:14):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:15):

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:15):

No, which elan just returns the empty string

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:15):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:16):

Bjørn Kjos-Hanssen said:

No, which elan just returns the empty string

Ooh, that's bad.

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:16):

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

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:17):

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

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

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:17):

the lean installation instructions will probably just quietly fail for you

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:18):

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:18):

I use Python but not Anaconda AFAIK

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:19):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:19):

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

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

view this post on Zulip Kevin Lacker (Sep 29 2020 at 18:20):

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:21):

hmm well now I have elan

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:22):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:23):

Great

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:24):

would you mind trying leanproject new my_playground again?

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:25):

That worked

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:25):

Now open it in VScode

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:27):

ooh... that seems to have fixed it

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:29):

(14 grad students in a class, I mean)

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

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:33):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:34):

See the bundles at the bottom of the install page

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:34):

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

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:35):

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

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

view this post on Zulip Bjørn Kjos-Hanssen (Sep 29 2020 at 18:36):

(deleted)

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