Zulip Chat Archive

Stream: general

Topic: system-wide elan


view this post on Zulip Patrick Massot (Jan 18 2019 at 09:33):

@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

view this post on Zulip Patrick Massot (Jan 18 2019 at 09:33):

Or should I forget about elan and install Lean directly?

view this post on Zulip Sebastian Ullrich (Jan 18 2019 at 09:40):

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

view this post on Zulip Patrick Massot (Jan 18 2019 at 09:42):

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

view this post on Zulip Sebastian Ullrich (Jan 18 2019 at 09:43):

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

view this post on Zulip Patrick Massot (Jan 18 2019 at 09:44):

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

view this post on Zulip Sebastian Ullrich (Jan 18 2019 at 09:45):

Yes, I hope I can get to that today

view this post on Zulip Patrick Massot (Jan 18 2019 at 09:45):

Thanks


Last updated: May 15 2021 at 00:39 UTC