system-wide install

Stream: general

[Miguel Marco]

I am trying to install Lean4+mathlib in the jupyter server we use for teaching.
It is a system where students access with their university credentials, and have a system user associated to them.

Thanks to the vscode-server proxy extension, each student, once logged in, can start a web version of vscode. Now we need to install lean+mathlib in a way that is accessible to every user.

From what i have seen, the elan approach is to install everything at user level. That is, each students should run the corresponding script, initialize a project and so on.

Is there a way to do that steps on a system level, so that each user just has to log in and have a working lean+mathlib environment?

[Mac Malone]

To get elan working at a system level, you may be able to just install it as whatever system user is running the vscode-server. VSCode should then make use of that lean toolchain. This would get a Lean 4 environment for students to use, and VS Code's embedded terminal should allow them to make use of elan executables like lake and lean.

As for mathlib, mathlib is a package, and current Lean package management unfortunately does not permit system wide package installs. You could have a preset package with mathlib already added to you have students open in VS Code. If you want students to create their own packages, you can have them use lake new <pkg> math to automatically add mathlib as a dependency, but they will still need to manually do the lake exe cache get dance to the get the oleans.

[Miguel Marco]

Thanks for the answer. Sadly, that doesn't work for me, since each user runs its own instance of vscode-server (we need to do that, because we impose resource limitations at user level).

I could hack something copying the elan toolchain and the 'lake-packages of a project to usr/local and then linking them from each user directory (in the case of the lake-packages` it is more tricky: i have a copy of the skeleton in each user dir, but the biggest subdirectories are symlinked). It works, but it is an ugly hack.

[Sebastian Ullrich]

Yes, you can put copies of Lean and mathlib4 somewhere and then add them to PATH and LEAN_PATH, respectively. I would say this is one of the few scenarios where touching LEAN_PATH is warranted

[Miguel Marco]

what is exactly the role of LEAN_PATH variable?

[Sebastian Ullrich]

It's the search path for import. Try running lake env bash -c 'echo $LEAN_PATH' in a Lake project

[Miguel Marco]

I see, if i have a global install, and have the proper PATH and LEAN_PATH variables, it should work without having anything specific in the user directory?

[Sebastian Ullrich]

Yes, exactly. Just make sure it's the same Lean version that produced the mathlib4 build files

[Miguel Marco]

thanks!

[Miguel Marco]

I tried that and I get an error message about manifest being outdated :man_shrugging:

[Sebastian Ullrich]

You should not use Lake at all in that case

[Sebastian Ullrich]

If you want users to develop a whole project with multiple files on top of mathlib4... then that's a problem with this approach

[Miguel Marco]

I see, well i will further investigate the approach of having a local project, but symlinking most of the directories to save space

[Mac Malone]

Miguel Marco said:

Thanks for the answer. Sadly, that doesn't work for me, since each user runs its own instance of vscode-server (we need to do that, because we impose resource limitations at user level).

This confuses me a bit. If users run their own instance of vscode-server, why not have them run their own instance of elan as well?

[Miguel Marco]

Mac said:

Miguel Marco said:

Thanks for the answer. Sadly, that doesn't work for me, since each user runs its own instance of vscode-server (we need to do that, because we impose resource limitations at user level).

This confuses me a bit. If users run their own instance of vscode-server, why not have them run their own instance of elan as well?

Because that would imply having a copy of all the packages (about 4GB) per user. We have potentially hundreds of users, so we risk running out of disk space.

[Kevin Buzzard]

elan is a very small program. It's mathlib that is huge.

[Miguel Marco]

yes, but if each user uses elan, it will install mathlib for each user.

[Miguel Marco]

the idea is to have averything set up so the students don't have to manage everything: they log in, and have a working environment to follow the course

[Eric Wieser]

Elan only manages lean, not mathlib

[Eric Wieser]

With only one lean version, I get

$ du -d0 -h ~/.elan
895M    /home/gitpod/.elan

[Eric Wieser]

Which is big enough that a global install is probably not a waste of time

[Eric Wieser]

Regarding mathlib; can't you use require mathlib from /"your"/"global"/"mathlib"/"install" in the lakefile?

[Miguel Marco]

Eric Wieser said:

Regarding mathlib; can't you use require mathlib from /"your"/"global"/"mathlib"/"install" in the lakefile?

Maybe... but don't know how to do it. I am kind of lost about what lake does.

[Eric Wieser]

When working on a local project depending on mathlib, lake is the thing downloading 3.6G of packages including mathlib

[Miguel Marco]

and how can i tell it to use a global install instead?

[Eric Wieser]

Eric Wieser said:

Regarding mathlib; can't you use require mathlib from /"your"/"global"/"mathlib"/"install" in the lakefile?

might do it

[Miguel Marco]

I get this error message:

warning: manifest out of date: source kind (git/path) of dependency mathlib changed, use `lake update` to update
info: mathlib: URL has changed; deleting ./lake-packages/mathlib and cloning again
error: permission denied (error code: 13)
  file: ./lake-packages/mathlib/.github/workflows/bors.yml

[Eric Wieser]

Is this while also having your symlink hacks?

[Miguel Marco]

yes. Will try a fresh approach

[Eric Wieser]

I don't know if lake makes a copy of local paths or makes a symlink

[Miguel Marco]

WIth a fresh project, it seems to work, but it still downloads proofwidgets Cli Qq aesop and std

Is there a way to configure to use them from a system wide install too?

[Eric Wieser]

Did the above make a local copy of the mathlib folder?

[Miguel Marco]

No, just the five packages I mentioned

[Mario Carneiro]

Eric Wieser said:

Regarding mathlib; can't you use require mathlib from /"your"/"global"/"mathlib"/"install" in the lakefile?

Note that FilePath abuses the Div operator to interpret the / there. It's a binary operator so the initial / is not syntactically legal

[Miguel Marco]

Oh, I just used a string with the full path:

require mathlib from "/usr/local/share/lean/lake-packages/mathlib"

[Mario Carneiro]

(the main purpose of using "foo" / "bar" style is that it uses the appropriate directory separator for the OS; this is obviously not a problem if you know the system.)

[Mario Carneiro]

(not to mention that "/" works as a directory separator on every supported system anyway)

[Eric Wieser]

I got that leading slash from a docstring

[Mario Carneiro]

double checked, it definitely doesn't work. which docstring?

[Sebastian Ullrich]

I think your best bet is to petition @Mac to allow Lake to inherit global LEAN_PATHs, perhaps as an opt-in. At least from my rough understanding of Lake that should be easier and more robust to do than supporting this kind of global, prebuilt dependency in Lake itself.

[Mac Malone]

@Sebastian Ullrich Lake should already inherit the global LEAN_PATH. If it does not, that is a bug.

[Sebastian Ullrich]

Oh! I briefly looked at the code yesterday and assumed it was by design to make the build more hermetic, but I didn't actually try

[Mac Malone]

Eric Wieser said:

I got that leading slash from a docstring

Oh, did your eyes fall on the /"path"/"dir" part of the require syntax docstring and extrapolate from there? If so, sorry! The non-git require syntax does not have a leading slash (as the docstring demonstrates at the top).

[Sebastian Ullrich]

@Miguel Marco so if it doesn't work with mathlib4 in LEAN_PATH and not in the lakefile, please open an issue in the lean4 repo :)