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.

[jgart]

Hi, has anyone had success with the lean installer in vscode on Fedora 41 Workstation?

[Notification Bot]

A message was moved here from #new members > Could someone help for proving this problem (identity 212)? by Eric Wieser.

[jgart]

The installer assumes that it can append into my ~/.profile but that is read-only.

[Chris Bailey]

I didn't have any issues, but I also have elan appended to my ~/.profile (I don't think I put it there).

[jgart]

Thanks for the feedback.

I know why my ~/.profile is read-only now. It's because of an immutable package manager that I am using for my home dotfiles (Guix which is like Nix).

Is it possible to have the elan write this configuration somewhere else?

[jgart]

Another interesting thing is that the installer checks that step green, signifying that it completed the step successfully when it actually failed to do so because of not being able to write to ~/.profile.

[Chris Bailey]

Does it require that to actually install everything else, or is that just part of the installation process? My first thought would be to just run the thing and put what it would have put in your profile wherever it needs to go in order for the PATH stuff to work. The string it writes is export PATH="$HOME/.elan/bin:$PATH"

[jgart]

This is what my ~/.profile contains:

$ cat .profile
HOME_ENVIRONMENT=$HOME/.guix-home
. $HOME_ENVIRONMENT/setup-environment
$HOME_ENVIRONMENT/on-first-login

[jgart]

But that ~/.profile is read-only.

[Chris Bailey]

If you've already run the installer, do you have a .elan folder?

[jgart]

Chris Bailey said:

My first thought would be to just run the thing and put what it would have put in your profile wherever it needs to go in order for the PATH stuff to work. The string it writes is export PATH="$HOME/.elan/bin:$PATH"

I was thinking that as well but I was also wondering where exactly it failed in that install step and what might it had failed to run after attempting to write the export command.

I'll have to read this install script source code closely. I haven't looked at that yet.

[jgart]

Chris Bailey said:

If you've already run the installer, do you have a .elan folder?

I do

$ ls .elan/bin/
elan  lake  lean  leanc  leanchecker  leanmake  leanpkg

[jgart]

Given the above, it sounds like I can just put that directory on PATH and proceed.

[jgart]

It sounds like maybe the installer should handle such a case in a less intrusive way. Maybe it could just suggest the user to add ~/.elan to PATH. If it wants to make that more user friendly it can print to standard output some ideas on how to do that instead of trying to write to ~/.profile on the user's behalf.

[Julian Berman]

--no-modify-path will tell the installer not to touch your system

[Julian Berman]

And then yes you simply append to your PATH however you like

[jgart]

--no-modify-path will tell the installer not to touch your system

TIL: Thanks.

[jgart]

I was also thinking that I might want to run the Lean installer in a toolbox or distrobox (podman container with access to host home) so that I don't modify my file system with various paths I'm not tracking or don't want to worry about how to clean up later.

[jgart]

Julian Berman said:

--no-modify-path will tell the installer not to touch your system

If I remember correctly, though, I migh have just clicked a button in vscode in order to start the process so not sure how I might have passed in that flag :duck:

[jgart]

I guess I should not follow the vscode GUI installation steps and find command line install steps instead :duck:

[jgart]

Looks like maybe this might have been the culprit. I'll try to reproduce the issue later and maybe report it:

https://github.com/leanprover/elan/blob/417e1abbd6e24781dde778e2d75d51361378f242/src/elan-cli/self_update.rs#L264

[jgart]

Thanks for the help with this. Much appreciated.