Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: installation issue

Jeremy Avigad (Jul 13 2020 at 14:17):

@Patrick Massot I have a user in my group who is trying to install Lean on Linux. He did the one-line install, but now types "leanproject get tutorial" and gets the error "leanproject: command not found". How shall I advise him?

Patrick Massot (Jul 13 2020 at 14:18):

source ~/.profile if he opened a different terminal but haven't logged in since installing.

Jeremy Avigad (Jul 13 2020 at 14:19):

He says he tried that already...

Jeremy Avigad (Jul 13 2020 at 14:19):

(and also an alternative version on the web page.)

Patrick Massot (Jul 13 2020 at 14:19):

echo $PATH and see if ~/.elan/bin is there

Johan Commelin (Jul 13 2020 at 14:20):

@Patrick Massot Do you want to move into a separate breakout room with this user?

Johan Commelin (Jul 13 2020 at 14:20):

We can ask Floris to take over your room for a moment

Patrick Massot (Jul 13 2020 at 14:20):

We could definitely do that

Patrick Massot (Jul 13 2020 at 14:20):

Scott and Markus are still in my room

Johan Commelin (Jul 13 2020 at 14:20):

@Floris van Doorn Are you available?

Johan Commelin (Jul 13 2020 at 14:20):

Oooh, ok

Johan Commelin (Jul 13 2020 at 14:20):

@Jeremy Avigad Who is the user?

Patrick Massot (Jul 13 2020 at 14:20):

So we don't need anyone else

Jeremy Avigad (Jul 13 2020 at 14:21):

Norman deVa ...

Patrick Massot (Jul 13 2020 at 14:21):

Assuming @Scott Morrison doesn't need to leave now

Floris van Doorn (Jul 13 2020 at 14:21):

I'm too late :)

Floris van Doorn (Jul 13 2020 at 14:21):

I am available if needed though

Scott Morrison (Jul 13 2020 at 14:21):

I'm fading :-)

Jeremy Avigad (Jul 13 2020 at 14:21):

We are in the same room.

Floris van Doorn (Jul 13 2020 at 14:21):

Do you want me to take over Scott?

Johan Commelin (Jul 13 2020 at 14:21):

Probably Markus can manage for 10 minutes (-;

Markus Himmel (Jul 13 2020 at 14:22):

Yes, no problem

Jeremy Avigad (Jul 13 2020 at 14:22):

He says ~/.elan/bin is in his path.

Jeremy Avigad (Jul 13 2020 at 14:33):

I am grateful for Patrick's help -- I was worried that I could not solve the problem. Patrick, I am curious to know that the problem was and how you fixed it

Jeremy Avigad (Jul 13 2020 at 14:35):

O.k., another question: a different user is trying to "leanproject get mathematics_in_lean" and is being asked for an SSH key.

Jeremy Avigad (Jul 13 2020 at 14:36):

I am guessing that this is a github setup issue and I directed him to the web page that explains how to set up SSH keys. Have other users had this problem?

Johan Commelin (Jul 13 2020 at 14:36):

Sophie had a similar issue this morning

Jeremy Avigad (Jul 13 2020 at 14:37):

Do you know how she solved it?

Scott Morrison (Jul 13 2020 at 14:37):

She eventually added an ssh key.

Scott Morrison (Jul 13 2020 at 14:37):

I'm still unsure what caused it.

Johan Commelin (Jul 13 2020 at 14:38):

@Jeremy Avigad which user?

Jeremy Avigad (Jul 13 2020 at 14:38):

He managed to solve it by signing into Github again. Anyhow, it is working now. (David Savitt is the user.)

Yakov Pechersky (Jul 13 2020 at 14:45):

It depends if you clone from git clone https://... or git clone ssh://...: https://docs.github.com/en/github/using-git/which-remote-url-should-i-use

Johan Commelin (Jul 13 2020 at 14:48):

But if you use leanproject than you shouldn't git clone at all...

Yakov Pechersky (Jul 13 2020 at 15:22):

Since https://github.com/leanprover-community/mathlib-tools/blob/24bab2810d0c9e7c03d21886f5b5577ba5d71b1c/mathlibtools/leanproject.py#L180if it will rely on ssh:// instead of https://

Dan Stanescu (Jul 13 2020 at 15:56):

Jeremy Avigad said:

O.k., another question: a different user is trying to "leanproject get mathematics_in_lean" and is being asked for an SSH key.

If I remember correctly, as opposed to other projects I got with leanproject get, it was also my experience that (much to my surprise) mathematics_in_lean asked to identify myself on GitHub before downloading.

Harshit J Motwani (Jul 13 2020 at 16:06):

I am facing this error when creating new lean package using this leanpackage new my_package in mac os :
error: no default toolchain configured. run elan toolchain install nightly
Command '['leanpkg', 'new', 'my_project']' returned non-zero exit status 1

I don't have any issues with leanproject get