system-wide elan

Stream: general

[Patrick Massot]

@Sebastian Ullrich I'd like to try to build a debian package for local deployment for my course. Is it possible to have a system-wide elan It seems elan always tries to install in the user directory

[Patrick Massot]

Or should I forget about elan and install Lean directly?

[Sebastian Ullrich]

You can do a system-wide installation of elan manually - here is Arch Linux's package for rustup for comparison: https://git.archlinux.org/svntogit/community.git/tree/trunk/PKGBUILD?h=packages/rustup#n30

[Patrick Massot]

Is there a command line argument for elan saying where it should install?

[Sebastian Ullrich]

But if you're using a single Lean version for your course, there's probably not much to benefit from elan

[Patrick Massot]

That's probably simpler indeed. Maybe releasing Lean 3.4.2 would also make it feel cleaner

[Sebastian Ullrich]

Yes, I hope I can get to that today

[Patrick Massot]

Thanks