Zulip Chat Archive

Stream: new members

Topic: installation on Fedora

mario (Feb 11 2022 at 14:14):

Hi All,
test. Do you see my message?

mario (Feb 11 2022 at 14:20):

lean newbie here.
I am trying to install and looking at the tutorial package -https://leanprover-community.github.io/install/project.html
I get

[mario@localhost lean]$ leanproject get tutorials
Cloning from git@github.com:leanprover-community/tutorials.git
The authenticity of host 'github.com (' can't be established.
ED25519 key fingerprint is SHA256:+........
This key is not known by any other names
Are you sure you want to continue connecting (yes/no/[fingerprint])? yes
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/tutorials.git
[Errno 2] No such file or directory: 'leanpkg'

which error is that?

mario (Feb 11 2022 at 14:21):

I am on a Fedora 35 machine

Julian Berman (Feb 11 2022 at 14:21):

Have you followed the installation instructions from here: https://leanprover-community.github.io/install/linux.html

Julian Berman (Feb 11 2022 at 14:22):

That error essentially means Lean (or elan) isn't installed, or isn't findable.

Notification Bot (Feb 11 2022 at 14:22):

This topic was moved here from #general > Test by Rob Lewis

Julian Berman (Feb 11 2022 at 14:22):

(The first part is unrelated and has something to do with your SSH setup, but is some separate issue that can be fixed after)

mario (Feb 11 2022 at 14:26):

Yes, I did. I tried VisualCode too, I create a test.lean, write #eval 1+2, and see 2.

Julian Berman (Feb 11 2022 at 14:32):

OK -- can you show us what type -a elan says?

mario (Feb 11 2022 at 14:37):

Julian Berman said:

OK -- can you show us what type -a elan says?

 type -a elan
elan is /home/mario/.elan/bin/elan
elan is /home/mario/.elan/bin/elan
elan is /home/mario/.elan/bin/elan

BUT, something I miss on my shell. Above on the tab I did PATH=$PATH:$HOME/.elan/bin. On the tab I launch leanproject get tutorials, i just get type -a elan > bash: type: elan: not found

Julian Berman (Feb 11 2022 at 14:38):

Is that the shell you first ran the installation instructions on? Can you restart your terminal and try leanproject get tutorials in a new one?

mario (Feb 11 2022 at 14:45):

My fault. I have two attempts of install, somehow mixed up. I clean my mess and try again. Thanks for now.

Reid Barton (Feb 11 2022 at 14:48):

Running a command like PATH=$PATH:$HOME/.elan/bin in a shell will only affect that shell (in your case, that tab).

Reid Barton (Feb 11 2022 at 14:49):

But the elan installation process should also have added this command to your shell's startup scripts, so it should work automatically in new shells.

mario (Feb 11 2022 at 21:37):

It seems it works fine now. Thanks.

Last updated: Dec 20 2023 at 11:08 UTC