Instaling elan, lean, lake in conda

Stream: lean4

[Jason Rute]

I want to install Lean on a high performance compute cluster (linux) which is pretty locked down (no root permissions). In the past, I've installed Ocaml, Coq, Python, and other things via conda. It works pretty well by providing a virtual environment in which I can install things and nuke them when I'm done. (Docker and other containers are not an option, unfortunately.) Most things I can brew install or apt-get install I can also conda install. How might I install Lean in a conda environment?. (Also, I know how to do vs code remotely already in this system and I'm also fine just running elan/lean/lake from the command line for my purposes.)

[Jason Rute]

I know there is a setup script for Lean in linux. I didn't run it yet for two reasons:

• I don't know enough of what it does to trust running it in this environment.
• I assume it will try to install things in a place that won't work and will fail anyway due to permissions.

[Jason Rute]

Also, this is sort of a long term ask to put elan-init (or whatever the Lean entry point is now-a-days) on conda-forge.

[Patrick Massot]

You don’t need any permission to install Lean. In fact the opposite is true: trying to have a system-wide Lean or even system-wide libraries is currently not supported.

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Using.20a.20read-only.20lib.2E/near/419738452 to learn how much your situation is the easy one.

[Jason Rute]

So if I run this script (https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh), where does it install Lean? On my Mac (which I set up a while ago), lake, elan, and lean are all in /usr/local/bin.

[Jason Rute]

Oh, nevermind it says it right here: https://leanprover-community.github.io/install/linux.html. It lives in $HOME/.elan. As long as it doesn't get too big (they don't let me keep much in my home directory), that should be fine.

[Jason Rute]

And it looks like that location is customizable (which might come in handy). I think unless I run into problems, I'm fine for now.

[Kevin Buzzard]

Jason Rute said:

Oh, nevermind it says it right here: https://leanprover-community.github.io/install/linux.html. It lives in $HOME/.elan. As long as it doesn't get too big (they don't let me keep much in my home directory), that should be fine.

If you also want mathlib then right now you're looking at about 5 gigs.