installation on Fedora

Stream: new members

[mario]

Hi All,
test. Do you see my message?

[mario]

Hi
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 (140.82.121.4)' 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]

I am on a Fedora 35 machine

[Julian Berman]

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

[Julian Berman]

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

[Notification Bot]

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

[Julian Berman]

(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]

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

[Julian Berman]

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

[mario]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

It seems it works fine now. Thanks.