installing Lean on university computer

Stream: lean4

[Floris van Doorn]

I want to install on some university computers, and I have a few questions:

• Once VSCode (and git) is installed on Ubuntu, does one require root access to install Lean itself?
• The home directory is on an old and slow (and remote) file server. If I have a symlink in ~/.elan and ~/.cache to another folder, will Lean (and the cache) respect these symlinks?
• Or alternatively, is it still possible to set LEAN_PATH or a similar environment variable to set the location for elan and the cache?

[Julian Berman]

ELAN_HOME is the envvar for telling elan where to put stuff (i.e. it defaults to ~/.elan)

[Jannis Limperg]

I think I tried a symlinked ~/.elan at some point and it caused problems, but I don't recall the details. Root should not be necessary to install elan and Lean.

[François G. Dorais]

Does ELAN_HOME just control where elan is or does it also control where the cache is?

[Eric Wieser]

You can also use elan toolchain link to point it at a toolchain stored somewhere else, so that only elan itself runs from the slow directory

[Floris van Doorn]

Cache seems to be controlled by the environment variable XDG_CACHE_HOME (source)

[Floris van Doorn]

I'll try setting ELAN_HOME and XDG_CACHE_HOME before doing any Lean-install, and hopefully that will result in my home directory not being used at all.

[François G. Dorais]

Please let us know how that works out! I personally need to do the same kind of thing here in the near future.

[Kevin Buzzard]

What does the blind sudo in the standard Linux set-up script do if root isn't needed?

[Jannis Limperg]

This script? The sudos install git, curl and VSCode.

[François G. Dorais]

Floris van Doorn said:

I'll try setting ELAN_HOME and XDG_CACHE_HOME before doing any Lean-install, and hopefully that will result in my home directory not being used at all.

Apologies for my impatience, did it work?

[Floris van Doorn]

I haven't tried yet, and it will probably take another week for me to try to do this setup.

[Floris van Doorn]

Sorry, I forgot to report back here. This is all working perfectly.

[Ruben Van de Velde]

Do you want to write up what you did exactly? :)

[Floris van Doorn]

It was done in collaboration with the IT-support here in Bonn, so I didn't execute all commands myself.
But basically, if you set the ELAN_HOME and XDG_CACHE_HOME environment variables before you do the Lean installation (and make sure these environment variables persist on later logins), then those are the places where Lean toolchains and compressed .olean caches are stored, and you can ensure that your home directory is not touched at all.

(note: in #new members > Looking for help @ 💬 @Julian Berman mentions you can also set $MATHLIB_CACHE_DIR instead of $XDG_CACHE_HOME)

[Julian Berman]

I'm not in front of lean but I may have misremembered whether MATHLIB_CACHE_DIR still exists these days -- it definitely did in lean 3 (I wrote the line which did it) but glancing at cache says maybe it does not anymore: https://github.com/leanprover-community/mathlib4/blob/24c597596e1eab32ef9047e2ca944e099df3d294/Cache/IO.lean#L47 so you may really just have XDG_CACHE_HOME at this point

[Julian Berman]

If someone is interested in having that work, https://github.com/leanprover-community/mathlib4/pull/21480 adds it.

[Kim Morrison]

I would love to have a CI workflow that installs things using this setup, so:

1. we can remain confident that the setup continues to work
2. if done nicely, people could even use it as a template to crib from

[François G. Dorais]

I'm a little bit concerned about setting XDG_CACHE_HOME since that's not a lean/lake/elan specific variable. I'm also concerned about Windows/VMWare installs since Windows remarkably sucks at sharing. Does anyone know enough about this to relieve/confirm my concerns?

[Kim Morrison]

@François G. Dorais, #21480 above allows you to set MATHLIB_CACHE_DIR instead of XDG_CACHE_HOME.

[Kim Morrison]

I don't understand what your concern is about Windows/VMWare. Are you saying you don't think this setup will work? Or something else?

[François G. Dorais]

Yes. I'm concerned because Windows/VMWare loves to lock files when another process uses them. I want all my students to be able to access the cache files at the same time (read only) but that hasn't been working reliably for me.

PS: I'm not a habitual Windows user so much of this may be due to my ignorance.

[François G. Dorais]

PPS: I'm hoping we will move away from VMWare but universities move slowly...